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 numbersp
andq
,countedSequence p q
is the set of all lists containingp
of1
s andq
of-1
s 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 withcountedSequence
is the set of lists where candidate A is strictly ahead.
Main result #
ballot_problem
: the ballot problem.
theorem
Ballot.staysPositive_suffix
{l₁ : List ℤ}
{l₂ : List ℤ}
(hl₂ : l₂ ∈ Ballot.staysPositive)
(h : l₁ <:+ l₂)
:
theorem
Ballot.staysPositive_cons
{x : ℤ}
{l : List ℤ}
:
x :: l ∈ Ballot.staysPositive ↔ l ∈ Ballot.staysPositive ∧ 0 < x + l.sum
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}
Instances For
theorem
Ballot.mem_countedSequence_iff_perm
{p : ℕ}
{q : ℕ}
{l : List ℤ}
:
l ∈ Ballot.countedSequence p q ↔ l.Perm (List.replicate p 1 ++ List.replicate q (-1))
An alternative definition of countedSequence
that uses List.Perm
.
@[simp]
@[simp]
theorem
Ballot.length_of_mem_countedSequence
{p : ℕ}
{q : ℕ}
{l : List ℤ}
(hl : l ∈ Ballot.countedSequence p q)
:
theorem
Ballot.counted_ne_nil_left
{p : ℕ}
{q : ℕ}
(hp : p ≠ 0)
{l : List ℤ}
(hl : l ∈ Ballot.countedSequence p q)
:
l ≠ []
theorem
Ballot.counted_ne_nil_right
{p : ℕ}
{q : ℕ}
(hq : q ≠ 0)
{l : List ℤ}
(hl : l ∈ Ballot.countedSequence p q)
:
l ≠ []
theorem
Ballot.counted_succ_succ
(p : ℕ)
(q : ℕ)
:
Ballot.countedSequence (p + 1) (q + 1) = List.cons 1 '' Ballot.countedSequence p (q + 1) ∪ List.cons (-1) '' Ballot.countedSequence (p + 1) q
@[irreducible]
theorem
Ballot.sum_of_mem_countedSequence
{p : ℕ}
{q : ℕ}
{l : List ℤ}
(hl : l ∈ Ballot.countedSequence p q)
:
theorem
Ballot.disjoint_bits
(p : ℕ)
(q : ℕ)
:
Disjoint (List.cons 1 '' Ballot.countedSequence p (q + 1)) (List.cons (-1) '' Ballot.countedSequence (p + 1) q)
@[irreducible]
theorem
Ballot.count_countedSequence
(p : ℕ)
(q : ℕ)
:
MeasureTheory.Measure.count (Ballot.countedSequence p q) = ↑((p + q).choose p)
theorem
Ballot.first_vote_pos
(p : ℕ)
(q : ℕ)
:
0 < p + q → (ProbabilityTheory.condCount (Ballot.countedSequence p q)) {l : List ℤ | l.headI = 1} = ↑p / (↑p + ↑q)
theorem
Ballot.first_vote_neg
(p : ℕ)
(q : ℕ)
(h : 0 < p + q)
:
(ProbabilityTheory.condCount (Ballot.countedSequence p q)) {l : List ℤ | l.headI = 1}ᶜ = ↑q / (↑p + ↑q)
theorem
Ballot.ballot_same
(p : ℕ)
:
(ProbabilityTheory.condCount (Ballot.countedSequence (p + 1) (p + 1))) Ballot.staysPositive = 0
theorem
Ballot.ballot_edge
(p : ℕ)
:
(ProbabilityTheory.condCount (Ballot.countedSequence (p + 1) 0)) Ballot.staysPositive = 1
theorem
Ballot.ballot_pos
(p : ℕ)
(q : ℕ)
:
(ProbabilityTheory.condCount (Ballot.countedSequence (p + 1) (q + 1) ∩ {l : List ℤ | l.headI = 1}))
Ballot.staysPositive = (ProbabilityTheory.condCount (Ballot.countedSequence p (q + 1))) Ballot.staysPositive
theorem
Ballot.ballot_neg
(p : ℕ)
(q : ℕ)
(qp : q < p)
:
(ProbabilityTheory.condCount (Ballot.countedSequence (p + 1) (q + 1) ∩ {l : List ℤ | l.headI = 1}ᶜ))
Ballot.staysPositive = (ProbabilityTheory.condCount (Ballot.countedSequence (p + 1) q)) Ballot.staysPositive
theorem
Ballot.ballot_problem'
(q : ℕ)
(p : ℕ)
:
q < p → ((ProbabilityTheory.condCount (Ballot.countedSequence p q)) Ballot.staysPositive).toReal = (↑p - ↑q) / (↑p + ↑q)
theorem
Ballot.ballot_problem
(q : ℕ)
(p : ℕ)
:
q < p → (ProbabilityTheory.condCount (Ballot.countedSequence p q)) Ballot.staysPositive = (↑p - ↑q) / (↑p + ↑q)
The ballot problem.