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.

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

Equations
Instances For
theorem Ballot.staysPositive_suffix {l₁ : } {l₂ : } (hl₂ : ) (h : l₁ <:+ l₂) :
theorem Ballot.staysPositive_cons {x : } {l : } :
0 < x + l.sum
theorem Ballot.sum_nonneg_of_staysPositive {l : } :
0 l.sum
theorem Ballot.staysPositive_cons_pos (x : ) (hx : 0 < x) (l : ) :
def Ballot.countedSequence (p : ) (q : ) :
Set ()

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
Instances For
theorem Ballot.mem_countedSequence_iff_perm {p : } {q : } {l : } :
l.Perm ( ++ List.replicate q (-1))

An alternative definition of countedSequence that uses List.Perm.

@[simp]
theorem Ballot.counted_right_zero (p : ) :
= {}
@[simp]
theorem Ballot.counted_left_zero (q : ) :
= {List.replicate q (-1)}
theorem Ballot.mem_of_mem_countedSequence {p : } {q : } {l : } (hl : ) {x : } (hx : x l) :
x = 1 x = -1
theorem Ballot.length_of_mem_countedSequence {p : } {q : } {l : } (hl : ) :
l.length = p + q
theorem Ballot.counted_eq_nil_iff {p : } {q : } {l : } (hl : ) :
l = [] p = 0 q = 0
theorem Ballot.counted_ne_nil_left {p : } {q : } (hp : p 0) {l : } (hl : ) :
l []
theorem Ballot.counted_ne_nil_right {p : } {q : } (hq : q 0) {l : } (hl : ) :
l []
@[irreducible]
theorem Ballot.countedSequence_finite (p : ) (q : ) :
().Finite
theorem Ballot.countedSequence_nonempty (p : ) (q : ) :
().Nonempty
theorem Ballot.sum_of_mem_countedSequence {p : } {q : } {l : } (hl : ) :
l.sum = p - q
@[irreducible]
theorem Ballot.count_countedSequence (p : ) (q : ) :
MeasureTheory.Measure.count () = ((p + q).choose p)
theorem Ballot.first_vote_pos (p : ) (q : ) :
0 < p + q {l : | l.headI = 1} = p / (p + q)
theorem Ballot.headI_mem_of_nonempty {α : Type u_1} [] {l : List α} :