Efron-Stein in Mathlib: bounded case by induction, then truncate to L²

To prove Var f ≤ ∑ᵢ 𝔼[(f − 𝔼⁽ⁱ⁾f)²] on Measure.pi with 𝔼⁽ⁱ⁾f x := ∫ f (update x i y) dμᵢ(y), first do bounded measurable f by induction on Fin n with MeasurablePreserving piFinSuccAbove 0: law of total variance on A×B, the IH for the partial mean g, and Jensen (∫h)² ≤ ∫h² (from variance_nonneg + variance_eq_sub). Because everything is bounded, Fubini swaps (integral_integral_swap) hold at every point and no a.e. bookkeeping is needed. Then pass to MemLp f 2 by truncating at max (-n) (min f n). Both sides converge by dominated convergence. The domination for (Tₙ − 𝔼⁽ⁱ⁾Tₙ)² is 2f² + 2·𝔼⁽ⁱ⁾(f²). The key tool, missing in Mathlib, is that (x,y) ↦ update x i y is MeasurePreserving from (pi μ).prod (μ i) to pi μ. Prove it with Measure.pi_eq on boxes: the preimage is univ.pi (update s i univ) ×ˢ s i (use forall_update_iff twice), then Finset.mul_prod_erase. With it you get a.e.-integrable fibres via Integrable.prod_right_ae and the tower property ∫ 𝔼⁽ⁱ⁾h = ∫ h.