def LopsidedLLL.avoidSet {Ω : Type u_1} {ι : Type u_2} (A : ι → Set Ω) (S : Finset ι) : Set Ω

The event that all events $A_j$ for $j \in S$ fail to occur, i.e. $\bigcap_{j \in S} A_j^c$.

theorem LopsidedLLL.avoidSet_measurableSet {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {A : ι → Set Ω} (hA : ∀ (i : ι), MeasurableSet (A i)) (S : Finset ι) : MeasurableSet (avoidSet A S)

If each $A_i$ is measurable, then avoidSet A S = ⋂_{j ∈ S} (A j)ᶜ is measurable.

theorem LopsidedLLL.avoidSet_insert_eq {Ω : Type u_1} {ι : Type u_2} [DecidableEq ι] (A : ι → Set Ω) (S : Finset ι) (j : ι) : avoidSet A (insert j S) = avoidSet A S ∩ (A j)ᶜ

Recursive identity: avoidSet A (insert j S) = avoidSet A S ∩ (A j)ᶜ.

theorem LopsidedLLL.avoidSet_union_eq {Ω : Type u_1} {ι : Type u_2} [DecidableEq ι] (A : ι → Set Ω) (S T : Finset ι) : avoidSet A (S ∪ T) = avoidSet A S ∩ avoidSet A T

avoidSet turns finset union into set intersection: avoidSet A (S ∪ T) = avoidSet A S ∩ avoidSet A T.

theorem LopsidedLLL.prod_one_sub_ne_zero {ι : Type u_2} [DecidableEq ι] (S : Finset ι) (x : ι → ENNReal) (hx : ∀ i ∈ S, x i < 1) : ∏ j ∈ S, (1 - x j) ≠ 0

If $x_i < 1$ for each $i \in S$ (in ℝ≥0∞), then $\prod_{j \in S}(1 - x_j) \neq 0$.

theorem LopsidedLLL.prod_one_sub_ne_top {ι : Type u_2} (S : Finset ι) (x : ι → ENNReal) : ∏ j ∈ S, (1 - x j) ≠ ⊤

The ℝ≥0∞-product $\prod_{j \in S}(1 - x_j)$ is bounded above by $1$, hence is never $\infty$.

theorem LopsidedLLL.prod_le_prod_of_superset {ι : Type u_2} [DecidableEq ι] {S₁ S₂ : Finset ι} {f : ι → ENNReal} (h : S₁ ⊆ S₂) (hf : ∀ i ∈ S₂, f i ≤ 1) : ∏ i ∈ S₂, f i ≤ ∏ i ∈ S₁, f i

If each factor satisfies $f_i \le 1$, then enlarging the index set can only decrease the product: $\prod_{i \in S_2} f_i \le \prod_{i \in S_1} f_i$ when $S_1 \subseteq S_2$.

theorem LopsidedLLL.avoidSet_ge_prod {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure ν] {A : Fin n → Set Ω} (hA : ∀ (i : Fin n), MeasurableSet (A i)) {x : Fin n → ENNReal} (hx_lt : ∀ (i : Fin n), x i < 1) (S : Finset (Fin n)) (hkey : ∀ j ∈ S, ∀ T ⊆ S, j ∉ T → ν[A j | avoidSet A T] ≤ x j) : ν (avoidSet A S) ≥ ∏ j ∈ S, (1 - x j)

Iteratively expanding conditional probabilities: under the hypothesis that for every $j \in S$ and every subset $T \subseteq S$ with $j \notin T$ one has $\nu(A_j \mid \text{avoidSet}\ A\ T) \le x_j$, one obtains the lower bound $\nu(\text{avoidSet}\ A\ S) \ge \prod_{j \in S}(1 - x_j)$.

theorem LopsidedLLL.key_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Fin n → Set Ω) (hA : ∀ (i : Fin n), MeasurableSet (A i)) (N : Fin n → Finset (Fin n)) (x : Fin n → ENNReal) (hx_lt : ∀ (i : Fin n), x i < 1) (hlop : ∀ (i : Fin n), ∀ S ⊆ Finset.univ \ (N i ∪ {i}), μ[A i | avoidSet A S] ≤ μ (A i)) (hbound : ∀ (i : Fin n), μ (A i) ≤ x i * ∏ j ∈ N i, (1 - x j)) (S : Finset (Fin n)) (i : Fin n) (hiS : i ∉ S) : μ[A i | avoidSet A S] ≤ x i

Core inductive estimate for the Lopsided Local Lemma: under the lopsidependency hypothesis hlop and the bound $\mu(A_i) \le x_i \prod_{j \in N(i)}(1-x_j)$, one has $\mu(A_i \mid \text{avoidSet}\ A\ S) \le x_i$ for every $i \notin S$.

theorem LopsidedLLL.lopsided_local_lemma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Fin n → Set Ω) (hA : ∀ (i : Fin n), MeasurableSet (A i)) (N : Fin n → Finset (Fin n)) (x : Fin n → ENNReal) (hx_lt : ∀ (i : Fin n), x i < 1) (hlop : ∀ (i : Fin n), ∀ S ⊆ Finset.univ \ (N i ∪ {i}), μ[A i | avoidSet A S] ≤ μ (A i)) (hbound : ∀ (i : Fin n), μ (A i) ≤ x i * ∏ j ∈ N i, (1 - x j)) : μ (⋂ (i : Fin n), (A i)ᶜ) ≥ ∏ i : Fin n, (1 - x i)

Lopsided Local Lemma (Theorem 6.5.1, general form): given events $A_1,\dots,A_n$ with a lopsidependency neighbourhood $N$, weights $x_i \in [0,1)$, the lopsidependency hypothesis $\mu(A_i \mid \bigcap_{j \in S}\overline{A_j}) \le \mu(A_i)$ for $S$ disjoint from $N(i) \cup \{i\}$, and $\mu(A_i) \le x_i \prod_{j \in N(i)}(1-x_j)$, one has $\mu(\bigcap_i \overline{A_i}) \ge \prod_i (1 - x_i)$.