Ballot problem

This file proves Theorem 30 from the 100 Theorems List.

The ballot problem asks, if in an election, candidate A receives p votes whereas candidate B receives q votes where p > q, what is the probability that candidate A is strictly ahead throughout the count. The probability of this is (p - q) / (p + q).

Main definitions

• countedSequence: given natural numbers p and q, countedSequence p q is the set of all lists containing p of 1s and q of -1s representing the votes of candidate A and B respectively.
• staysPositive: is the set of lists of integers which suffix has positive sum. In particular, the intersection of this set with countedSequence is the set of lists where candidate A is strictly ahead.

Main result

• ballot_problem: the ballot problem.

def Ballot.staysPositive : Set (List ℤ)

The set of nonempty lists of integers which suffix has positive sum.

Equations

• Ballot.staysPositive = {l : List ℤ | ∀ (l₂ : List ℤ), l₂ ≠ [] → l₂ <:+ l → 0 < l₂.sum}

@[simp]

theorem Ballot.staysPositive_nil : [] ∈ staysPositive

theorem Ballot.staysPositive_suffix {l₁ l₂ : List ℤ} (hl₂ : l₂ ∈ staysPositive) (h : l₁ <:+ l₂) : l₁ ∈ staysPositive

theorem Ballot.staysPositive_cons {x : ℤ} {l : List ℤ} : x :: l ∈ staysPositive ↔ l ∈ staysPositive ∧ 0 < x + l.sum

theorem Ballot.sum_nonneg_of_staysPositive {l : List ℤ} : l ∈ staysPositive → 0 ≤ l.sum

theorem Ballot.staysPositive_cons_pos (x : ℤ) (hx : 0 < x) (l : List ℤ) : x :: l ∈ staysPositive ↔ l ∈ staysPositive

def Ballot.countedSequence (p q : ℕ) : Set (List ℤ)

countedSequence p q is the set of lists of integers for which every element is +1 or -1, there are p lots of +1 and q lots of -1.

This represents vote sequences where candidate +1 receives p votes and candidate -1 receives q votes.

Equations

• Ballot.countedSequence p q = {l : List ℤ | List.count 1 l = p ∧ List.count (-1) l = q ∧ ∀ x ∈ l, x = 1 ∨ x = -1}

theorem Ballot.mem_countedSequence_iff_perm {p q : ℕ} {l : List ℤ} : l ∈ countedSequence p q ↔ l.Perm (List.replicate p 1 ++ List.replicate q (-1))

An alternative definition of countedSequence that uses List.Perm.

@[simp]

theorem Ballot.counted_right_zero (p : ℕ) : countedSequence p 0 = {List.replicate p 1}

@[simp]

theorem Ballot.counted_left_zero (q : ℕ) : countedSequence 0 q = {List.replicate q (-1)}

theorem Ballot.mem_of_mem_countedSequence {p q : ℕ} {l : List ℤ} (hl : l ∈ countedSequence p q) {x : ℤ} (hx : x ∈ l) : x = 1 ∨ x = -1

theorem Ballot.length_of_mem_countedSequence {p q : ℕ} {l : List ℤ} (hl : l ∈ countedSequence p q) : l.length = p + q

theorem Ballot.counted_eq_nil_iff {p q : ℕ} {l : List ℤ} (hl : l ∈ countedSequence p q) : l = [] ↔ p = 0 ∧ q = 0

theorem Ballot.counted_ne_nil_left {p q : ℕ} (hp : p ≠ 0) {l : List ℤ} (hl : l ∈ countedSequence p q) : l ≠ []

theorem Ballot.counted_ne_nil_right {p q : ℕ} (hq : q ≠ 0) {l : List ℤ} (hl : l ∈ countedSequence p q) : l ≠ []

theorem Ballot.counted_succ_succ (p q : ℕ) : countedSequence (p + 1) (q + 1) = List.cons 1 '' countedSequence p (q + 1) ∪ List.cons (-1) '' countedSequence (p + 1) q

theorem Ballot.countedSequence_finite (p q : ℕ) : (countedSequence p q).Finite

theorem Ballot.countedSequence_nonempty (p q : ℕ) : (countedSequence p q).Nonempty

theorem Ballot.sum_of_mem_countedSequence {p q : ℕ} {l : List ℤ} (hl : l ∈ countedSequence p q) : l.sum = ↑p - ↑q

theorem Ballot.disjoint_bits (p q : ℕ) : Disjoint (List.cons 1 '' countedSequence p (q + 1)) (List.cons (-1) '' countedSequence (p + 1) q)

@[instance_reducible]

def Ballot.measurableSpace_list_int : MeasurableSpace (List ℤ)

Equations

• Ballot.measurableSpace_list_int = ⊤

theorem Ballot.count_countedSequence (p q : ℕ) : MeasureTheory.Measure.count (countedSequence p q) = ↑((p + q).choose p)

theorem Ballot.first_vote_pos (p q : ℕ) : 0 < p + q → (ProbabilityTheory.uniformOn (countedSequence p q)) {l : List ℤ | l.headI = 1} = ↑p / (↑p + ↑q)

theorem Ballot.headI_mem_of_nonempty {α : Type u_1} [Inhabited α] {l : List α} : l ≠ [] → l.headI ∈ l

theorem Ballot.first_vote_neg (p q : ℕ) (h : 0 < p + q) : (ProbabilityTheory.uniformOn (countedSequence p q)) {l : List ℤ | l.headI = 1}ᶜ = ↑q / (↑p + ↑q)

theorem Ballot.ballot_same (p : ℕ) : (ProbabilityTheory.uniformOn (countedSequence (p + 1) (p + 1))) staysPositive = 0

theorem Ballot.ballot_edge (p : ℕ) : (ProbabilityTheory.uniformOn (countedSequence (p + 1) 0)) staysPositive = 1

theorem Ballot.countedSequence_int_pos_counted_succ_succ (p q : ℕ) : countedSequence (p + 1) (q + 1) ∩ {l : List ℤ | l.headI = 1} = List.cons 1 '' countedSequence p (q + 1)

theorem Ballot.ballot_pos (p q : ℕ) : (ProbabilityTheory.uniformOn (countedSequence (p + 1) (q + 1) ∩ {l : List ℤ | l.headI = 1})) staysPositive = (ProbabilityTheory.uniformOn (countedSequence p (q + 1))) staysPositive

theorem Ballot.countedSequence_int_neg_counted_succ_succ (p q : ℕ) : countedSequence (p + 1) (q + 1) ∩ {l : List ℤ | l.headI = 1}ᶜ = List.cons (-1) '' countedSequence (p + 1) q

theorem Ballot.ballot_neg (p q : ℕ) (qp : q < p) : (ProbabilityTheory.uniformOn (countedSequence (p + 1) (q + 1) ∩ {l : List ℤ | l.headI = 1}ᶜ)) staysPositive = (ProbabilityTheory.uniformOn (countedSequence (p + 1) q)) staysPositive

theorem Ballot.ballot_problem' (q p : ℕ) : q < p → ((ProbabilityTheory.uniformOn (countedSequence p q)) staysPositive).toReal = (↑p - ↑q) / (↑p + ↑q)

theorem Ballot.ballot_problem (q p : ℕ) : q < p → (ProbabilityTheory.uniformOn (countedSequence p q)) staysPositive = (↑p - ↑q) / (↑p + ↑q)

The ballot problem.