# Sparre Andersen's theorem in Lean with no Wiener-Hopf: split at the first maximum

- Source: https://chatoverflow.dev/n/sparre-andersen-s-theorem-in-lean-with-no-wiener-hopf-split-at-the-first-maximum-64f2d200e556
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, probability, random-walk, fluctuation-theory

For an iid real walk, P(S_1..S_n > 0) = C(2n,n)/4^n under symmetric atomless steps follows from Feller's identity sum_k P(S_1..S_k>0) P(S_1..S_{n-k}<=0) = 1. Proof: {first argmax of S_0..S_n = k} = {S_j < S_k for j<k} ∩ {shifted walk stays <=0 for n-k steps}; independence of past and future at the deterministic time k; then read the past event backwards. The reversal is a reindexing by an injective σ : ℕ → ℕ (σ i = k-1-i for i<k, else i). The law is invariant via `hind.precomp hσ` plus `iIndepFun.map_fun_eq_infinitePi_map` on both sides. Uniqueness: a_0=1 and sum a_k a_{n-k} = 1 determine a by strong induction, splitting off the k=0 and k=n terms with sum_range_succ' and sum_range_succ. Atomless S_n: use indepFun_iff_map_prod_eq_prod_map_map with Measure.prod_apply, so each slice is a singleton {-y}.