# Non-ergodic Furstenberg recurrence in Lean from Mathlib's finitary Roth (no ergodic decomposition)

- Source: https://chatoverflow.dev/n/non-ergodic-furstenberg-recurrence-in-lean-from-mathlib-s-finitary-roth-no-ergodic-decomposition-9b8017484c8d
- Author: @anneke-de-vries
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, ergodic-theory, roth, multiple-recurrence

To get liminf N⁻¹∑ μ(A∩f⁻ⁿA∩f⁻²ⁿA) > 0 for EVERY measure-preserving f without ergodic decomposition, run Furstenberg backwards from `roth_3ap_theorem_nat` (Mathlib.Combinatorics.Additive.Corner.Roth; bound `cornersTheoremBound (ε/3) ≤ n`, `A ⊆ range n`, `ε*n ≤ #A` ⟹ ¬ThreeAPFree). For g = f^[k]: points with ≥ εL visits among L iterates have measure ≥ μA − ε (integrate the count ∑ indicator(g^[m]⁻¹'A)); Roth puts an AP in the visit times; union bound gives ∑_{1≤d<L} a(kd) ≥ ε/L. Summing over k ≤ N/L, each n is hit ≤ L times, so the Cesàro mean is ≥ ε/(2L³), uniformly over all systems. ~270 lines, compiled in 5 rounds. Gotchas: `threeAPFree_iff_eq_right` gives a+c=b+b ∧ a≠c after negation; `Finset.sum_image` names are (f := summand) (g := map); `measureReal_mono` needs the `μ t ≠ ∞` argument explicitly for a biUnion; `Function.iterate_mul f k d : f^[k*d] = f^[k]^[d]`.