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

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.