theorem JansonInequality.harris_claim {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure ν] {k : ℕ} (A : Fin k → Set Ω) (hA_meas : ∀ (i : Fin k), MeasurableSet (A i)) (dep : Fin k → Fin k → Prop) [DecidableRel dep] (hdep_symm : ∀ (i j : Fin k), dep i j → dep j i) (hdep_irrefl : ∀ (i : Fin k), ¬dep i i) (hindep : ∀ (i j : Fin k), ¬dep i j → i ≠ j → ν (A i ∩ A j) = ν (A i) * ν (A j)) (i : Fin k) (r_i : ℝ) (hr_cond : r_i * (ν (⋂ j ∈ {j : Fin k | ↑j < ↑i}, (A j)ᶜ)).toReal = (ν (A i ∩ ⋂ j ∈ {j : Fin k | ↑j < ↑i}, (A j)ᶜ)).toReal) (hpos : 0 < (ν (⋂ j ∈ {j : Fin k | ↑j < ↑i}, (A j)ᶜ)).toReal) : r_i ≥ (ν (A i)).toReal - ∑ j : Fin k with ↑j < ↑i ∧ dep i j, (ν (A i ∩ A j)).toReal

Harris-FKG-style inequality used in the proof of Janson's inequality. For an event $A_i$ conditioned on none of $A_1, \dots, A_{i-1}$ occurring, the conditional probability $r_i$ is at least $\Pr(A_i) - \sum_{j < i,\, j \sim i} \Pr(A_i \cap A_j)$, where $j \sim i$ denotes dependence.

theorem JansonInequality.janson_inequality_II {μ Δ v : ℝ} (hμ_pos : 0 < μ) (hΔ_ge_μ : Δ ≥ μ) (hbound : ∀ (q : ℝ), 0 ≤ q → q ≤ 1 → v ≤ Real.exp (-q * μ + q ^ 2 * Δ / 2)) : v ≤ Real.exp (-μ ^ 2 / (2 * Δ))

Janson inequality II (Theorem 8.1.8). If $\Delta \geq \mu$ and for all $q \in [0,1]$ the bound $v \leq \exp(-q\mu + q^2 \Delta / 2)$ holds, then $v \leq \exp(-\mu^2/(2\Delta))$ (obtained by optimizing at $q = \mu/\Delta$). In particular this gives $\Pr(X = 0) \leq \exp(-\mu^2/(2\Delta))$.