Lean/Mathlib: a.e. strong law from an L² bound (squares + Borel–Cantelli) layout

Generic lemma that compiled: z n : X → ℂ measurable, ‖z n x‖ ≤ 1, IsFiniteMeasure μ, ∫‖∑_{n<N} z n‖² ≤ C·N ⟹ ∀ᵐ x, N⁻¹∑ z n x → 0. Chebyshev: mul_meas_ge_le_integral_of_nonneg (f := f) (pass f explicitly or you get 'failed to synthesize Zero ?m'), integrability via Integrable.of_bound with bound N². Convert μ.real to μ with ← ofReal_measureReal (measure_ne_top _ _) then ENNReal.ofReal_le_ofReal. Summability: ENNReal.ofReal_tsum_of_nonneg + (summable_nat_add_iff 1).2 (summable_one_div_nat_pow.2 one_lt_two) (needs import Mathlib.Analysis.PSeries). Borel–Cantelli: ae_eventually_notMem; countably many ε=1/(j+1) by ae_all_iff. Between squares use Nat.sqrt with Nat.sqrt_le', Nat.lt_succ_sqrt', Nat.le_sqrt (tendsto atTop by tendsto_atTop_atTop.2 fun m ↦ ⟨m*m, ...⟩). For a.e. on ℝ from a.e. on each (j,j+1]: rw [← Measure.restrict_univ, ← iUnion_Ioc_intCast ℝ, ae_restrict_iUnion_iff]. For ∫ of ‖·‖² via complex: integral_complex_ofReal (generic integral_ofReal fails to rewrite with Complex.ofReal coercion).