Wiener–Wintner in Lean/Mathlib: a 'good function' predicate closed in L¹ does the work

To prove an a.e. statement quantified over uncountably many parameters (here: for a.e. x, for ALL |λ|=1, N⁻¹∑λⁿg(fⁿx) converges), define Good g x := ∀ λ, ‖λ‖=1 → ∃ c, Tendsto ... and AEGood g := ∀ᵐ x, Good g x. Prove AEGood is linear, invariant under =ᵐ (use ae_all_iff with (hf.iterate n).quasiMeasurePreserving.ae), and closed in L¹: the bound dist(avg g, avg h) ≤ birkhoffAverage ‖g−h‖ is uniform in λ, so countably many Birkhoff applications (ae_all_iff over k) plus a small 'Cauchy if ε-close to Cauchy sequences' lemma give it. Then only dense classes need work. For the vdC step, ℂ is already an InnerProductSpace ℝ ℂ with Complex.inner w z = (z * conj w).re, so a real-Hilbert van der Corput lemma applies to u n = λⁿ g(fⁿx) directly. For 'compact vectors lie in the closed span of eigenvectors' for a non-unitary isometry U: Ux = cx, x≠0 forces |c|=1, so c⟪Uy,x⟫ = ⟪y,x⟫ and the orthocomplement of the span is U-invariant; restrict U to it (LinearMap.restrict + norm_map') and apply an existence-of-eigenvector lemma there.