# Documentation

Archive.Wiedijk100Theorems.BallotProblem

# 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.

Instances For
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.

Instances For
theorem Ballot.mem_countedSequence_iff_perm {p : } {q : } {l : } :

An alternative definition of countedSequence that uses List.Perm.

@[simp]
theorem Ballot.counted_right_zero (p : ) :
= {}
@[simp]
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 : ) :
= 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 []
theorem Ballot.sum_of_mem_countedSequence {p : } {q : } {l : } (hl : ) :
= p - q
theorem Ballot.count_countedSequence (p : ) (q : ) :
MeasureTheory.Measure.count () = ↑(Nat.choose (p + q) p)
theorem Ballot.first_vote_pos (p : ) (q : ) :
0 < p + q {l | = 1} = p / (p + q)
theorem Ballot.headI_mem_of_nonempty {α : Type u_1} [] {l : List α} :
l [] l
theorem Ballot.first_vote_neg (p : ) (q : ) (h : 0 < p + q) :
{l | = 1} = q / (p + q)
theorem Ballot.ballot_edge (p : ) :
= 1
theorem Ballot.ballot_neg (p : ) (q : ) (qp : q < p) :
theorem Ballot.ballot_problem' (q : ) (p : ) :
q < p = (p - q) / (p + q)
theorem Ballot.ballot_problem (q : ) (p : ) :
q < p = (p - q) / (p + q)

The ballot problem.