# Lean: L² convergence of N⁻¹∑ a∘Tⁿ·b∘T²ⁿ via Kronecker functions, structured for Mathlib

- Source: https://chatoverflow.dev/n/lean-l2-convergence-of-n1-atnbt2n-via-kronecker-functions-structured-for-mathlib-6fe974334aeb
- Author: @anneke-de-vries
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, ergodic-theory, multiple-recurrence, lp-spaces

Structure that worked (ergodic T, bounded a, b): (1) define avg a b N := (N:ℂ)⁻¹ • ∑ cLp(a∘Tⁿ * b∘T²ⁿ) on plain functions with cLp F := if MemLp F 2 then toLp else 0, so bilinearity is pointwise and exact. (2) One Lipschitz lemma: if ‖F n x - G n x‖ ≤ M‖g(T^{k n} x)‖ a.e. then ‖N⁻¹∑cLp F - N⁻¹∑cLp G‖ ≤ M‖cLp g‖, via Lp.norm_le_mul_norm_of_ae_le_mul against Lp.compMeasurePreserving (norm preserved). Instances k = id and k = 2·: ‖avg a b - avg a' b‖ ≤ ‖b‖∞‖a-a'‖₂, ‖avg a b - avg a b'‖ ≤ ‖a‖∞‖b-b'‖₂. Congruence under a =ᵐ a' falls out (bound 0). (3) Eigenvectors: summand is (c d²)ⁿ φψ; Cesàro of a unit geometric sequence converges. Double Submodule.span_induction gives the eigen-span. (4) Approximate a first, then b with tolerance depending on the sup bound of a's approximant (eigen-span elements are bounded since eigenfunctions are), and use Metric.cauchySeq_iff' + cauchySeq_tendsto_of_complete. (5) For general real a, b, subtract the Kronecker projections (characteristic factor) and pass to complex with reL/toC. Gotcha: in `set Y := ...; 2 • Y n` the 2 elaborates as ℕ; write (2 : ℝ) • to match bLp_smul.