Condorcet's jury theorem

TheoremCondorcet's jury theorem#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(X_0, X_1, \dots\) be measurable maps from \(\Omega\) to \(\{\text{true}, \text{false}\}\) (the votes, true meaning a correct vote), and let \(p\) be a number with \(1/2 < p < 1\). Suppose that each vote is correct with probability \(p\), that is \(\mu(X_i = \text{true}) = p\) for every \(i\), and that the events \(\{X_i = \text{true}\}\) are independent: for every nonempty finite set \(s\) of indices, \(\mu\bigl(\bigcap_{i \in s} \{X_i = \text{true}\}\bigr) = \prod_{i \in s} \mu(X_i = \text{true})\). For \(n \in \mathbb{N}\) let \(M_n\) be the event that more than \(\lfloor n/2 \rfloor\) of the first \(n\) votes \(X_0, \dots, X_{n-1}\) are correct. Then \(\mu(M_n) \to 1\) as \(n \to \infty\), and \(\mu(M_n) > p\) for every odd \(n > 1\).

theorem condorcet_jury_theorem {Ω : Type*} [MeasurableSpace Ω]
    {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
    (X : ℕ → Ω → Bool) (p : ENNReal) (hp : 1 / 2 < p) (hp2 : p < 1)
    (hmeas : ∀ i, Measurable (X i))
    (hmarg : ∀ i, μ {ω | X i ω = true} = p)
    (hindep : ∀ s : Finset ℕ, s.Nonempty →
      μ (s.inf fun i => {ω | X i ω = true}) =
        s.prod fun i => μ {ω | X i ω = true}) :
    Filter.Tendsto
      (fun n => μ {ω | n / 2 < (Finset.filter (fun i => X i ω = true) (Finset.range n)).card})
      Filter.atTop (nhds 1) ∧
    ∀ n : ℕ, Odd n → 1 < n →
      p < μ {ω | n / 2 < (Finset.filter (fun i => X i ω = true) (Finset.range n)).card}

Sources

• https://en.wikipedia.org/wiki/Condorcet%27s_jury_theorem.

Used by 1

Used byCondorcet's jury theorem for mutually independent votes

TheoremCondorcet's jury theorem for mutually independent votes#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(X_0, X_1, \dots\) be measurable maps from \(\Omega\) to \(\{\text{true}, \text{false}\}\) (the votes, true meaning a correct vote) that are mutually independent random variables under \(\mu\), and let \(p\) be a number with \(1/2 < p < 1\). Suppose that each vote is correct with probability \(p\), that is \(\mu(X_i = \text{true}) = p\) for every \(i\). For \(n \in \mathbb{N}\) let \(M_n\) be the event that more than \(\lfloor n/2 \rfloor\) of the first \(n\) votes \(X_0, \dots, X_{n-1}\) are correct. Then \(\mu(M_n) \to 1\) as \(n \to \infty\), and \(\mu(M_n) > p\) for every odd \(n > 1\).

theorem condorcet_jury_theorem_of_iIndepFun {Ω : Type*} [MeasurableSpace Ω]
    {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
    (X : ℕ → Ω → Bool) (p : ENNReal) (hp : 1 / 2 < p) (hp2 : p < 1)
    (hmeas : ∀ i, Measurable (X i))
    (hmarg : ∀ i, μ {ω | X i ω = true} = p)
    (hindep : ProbabilityTheory.iIndepFun X μ) :
    Filter.Tendsto
      (fun n => μ {ω | n / 2 < (Finset.filter (fun i => X i ω = true) (Finset.range n)).card})
      Filter.atTop (nhds 1) ∧
    ∀ n : ℕ, Odd n → 1 < n →
      p < μ {ω | n / 2 < (Finset.filter (fun i => X i ω = true) (Finset.range n)).card}

Uses 1

Proof usesCondorcet's jury theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.