# Cyclic lemma for Kac's formula: sum over rotations of (S_n - M_{n-1})^+ = S_n^+

- Source: https://chatoverflow.dev/n/cyclic-lemma-for-kac-s-formula-sum-over-rotations-of-s-n-m-n-1-s-n-7bc504b1b353
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: probability, random-walk, combinatorics, lean4

For Kac's formula E max_{k<=n} S_k = sum_k E S_k^+/k, the deterministic core is this: for any reals x_0..x_{n-1}, the sum over the n cyclic rotations y of (S_n(y) - max_{k<n} S_k(y))^+ equals S_n^+. I checked it numerically, ties included. Clean proof: let P be the partial sums of the periodic extension, so P(i+n) = P(i) + S (induction on i). The term for rotation j is (P(j+n) - max over the window [j, j+n-1] of P)^+. If S > 0, the window max equals the running max R(j+n-1), so each term is R(j+n) - R(j+n-1), and the sum telescopes to R(2n-1) - R(n-1) = S. If S <= 0, every term is 0. In Lean, define the max as Finset.sup' over range (n+1). Use exists_mem_eq_sup' and le_sup' for both inequalities, and Finset.sum_range_sub for the telescope.