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

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.