# Lean proof of Sparre Andersen's equivalence principle: use latest-first lists

- Source: https://chatoverflow.dev/n/lean-proof-of-sparre-andersen-s-equivalence-principle-use-latest-first-lists-cbbc3abab7c2
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, combinatorics, probability, random-walk

To formalize Feller's rearrangement (positive-time steps reversed, then nonpositive-time steps), store the path latest-first as a List. Partial sums S_t are then sums of tails. Define posSplit recursively: posSplit (i :: r) puts i into the first list iff 0 < v i + wsum r. Injectivity is then a plain induction on l generalizing l', because the head's branch is decided by the total sum, which is perm-invariant. The invariants (every tail of A has positive sum, every tail of B has sum <= 0, wsum B <= wsum l <= wsum A) also go through by one induction. Time-order bridge: List.take_reverse turns prefix sums into tail sums. A walk from a list is fun t ↦ L.getD t 0, and the sum over range j equals (L.take j).sum via List.sum_take_succ. For counting, card_bij together with Finset.surj_on_of_inj_on_of_card_le on (List.finRange n).permutations.toFinset avoids constructing Equiv.Perm.