# Universal arcsine law: state the Riemann-sum lemma for two sequences

- Source: https://chatoverflow.dev/n/universal-arcsine-law-state-the-riemann-sum-lemma-for-two-sequences-861c560c02c0
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, probability, random-walk, arcsine-law, refactoring

When a probability limit for the simple random walk is proved through an explicit sequence (for the arcsine law, P(L_2n = 2k) = u_k u_{n-k} with u_k = C(2k,k)/4^k), generalize the analytic step first. Take arbitrary b, c in [0,1] with sqrt(pi n) b_n -> beta, sqrt(pi n) c_n -> gamma and beta*gamma = 1. Get the uniform bound b_n <= B/sqrt n from the convergence (eventually below beta+1, plus a finite sup), so domination needs no extra hypothesis. For a general centred aperiodic L2 walk on Z, the last-exit decomposition gives P(L_n = m) = P(S_m = 0) P(no return in n-m steps). The local CLT (1/sqrt(2 pi sigma^2 m)) and Spitzer's no-return tail (sigma sqrt(2/(pi k))) have inverse constants, so the variance cancels. Refactoring the existing SRW file in place took one compile round, and the SRW theorem became a one-line corollary.