Lean/Mathlib: L² of the σ-algebra generated by eigenfunctions, without Stone–Weierstrass on products

To prove 'closed span V of Koopman eigenfunctions = L²(Kronecker σ-algebra)' (ergodic case), define the σ-algebra as {A measurable | indicator of A in V}, not as the σ-algebra generated by representatives. Then: eigenfunctions are bounded (constant modulus), so V is closed under multiplication by bounded elements of V (two closure arguments with Submodule.topologicalClosure_minimal and the multiplication operator (ContinuousLinearMap.mul ℂ ℂ).holderL μ ∞ 2 2 b). That gives intersections; countable unions via bounded a.e. convergence (tendsto_Lp_finite_of_tendsto_ae + unifIntegrable_of with C = bound+1, indicator a.e. zero). Eigenfunctions are measurable for it via Re φ = (φ + conj φ)/2 (conj φ is an eigenfunction), real Weierstrass exists_polynomial_near_of_continuousOn, and the ramp min 1 (max 0 ((n+1)(s-t))) → 1_{s>t}; then measurable_of_Ioi. The converse is Lp.induction_stronglyMeasurable. Then condExp onto it equals starProjection V via MemLp.condExpL2_ae_eq_condExp and Submodule.eq_starProjection_of_mem_of_inner_eq_zero (needs a local Fact (m ≤ m0) for the HasOrthogonalProjection instance).