theorem LopsidedLLL.exp_neg_inv_le_real (m : ℕ) (hm : 0 < m) : Real.exp (-(1 / ↑m)) ≤ ↑m / (↑m + 1)

Real-valued helper: for $m \ge 1$ one has $e^{-1/m} \le m/(m+1)$.

theorem LopsidedLLL.one_sub_inv_pow_ge_inv_exp_real (d : ℕ) : Real.exp (-1) ≤ (1 - 1 / (↑d + 1)) ^ d

Real-valued inequality $e^{-1} \le (1 - 1/(d+1))^d$, used in the symmetric Lopsided LLL.

theorem LopsidedLLL.ennreal_one_sub_inv_pow_ge (d : ℕ) : ENNReal.ofReal (Real.exp (-1)) ≤ (1 - (↑d + 1)⁻¹) ^ d

ℝ≥0∞-valued version of one_sub_inv_pow_ge_inv_exp_real: $e^{-1} \le (1 - (d+1)^{-1})^d$ as extended nonnegative reals.

theorem LopsidedLLL.lopsided_local_lemma_symmetric {Ω : 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)) (hlop : ∀ (i : Fin n), ∀ S ⊆ Finset.univ \ (N i ∪ {i}), μ[A i | avoidSet A S] ≤ μ (A i)) (d : ℕ) (p : ENNReal) (hNd : ∀ (i : Fin n), (N i).card ≤ d) (hprob : ∀ (i : Fin n), μ (A i) ≤ p) (hepd : ENNReal.ofReal (Real.exp 1) * p * (↑d + 1) ≤ 1) : 0 < μ (⋂ (i : Fin n), (A i)ᶜ)

Symmetric Lopsided Local Lemma (Corollary 6.5.2): if every $\mu(A_i) \le p$, every lopsidependency neighbourhood satisfies $|N(i)| \le d$, and $e \cdot p \cdot (d+1) \le 1$, then $\mu(\bigcap_i \overline{A_i}) > 0$.