# mathlib3documentation

mathlib-archive / wiedijk_100_theorems.ballot_problem

# Ballot problem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• counted_sequence: given natural numbers p and q, counted_sequence 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.
• stays_positive: is the set of lists of integers which suffix has positive sum. In particular, the intersection of this set with counted_sequence is the set of lists where candidate A is strictly ahead.

## Main result #

• ballot: the ballot problem.

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

Equations
@[simp]
theorem ballot.stays_positive_cons_pos (x : ) (hx : 0 < x) (l : list ) :

counted_sequence 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
theorem ballot.mem_counted_sequence_iff_perm {p q : } {l : list } :
l ~ ++ (-1)

An alternative definition of counted_sequence that uses list.perm.

@[simp]
theorem ballot.counted_right_zero (p : ) :
= 1}
@[simp]
theorem ballot.counted_left_zero (q : ) :
= (-1)}
theorem ballot.mem_of_mem_counted_sequence {p q : } {l : list } (hl : l ) {x : } (hx : x l) :
x = 1 x = -1
theorem ballot.length_of_mem_counted_sequence {p q : } {l : list } (hl : l ) :
l.length = p + q
theorem ballot.counted_eq_nil_iff {p q : } {l : list } (hl : l ) :
p = 0 q = 0
theorem ballot.counted_ne_nil_left {p q : } (hp : p 0) {l : list } (hl : l ) :
theorem ballot.counted_ne_nil_right {p q : } (hq : q 0) {l : list } (hl : l ) :
theorem ballot.sum_of_mem_counted_sequence {p q : } {l : list } (hl : l ) :
l.sum = p - q
theorem ballot.disjoint_bits (p q : ) :
theorem ballot.count_counted_sequence (p q : ) :
= ((p + q).choose p)
theorem ballot.first_vote_pos (p q : ) :
0 < p + q {l : | l.head = 1} = p / (p + q)
theorem ballot.head_mem_of_nonempty {α : Type u_1} [inhabited α] {l : list α} (hl : l list.nil) :