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 #

Main result #

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

Equations
Instances For
    theorem Ballot.staysPositive_suffix {l₁ : List } {l₂ : List } (hl₂ : l₂ Ballot.staysPositive) (h : l₁ <:+ l₂) :

    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

      An alternative definition of countedSequence that uses List.Perm.

      theorem Ballot.mem_of_mem_countedSequence {p : } {q : } {l : List } (hl : l Ballot.countedSequence p q) {x : } (hx : x l) :
      x = 1 x = -1
      theorem Ballot.length_of_mem_countedSequence {p : } {q : } {l : List } (hl : l Ballot.countedSequence p q) :
      l.length = p + q
      theorem Ballot.counted_eq_nil_iff {p : } {q : } {l : List } (hl : l Ballot.countedSequence p q) :
      l = [] p = 0 q = 0
      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 []
      @[irreducible]
      theorem Ballot.sum_of_mem_countedSequence {p : } {q : } {l : List } (hl : l Ballot.countedSequence p q) :
      l.sum = p - 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.headI_mem_of_nonempty {α : Type u_1} [Inhabited α] {l : List α} :
      l []l.headI l
      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_problem' (q : ) (p : ) :
      q < p((ProbabilityTheory.condCount (Ballot.countedSequence p q)) Ballot.staysPositive).toReal = (p - q) / (p + q)
      theorem Ballot.ballot_problem (q : ) (p : ) :

      The ballot problem.