@[irreducible]

def ballotCount : ℕ → ℕ → ℕ

The combinatorial ballot count ballotCount a b: the number of ways to order a votes for candidate A and b votes for candidate B so that A strictly leads B throughout the counting. It is defined by the natural recurrence at the boundary between the +1 and -1 partial sums: zero when a = 0, one when b = 0 (any ordering of all-A votes is valid), and ballotCount a (b+1) + ballotCount (a+1) b when a > b.

@[simp]

theorem ballotCount_zero_left (b : ℕ) : ballotCount 0 b = 0

Boundary case: with zero votes for A, no valid sequence can have A strictly leading, so ballotCount 0 b = 0.

@[simp]

theorem ballotCount_succ_zero (a : ℕ) : ballotCount (a + 1) 0 = 1

Boundary case: with at least one A vote and no B votes, the unique ordering (all A's) keeps A in the lead, so ballotCount (a+1) 0 = 1.

theorem ballotCount_le {a b : ℕ} (h : a ≤ b) : ballotCount a b = 0

If A has at most as many votes as B (a ≤ b), then no ordering can keep A strictly ahead throughout, so ballotCount a b = 0.

def IsBallotSeq (a b : ℕ) (l : List ℤ) : Prop

A ballot sequence with a A-votes and b B-votes: a list of ±1s of length a + b containing exactly a ones and b negative ones. Each +1 represents a vote for candidate A, each -1 a vote for B.

noncomputable def favorableSequences (a b : ℕ) : Finset (List ℤ)

The set of favorable ballot sequences for the parameters a, b: all permutations of a list with a ones and b negative ones such that every non-empty prefix has strictly positive sum (i.e. candidate A is ahead at every intermediate counting step).

theorem ballotCount_eq_card_favorableSequences (a b : ℕ) (hab : a > b) : ballotCount a b = (favorableSequences a b).card

The recursively defined ballotCount a b agrees with the combinatorial count of favorable ballot sequences (permutations of a A-votes and b B-votes with all strictly positive prefix sums).

theorem ballot_theorem (a b : ℕ) (hab : a > b) : ballotCount a b * (a + b) = (a - b) * (a + b).choose a

Ballot Theorem (integer form). If candidate A receives a votes and candidate B receives b < a votes, then the number of vote orderings in which A is strictly ahead throughout the count, times the total number of votes, equals (a - b) times the number of orderings of the votes: ballotCount a b * (a + b) = (a - b) * C(a + b, a). This is the combinatorial content of the classical Bertrand ballot theorem (Durrett, Lecture 23).

theorem ballot_theorem_div (a b : ℕ) (hab : a > b) : ↑(ballotCount a b) / ↑((a + b).choose a) = (↑a - ↑b) / (↑a + ↑b)

Ballot Theorem (probability form). With a > b ≥ 0 votes for A and B, the probability that A is strictly ahead throughout the counting—the ratio of favorable orderings to all orderings—equals (a - b)/(a + b). This is the quotient version of ballot_theorem.