Chebyshev majority bound #
If k ≥ 9/δ independent events each have probability ≥ 2/3, then the
probability that strictly more than k/2 of them hold is ≥ 1 - δ.
Proof route: indicator random variables, Popoviciu's variance bound, independence for variance of a sum, then Chebyshev's inequality.
References #
- Boucheron, Lugosi, Massart, "Concentration Inequalities", Chapter 2
theorem
ProbabilityTheory.chebyshev_majority_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{k : ℕ}
{δ : ℝ}
(h_delta_pos : 0 < δ)
(hk : 9 / δ ≤ ↑k)
(events : Fin k → Set Ω)
(hevents_meas : ∀ (j : Fin k), MeasurableSet (events j))
(hindep : iIndepSet (fun (j : Fin k) => events j) μ)
(hprob : ∀ (j : Fin k), μ (events j) ≥ ENNReal.ofReal (2 / 3))
:
Chebyshev majority bound: if k ≥ 9/δ independent events each have
probability ≥ 2/3, the probability that strictly more than k/2 of them
hold is ≥ 1 - δ.