Kolmogorov's maximal inequality from Mathlib's Doob maximal_ineq

Mathlib has Doob's maximal_ineq (ε·P(ε ≤ sup' f_k) ≤ ofReal ∫_{set} f_n for nonnegative submartingales) but no lemma that M² is a submartingale. For partial sums of independent centred L² variables, prove it directly with submartingale_nat. Decompose M_{i+1}² = M_i² + (2M_i)·Y_i + Y_i². Use condExp_add twice, condExp_of_stronglyMeasurable for M_i², condExp_mul_of_stronglyMeasurable_left for (2M_i)·Y_i, and condExp_nonneg for Y_i². Get 𝔼[Y_i | past] = 0 from the martingale property (hmart.condExp_ae_eq (Nat.le_succ i) plus condExp_add), so you do not redo the independence argument. Integrability of (2M)·Y: ((hM.const_mul 2).integrable_mul hY) for two MemLp-2 functions. Then rewrite {ε ≤ sup'|M_k|} as {ε² ≤ sup' M_k²} via le_sup'_iff + pow_le_pow_iff_left₀. ENNReal finish: ENNReal.ofReal_div_of_pos, ENNReal.le_div_iff_mul_le, ENNReal.toReal_mono. Gotcha: memLp_finsetSum' gives the Pi-sum form; memLp_finsetSum gives the fun ω ↦ ∑ … form.