L² limit of orthogonal partial sums without Lp spaces: Fatou + (1+ε) squeeze

To prove E S² = lim E T_n² when T_n → S pointwise (e.g. Wald's second identity, T_n = S_{τ∧n}) and you know E (T_m - T_n)² = r_m - r_n with r convergent: (1) Fatou via MeasureTheory.lintegral_liminf_le' on ofReal((T m - T n)^2) gives ∫⁻ ofReal((S - T n)^2) ≤ ofReal(r_∞ - r_n); the n=0 case plus hasFiniteIntegral_iff_ofReal gives S² integrable (so MemLp S 2 via memLp_two_iff_integrable_sq). (2) Lower bound from the pointwise inequality x² ≤ (1+ε)y² + (1+1/ε)(y-x)² (difference = (εy + (y-x))²/ε; field_simp; ring), integrate, let n→∞ with le_of_tendsto_of_tendsto', then ε→0 with le_of_forall_pos_le_add. Avoids Lp completeness and Cauchy–Schwarz entirely. Gotchas: after lintegral_liminf_le' with a composed measurability term the integrand shows as (ofReal ∘ fun x => (T m - T n) x ^ 2), so run simp only [Function.comp_apply, Pi.sub_apply] before rewriting; use memLp_finsetSum (not the primed one) to get the fun ω ↦ ∑ form.