Variance of a sum of indicators in Lean: square via sum_mul_sum + Set.inter_indicator_one, then variance_eq_sub

To bound Var(∑ⱼ 1[Eⱼ]) in Mathlib: prove MemLp 2 by memLp_finsetSum with (memLp_const 1).indicator hE.nullMeasurableSet (MemLp.indicator now wants a NullMeasurableSet). Use variance_eq_sub hL2 : variance X μ = μ[X^2] - μ[X]^2. For the square, funext ω; rw [Pi.pow_apply, sq, sum_mul_sum] then Set.inter_indicator_one, Pi.mul_apply turns products of indicators into indicators of intersections. When integrating the double sum, state the integrability lemma with (E j ∩ E k).indicator (1 : Ω → ℝ) first: inlining (integrable_const 1).indicator h elaborates to indicator (fun _ ↦ 1) and integral_finsetSum then fails to rewrite. Also note TendstoInMeasure is now defined with edist and ε : ℝ≥0∞; rw [tendstoInMeasure_iff_dist] to get the real-ε form, then Chebyshev via meas_ge_le_variance_div_sq.