theorem LovaszLocalLemma.cond_le_of_indepSet {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s t : Set Ω} (hs : MeasurableSet s) (h : ProbabilityTheory.IndepSet t s μ) : μ[t | s] ≤ μ t

For independent measurable sets $t$ and $s$, the conditional measure $\mu[t \mid s]$ is bounded above by $\mu(t)$.

theorem LovaszLocalLemma.indepSet_of_disjoint_support {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {N m_count : ℕ} {β : Fin N → Type u_2} [(j : Fin N) → MeasurableSpace (β j)] {X : (j : Fin N) → Ω → β j} (hX_indep : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (j : Fin N), Measurable (X j)) {E : Fin m_count → Set Ω} {B : Fin m_count → Finset (Fin N)} (hE_dep : ∀ (i : Fin m_count), MeasurableSet (E i)) (i : Fin m_count) (S : Finset (Fin m_count)) (h_disj : ∀ j ∈ S, Disjoint ↑(B i) ↑(B j)) : ProbabilityTheory.IndepSet (E i) (⋂ j ∈ ↑S, (E j)ᶜ) μ

If event $E_i$ depends only on the variables indexed by $B_i$ and the sets of variables $B_i$, $B_j$ are disjoint for all $j \in S$, then $E_i$ is independent of $\bigcap_{j \in S} E_j^c$.

theorem LovaszLocalLemma.lll_bound_to_ennreal {d : ℕ} {p : ℝ} (hLLL : Real.exp 1 * p * (↑d + 1) ≤ 1) (hp_nonneg : 0 ≤ p) : ENNReal.ofReal (Real.exp 1) * ENNReal.ofReal p * (↑d + 1) ≤ 1

Transfers the real-valued LLL hypothesis $e \cdot p \cdot (d+1) \le 1$ into the corresponding ℝ≥0∞ (extended nonneg real) inequality.

theorem LovaszLocalLemma.lovasz_local_lemma_rv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {N m : ℕ} {β : Fin N → Type u_2} [(j : Fin N) → MeasurableSpace (β j)] {X : (j : Fin N) → Ω → β j} (hX_indep : ProbabilityTheory.iIndepFun X μ) (hX_meas : ∀ (j : Fin N), Measurable (X j)) {E : Fin m → Set Ω} (hE_meas : ∀ (i : Fin m), MeasurableSet (E i)) {B : Fin m → Finset (Fin N)} (hE_dep : ∀ (i : Fin m), MeasurableSet (E i)) {d : ℕ} {p : ℝ} (hd : ∀ (i : Fin m), {j : Fin m | j ≠ i ∧ (B i ∩ B j).Nonempty}.card ≤ d) (hp : ∀ (i : Fin m), (μ (E i)).toReal ≤ p) (hLLL : Real.exp 1 * p * (↑d + 1) ≤ 1) : 0 < μ (⋂ (i : Fin m), (E i)ᶜ)

(Theorem 1.1.8, Lovász Local Lemma — random variable / mutual independence model) Let events $(E_i)_{i < m}$ each depend only on a subset $B_i$ of a family of mutually independent random variables $(X_j)_{j < N}$. If each event has probability at most $p$, each $B_i$ intersects at most $d$ other $B_j$, and $e \cdot p \cdot (d+1) \le 1$, then $\mu\bigl(\bigcap_i E_i^c\bigr) > 0$.