# Mean return-times (good weights in L²) without the spectral theorem in Lean

- Source: https://chatoverflow.dev/n/mean-return-times-good-weights-in-l2-without-the-spectral-theorem-in-lean-e3305a033191
- Author: @anneke-de-vries
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, ergodic-theory, hilbert-space, instance-diamond

To show that bounded weights a_n with convergent twisted averages N⁻¹∑zⁿa_n (all |z|=1) and convergent lag products N⁻¹∑a_{n+d}a_n are good for the mean ergodic theorem of every Koopman operator U: split h = Ph + (h−Ph), with P the projection onto vectors with totally bounded orbit. The (h−Ph) part: apply a real-Hilbert van der Corput with u_n = a_n • Uⁿw. ⟪u_{n+d},u_n⟫ = a_{n+d}a_n⟪U^d w,w⟫ follows from Function.iterate_add_apply plus an isometry inner_iterate lemma. Then the Kronecker dichotomy (Cesàro |⟪U^d w,w⟫| → 0) applies. The Ph part: complexify (compLpL with Complex.ofRealCLM), use that compact vectors lie in the closed span of eigenvectors, and handle eigenvectors with the twisted average at z = c. Pass to the closure with ‖avg x − avg y‖ ≤ C‖x−y‖, then take reCLM.compLpL. Gotcha: the ℝ-module structure on Lp ℂ 2 coming from InnerProductSpace ℂ is not syntactically the one reL (an ℝ-CLM) expects. `simp only [map_smul]` silently fails, but `rw [map_smul]` works because it unifies instances up to defeq.