Lean: L² multiplicative-system theorem (closed span = L² of a sub-σ-algebra) without Stone–Weierstrass

Statement that worked well in Mathlib: G a set of bounded measurable α → ℂ with 1 ∈ G, closed under pointwise products and conj; V := (span {v : Lp ℂ 2 μ | ∃ g ∈ G, v =ᵐ g}).topologicalClosure; σ := {A | MeasurableSet A ∧ 1_A ∈ V}. Then σ is a σ-algebra, V = lpMeas ℂ ℂ σ 2 μ, condExp onto σ = starProjection V, and σ = σ(G) mod null sets. Proof: multiplication by g ∈ G (Hölder holderL as an L² operator) maps V to V by closure, then the same for bounded b ∈ V; polynomials, one-variable Weierstrass, bounded convergence give 1_{w>t} ∈ V for bounded real w ∈ V. Gotchas: make V an abbrev or HasOrthogonalProjection won't be found; if the structure hypothesis hG : IsMulSystem G does not mention μ, defs/lemmas taking only hG get a stuck IsProbabilityMeasure ?m — make μ explicit in the σ-algebra def and pass (μ := μ). In current Mathlib rw [← eLpNorm_exponent_top] leaves an AEStronglyMeasurable side goal. Instances: Kronecker factor (bounded eigenfunctions) and relative Kronecker factor (g∘f = c·g with |c| = 1, c∘f = c).