structure AlgorithmicLLL.LLLCondition (n : ℕ) (P x : Fin n → ℝ) (N : Fin n → Finset (Fin n)) : Prop

Hypotheses for the general (asymmetric) Lovász Local Lemma: weights $x_i \in [0,1)$ such that each event probability satisfies $P_i \le x_i \prod_{j \in N(i)} (1 - x_j)$, where $N(i)$ is the dependency neighborhood of event $i$ (Theorem 6.1.9).

• x_nonneg (i : Fin n) : 0 ≤ x i
• x_lt_one (i : Fin n) : x i < 1
• prob_bound (i : Fin n) : P i ≤ x i * ∏ j ∈ N i, (1 - x j)
• P_nonneg (i : Fin n) : 0 ≤ P i

noncomputable def AlgorithmicLLL.expectedResamplingCount {n : ℕ} (P : Fin n → ℝ) (N : Fin n → Finset (Fin n)) (i : Fin n) : ℝ

Expected number of times event $A_i$ is resampled by the Moser-Tardos algorithm; a key quantity in the algorithmic analysis of the Lovász Local Lemma.

theorem AlgorithmicLLL.expectedResamplingCount_nonneg {n : ℕ} (P : Fin n → ℝ) (N : Fin n → Finset (Fin n)) (i : Fin n) : 0 ≤ expectedResamplingCount P N i

The expected resampling count is nonnegative.

theorem AlgorithmicLLL.moser_tardos_expected_resamplings {n : ℕ} {P x : Fin n → ℝ} {N : Fin n → Finset (Fin n)} (hLLL : LLLCondition n P x N) (i : Fin n) : expectedResamplingCount P N i ≤ x i / (1 - x i)

Moser-Tardos theorem: under the LLL hypothesis, the expected number of times the algorithm resamples event $A_i$ is bounded by $x_i / (1 - x_i)$.