Majority from pairwise independence

Pairwise independent votes, each correct with probability at least 1 / 2 + ε, fail to have a strict majority with probability at most 1 / (4 * ε ^ 2 * m), where m > 0 is the number of votes. More generally the same bound holds for scores in [0, 1] with these expectations. Ties are included in the failure event.

The proof uses Mathlib's variance bound for bounded random variables, additivity of variance under pairwise independence, and Chebyshev's inequality. This is the concentration step in the Goldreich–Levin subset-sum decoder. Adapted from the cslib crypto branch at 5ff69ca.

Main results

• PMF.indepFun_of_map_pair: factorization of a joint PMF proves independence.
• majority_error_bound: pairwise-independent bounded scores concentrate above half.

References

• L. Trevisan, CS276 Lecture 12: Goldreich–Levin, Lemma 4

theorem Cslib.Probability.PMF.indepFun_of_map_pair {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Countable α] [Countable β] (p : PMF Ω) (f : Ω → α) (g : Ω → β) (hf : Measurable f) (hg : Measurable g) (h : PMF.map (fun (ω : Ω) => (f ω, g ω)) p = (PMF.map f p).bind fun (a : α) => PMF.map (fun (b : β) => (a, b)) (PMF.map g p)) : ProbabilityTheory.IndepFun f g p.toMeasure

A factorization of the joint PMF establishes Mathlib's measure-theoretic independence.

theorem Cslib.Probability.majority_error_bound {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (s : Finset ι) (X : ι → Ω → ℝ) (ε : ℝ) (hε : 0 < ε) (hs : s.Nonempty) (hm : ∀ i ∈ s, AEMeasurable (X i) μ) (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, X i ω ∈ Set.Icc 0 1) (hi : (↑s).Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) μ) (he : ∀ i ∈ s, 1 / 2 + ε ≤ ∫ (ω : Ω), X i ω ∂μ) : μ {ω : Ω | ∑ i ∈ s, X i ω ≤ ↑s.card / 2} ≤ ENNReal.ofReal (1 / (4 * ε ^ 2 * ↑s.card))

Pairwise independent scores in [0, 1] with mean at least 1 / 2 + ε have a strict majority except with probability at most 1 / (4 * ε ^ 2 * m).