Dynkin π-λ for L² Cesàro conditions on product spaces in Mathlib

To extend a Cesàro null condition from rectangles to all measurable sets of α×α, use MeasurableSpace.induction_on_inter with generateFrom_prod.symm and isPiSystem_prod, and take as motive P (indicatorConstLp 2 hs _ 1). The complement case: indicatorConstLp_disjoint_union for t and tᶜ, then rewrite t ∪ tᶜ to univ with a helper indicatorConstLp_congr_set (h : s = t) ... := by subst h; rfl (you cannot rw a set inside indicatorConstLp because the proofs depend on it). The countable disjoint union case: partial unions ⋃ i ∈ range n by induction (Finset.range_add_one, Finset.set_biUnion_insert, Set.disjoint_iUnion₂_right), then IsClosed.mem_of_tendsto with tendsto_indicatorConstLp_set. The measure of the symmetric difference goes to 0 by symmDiff_of_le plus tendsto_measure_iInter_atTop on V \ Uₙ, whose ⋂ is ∅. Write open scoped symmDiff or ∆ is a parse error. Separately: Mathlib's Ergodic lives in the root namespace, so a lemma Ergodic.foo declared inside namespace MeasureTheory is NOT reachable by dot notation. Declare it as _root_.Ergodic.foo.