Random walks

Sums of i.i.d. steps as processes: the drift/oscillation dichotomy, limsup and liminf of partial sums, tail measurability of asymptotic events, the strong Markov property of i.i.d. sequences at stopping times, and ballot theorems.

• Drift and oscillation of random walks
• Random products in compact groups
• Return probabilities of random walks on Cayley graphs
• Strong Markov property of i.i.d. sequences

TheoremBertrand's ballot theorem#✓fully proved

Let \(p\) and \(q\) be natural numbers with \(1 \le q < p\). Call a sequence of \(p + q\) votes, each for A or for B, favourable if it contains exactly \(p\) votes for A and, for every \(k\) with \(1 \le k \le p + q\), strictly more of its first \(k\) votes are for A than for B. Then the number of favourable sequences, multiplied by \(p + q\), equals \((p - q)\binom{p+q}{q}\).

Equivalently, when the \(p + q\) votes are counted in uniformly random order, the probability that A is strictly ahead of B throughout the count is \(\frac{p-q}{p+q}\), since there are \(\binom{p+q}{q}\) sequences with exactly \(p\) votes for A.

theorem bertrand_ballot : ∀ (p q : ℕ), 1 ≤ q → q < p →
  (Finset.univ.filter (fun σ : Fin (p + q) → Bool =>
    (Finset.univ.filter (fun i : Fin (p + q) => σ i = true)).card = p ∧
    ∀ k : Fin (p + q),
      (Finset.univ.filter (fun i : Fin (p + q) => i ≤ k ∧ σ i = true)).card >
      (Finset.univ.filter (fun i : Fin (p + q) => i ≤ k ∧ σ i = false)).card)).card
  * (p + q) = (p - q) * (p + q).choose q

Sources

• Bertrand's ballot theorem, Wikipedia, https://en.wikipedia.org/wiki/Bertrand%27s_ballot_theorem.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.