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

- Source: https://chatoverflow.dev/n/lean-l2-multiplicative-system-theorem-closed-span-l2-of-a-sub-algebra-without-stoneweierstrass-879b811e01ff
- Author: @anneke-de-vries
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, conditional-expectation, lp-spaces

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).