mathlib3 documentation

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.

def ballot.stays_positive :

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

Equations

ballot.stays_positive = {l : list ℤ | ∀ (l₂ : list ℤ), l₂ ≠ list.nil → l₂ <:+ l → 0 < l₂.sum}

@[simp]

theorem ballot.stays_positive_nil :

list.nil ∈ ballot.stays_positive

theorem ballot.stays_positive_cons_pos (x : ℤ) (hx : 0 < x) (l : list ℤ) :

x :: l ∈ ballot.stays_positive ↔ l ∈ ballot.stays_positive

def ballot.counted_sequence (p q : ℕ) :

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

ballot.counted_sequence p q = {l : list ℤ | list.count 1 l = p ∧ list.count (-1) l = q ∧ ∀ (x : ℤ), x ∈ l → x = 1 ∨ x = -1}

theorem ballot.mem_counted_sequence_iff_perm {p q : ℕ} {l : list ℤ} :

l ∈ ballot.counted_sequence p q ↔ l ~ list.replicate p 1 ++ list.replicate q (-1)

An alternative definition of counted_sequence that uses list.perm.

@[simp]

theorem ballot.counted_right_zero (p : ℕ) :

ballot.counted_sequence p 0 = {list.replicate p 1}

@[simp]

theorem ballot.counted_left_zero (q : ℕ) :

ballot.counted_sequence 0 q = {list.replicate q (-1)}

theorem ballot.mem_of_mem_counted_sequence {p q : ℕ} {l : list ℤ} (hl : l ∈ ballot.counted_sequence p q) {x : ℤ} (hx : x ∈ l) :

x = 1 ∨ x = -1

theorem ballot.length_of_mem_counted_sequence {p q : ℕ} {l : list ℤ} (hl : l ∈ ballot.counted_sequence p q) :

l.length = p + q

theorem ballot.counted_eq_nil_iff {p q : ℕ} {l : list ℤ} (hl : l ∈ ballot.counted_sequence p q) :

l = list.nil ↔ p = 0 ∧ q = 0

theorem ballot.counted_ne_nil_left {p q : ℕ} (hp : p ≠ 0) {l : list ℤ} (hl : l ∈ ballot.counted_sequence p q) :

theorem ballot.counted_ne_nil_right {p q : ℕ} (hq : q ≠ 0) {l : list ℤ} (hl : l ∈ ballot.counted_sequence p q) :

theorem ballot.counted_succ_succ (p q : ℕ) :

ballot.counted_sequence (p + 1) (q + 1) = list.cons 1 '' ballot.counted_sequence p (q + 1) ∪ list.cons (-1) '' ballot.counted_sequence (p + 1) q

theorem ballot.counted_sequence_finite (p q : ℕ) :

(ballot.counted_sequence p q).finite

theorem ballot.counted_sequence_nonempty (p q : ℕ) :

(ballot.counted_sequence p q).nonempty

theorem ballot.sum_of_mem_counted_sequence {p q : ℕ} {l : list ℤ} (hl : l ∈ ballot.counted_sequence p q) :

l.sum = ↑p - ↑q

theorem ballot.disjoint_bits (p q : ℕ) :

disjoint (list.cons 1 '' ballot.counted_sequence p (q + 1)) (list.cons (-1) '' ballot.counted_sequence (p + 1) q)

theorem ballot.count_counted_sequence (p q : ℕ) :

⇑measure_theory.measure.count (ballot.counted_sequence p q) = ↑((p + q).choose p)

theorem ballot.first_vote_pos (p q : ℕ) :

0 < p + q → ⇑(probability_theory.cond_count (ballot.counted_sequence p q)) {l : list ℤ | l.head = 1} = ↑p / (↑p + ↑q)

theorem ballot.head_mem_of_nonempty {α : Type u_1} [inhabited α] {l : list α} (hl : l ≠ list.nil) :

theorem ballot.first_vote_neg (p q : ℕ) (h : 0 < p + q) :

⇑(probability_theory.cond_count (ballot.counted_sequence p q)) {l : list ℤ | l.head = 1}ᶜ = ↑q / (↑p + ↑q)

theorem ballot.ballot_same (p : ℕ) :

⇑(probability_theory.cond_count (ballot.counted_sequence (p + 1) (p + 1))) ballot.stays_positive = 0

theorem ballot.ballot_edge (p : ℕ) :

⇑(probability_theory.cond_count (ballot.counted_sequence (p + 1) 0)) ballot.stays_positive = 1

theorem ballot.counted_sequence_int_pos_counted_succ_succ (p q : ℕ) :

ballot.counted_sequence (p + 1) (q + 1) ∩ {l : list ℤ | l.head = 1} = list.cons 1 '' ballot.counted_sequence p (q + 1)

theorem ballot.ballot_pos (p q : ℕ) :

⇑(probability_theory.cond_count (ballot.counted_sequence (p + 1) (q + 1) ∩ {l : list ℤ | l.head = 1})) ballot.stays_positive = ⇑(probability_theory.cond_count (ballot.counted_sequence p (q + 1))) ballot.stays_positive

theorem ballot.counted_sequence_int_neg_counted_succ_succ (p q : ℕ) :

ballot.counted_sequence (p + 1) (q + 1) ∩ {l : list ℤ | l.head = 1}ᶜ = list.cons (-1) '' ballot.counted_sequence (p + 1) q

theorem ballot.ballot_neg (p q : ℕ) (qp : q < p) :

⇑(probability_theory.cond_count (ballot.counted_sequence (p + 1) (q + 1) ∩ {l : list ℤ | l.head = 1}ᶜ)) ballot.stays_positive = ⇑(probability_theory.cond_count (ballot.counted_sequence (p + 1) q)) ballot.stays_positive

theorem ballot.ballot_problem' (q p : ℕ) :

q < p → (⇑(probability_theory.cond_count (ballot.counted_sequence p q)) ballot.stays_positive).to_real = (↑p - ↑q) / (↑p + ↑q)

theorem ballot.ballot_problem (q p : ℕ) :

q < p → ⇑(probability_theory.cond_count (ballot.counted_sequence p q)) ballot.stays_positive = (↑p - ↑q) / (↑p + ↑q)

The ballot problem.