# An exact L-squared tail on a finite law [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-lp-convergence/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-lp-convergence-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Compute the second error moment and give a tail for any tolerance. Fix p=2; no other mode is inferred from a finite prefix. ## Givens and symbols - work - G1 — Omega={a,b} has masses 1/4,3/4; X(a)=1, X(b)=-1; for every n≥1, X_n(a)=1+2/(n+1), X_n(b)=-1-1/(n+1). - p — fixed exponent2 - η — moment tolerance - ε — norm tolerance ## Rules and sources - mko_definition · cited — This slice uses positive integer p, a complete finite atomic law and symbolic error amplitudes c_i/(n+s). Compute exact p-moments and epsilon tail bounds. A finite prefix is insufficient; unrestricted almost-sure, other-Lq or reverse probability-mode implications are not inferred without their additional theorem assumptions. · mko-lp-convergence - work · prerequisite — Finite-law p-moments sum weighted absolute pth powers; the L2 norm is the square root of the second moment; L2 convergence means the L2 error norm tends to zero; floor(u)+1>u. ## Main derivation S01 · impliesBefore p=2,\quad1/4+3/4=1 After X_n,X\in L^2(\Omega,P)\quad(n\ge1) Conditions: none Rule: work · Uses: G1, work Leaf basis: work Finite rational values on one space ensure each second moment exists. S02 · impliesBefore X_n-X After (2/(n+1),-1/(n+1)) Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work Compute signed errors atom by atom first. S03 · impliesBefore |X_n-X|^2 After (4/(n+1)^2,1/(n+1)^2) Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work Absolute squares make both terms nonnegative. S04 · impliesBefore E|X_n-X|^2 After \frac14\frac4{(n+1)^2}+\frac34\frac1{(n+1)^2}=\frac7{4(n+1)^2} Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work Use the original masses for the exact second error moment. S05 · impliesBefore \|X_n-X\|_2^2=7/[4(n+1)^2] After \|X_n-X\|_2=\sqrt7/[2(n+1)] Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work The L2 norm is the square root of the second moment, not that moment itself. S06 · impliesBefore \eta>0,\quad N=\lfloor7/(4\eta)\rfloor+1 After n\ge N\implies\frac7{4(n+1)^2}\le\frac7{4(n+1)}<\eta Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work A looser rational bound still yields an explicit universal tail. S07 · impliesBefore \eta=\varepsilon^2\quad(\varepsilon>0) After n\ge N(\varepsilon^2)\implies\|X_n-X\|_2<\varepsilon Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work Controlling the moment by epsilon squared controls the norm. S08 · impliesBefore \forall\varepsilon>0\ \exists N\ \forall n\ge N:\|X_n-X\|_2<\varepsilon After X_n\to X\text{ in }L^2 Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work The full quantifiers prove L2 convergence, not a finite moment list. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — No general cross-mode theorem is inferred from this calculation. - S07 · premise_audit · G1, S06, work — Keep norm tolerance distinct from moment tolerance. - S06 · premise_audit · G1, S05, work — The comparison of denominators uses n+1≥1. - S05 · premise_audit · G1, S04, work — The denominator simplifies because n+1 is positive. - S04 · premise_audit · G1, S03, work — The weighted constant is 7/4, not 4+1. - S03 · premise_audit · G1, S02, work — The denominator must be squared too. - S02 · premise_audit · G1, S01, work — Do not cancel b's negative error against a before squaring. - S01 · premise_audit · G1, work — The positive integer p=2 is fixed across n. ## Error controls and negative controls WeightsThe weighted constant is(1/4)4+(3/4)1=7/4. Two tolerancesSet the moment tolerance to epsilon squared before concluding norm