Grace/Cumulus/Combinatorics/BallotProbability.g17

Open in Workbench Download source

Imports

Ballot · Probability.Uniform

Declarations

• ballot.probability theorem derivation

Source

1-- The ballot problem as a probability: under the uniform distribution on2-- the orderings of a votes for A and b < a votes for B, A stays strictly3-- ahead throughout the count with probability (a − b)/(a + b).4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Combinatorics.BallotProbability10import Ballot11import Probability.Uniform1213-- Bertrand's ballot theorem, as a probability.14theorem ballot.probability (a b : Nat)15  requires lead : b < a16  shows prob(uniformWeight(orderings(a, b)), ballotSequences(a, b)) =17    (realNat(a - b):R) / (realNat(a + b):R)18proof19  have finite := orderings.finite at a, b20  have event := ballotSequences.subset_orderings at a, b21  have classical := prob.uniform with finite, event22  have count := ballot.count with lead23  have le : a ≤ a + b by arith24  have positive := choose.positive with le25  have nonzeroChoose : (a + b) choose a ≠ 026    intro zero27    rw zero at positive28    arith29  have nonzeroTotal : a + b ≠ 030    intro zero31    arith32  have realChoose := realNat.ne_zero with nonzeroChoose33  have realTotal := realNat.ne_zero with nonzeroTotal34  have cross : (realNat(a - b):R) * (realNat((a + b) choose a):R) =35      (realNat(a + b):R) * (realNat(cardinality(ballotSequences(a, b))):R)36    rw [← realNat.mul, ← realNat.mul, count]37    rfl38  rw [classical, realSize.value, realSize.value, orderings.count]39  exact realDiv.eq_of_cross with realChoose, realTotal, cross40