Asymptotic statistics has an algebraic structure nobody was using. OP(1) is a commutative ring, oP(1) is an ideal inside it, and every “= … + oP(1)” in a statistics paper is an equality in the quotient ring. This library makes that literal, and machine-checks an M-estimator theorem with it.
van de Geer's Lemma 10.2.1 absorbs the remainder term into oP(1) at a point where √n(θ̂−θ₀) ∈ OP(1) is not yet available — it is precisely what the argument is deriving. The published proof reads:
0 = oP(n−1/2) + V(θ̂−θ₀) + o(|θ̂−θ₀|) + Pnψθ₀
and reads the conclusion off. Our own paper draft has the same step, phrased as “but θn − θ₀ ∈ I, so multiplying both sides by its norm”. Lean refused it.
The library does not patch the hole by assuming √n-consistency. It derives the rate: rewrite condition b as an exact factorisation √n Pψθ̂ = √n(θ̂−θ₀)·(V + u) with u ∈ oP(1), then observe that on the event |u| ≤ |V|/2 the factor is bounded away from zero. Conditions b and c alone suffice, as originally claimed.
The eight ring axioms are free — ℕ → Ω → ℝ is already a commutative ring in
Mathlib. What has to be proved is closure, and closure is exactly the familiar
calculus of stochastic order symbols.
Uniformly tight sequences of random variables, a subring of the ring of
all sequences. Membership is closed under +, ×, −.
Sequences converging to zero in probability. Additive closure is Slutsky; absorption A · I ⊆ I is what makes it an ideal rather than a mere subgroup.
Because Mathlib knows oP1 is an Ideal, the quotient is a
CommRing for free, and asymptotic equality becomes ordinary equality.
This is not a private definition. A sequence converging in distribution has
laws which, together with the limit, form a compact set in the space of probability
measures — so isTightMeasureSet_of_isCompact_closure applies and Prokhorov's
theorem hands back tightness. IsBigOP is therefore literally Mathlib's
IsTightMeasureSet, read along a sequence.
The one difference is the ∃ N. Tightness of a family asks for a single compact set carrying every measure at once; asymptotic tightness of a sequence only asks for it eventually. That quantifier is exactly what makes OP(1) closed under the ring operations, and it is the whole reason a ring exists here rather than merely a tight family.
measure_mono and measure_union_le hold
unconditionally. Every closure proof routes through one union-bound lemma,
meas_lt_norm_le_add, which turns a pointwise bound into a probabilistic one.Each rule textbooks state as a separate fact is one closure obligation of the algebraic structure. Nothing else needs proving — associativity, distributivity and the rest are inherited.
Split ε in half, bound each term past its own index, union bound.
Same shape with thresholds M₁M₂ instead of M₁+M₂.
Slutsky. Gives the additive subgroup.
The load-bearing one. Threshold δ/M on the small factor; this single law is what kills every remainder term downstream.
Take threshold 1. Puts the ideal inside the ring.
One line once the ideal exists: an ideal absorbs multiplication.
van de Geer's Lemma 10.2.1 in the scalar case. Select a step to see what it establishes and which algebraic law does the work. Two steps use absorption; that is the entire content of the “remainder is negligible” hand-wave.
Concentration theory delivers bounds of the shape “with probability at least 1−δ,
‖Xn‖ ≤ C(δ)·Rn”. Written as HasRate X R — that is,
membership in the ideal generated by R — combining them stops being fresh ε–δ work.
Two bounds add. One proof, reused forever.
Two bounds multiply — the step behind the product-rate condition.
Consistency falls out of any vanishing rate, with no argument repeated.
Filter by algebraic role, or search names and statements.
| Declaration | Statement | Role |
|---|
Every 2026 Lean statistics development works on a triangular array: the sample of
size n lives in Fin n → Ω under a product measure that changes with n. A ring
fixed to a single Ω cannot plug into that. So the ring was rebuilt over an arbitrary family
μ : ∀ n, Measure (α n) — same closure proofs, same subring, same ideal — and the
original library is recovered as the constant array.
The fixed-space library is definitionally the special case, so nothing is duplicated and nothing downstream breaks.
Their AsymptoticallyLinearAt unfolds to convergence in probability
of the linearisation residual over Measure.pi. That is exactly membership in
our ideal — so anything the calculus proves negligible discharges the field they currently
assume and document as “not proved here”.
A concentration theorem concludes “with probability at least 1−δ, the deviation is at most b(δ,n)”. Whenever that profile factors as C(δ)·Rₙ — which the √(log(1/δ)/n), √(d/n) and entropy-integral shapes all do — it is a rate, and the rest is ideal arithmetic.
The composite runs from the shape group 1 proves to the shape group 3 consumes, with our ideal arithmetic in between. Neither development is edited.
And the M-estimator argument itself now runs on arrays too, so the chain is complete: the same conditions a, b, c deliver the linearisation residual in the influence-function format the efficiency developments expect, with φ = −V⁻¹ψθ₀.
Taking α n = Fin n → Ω and μ n = Measure.pi (fun _ => P) is
literally their setting. What remains is to prove condition c from a chaining bound rather
than assume it — the one genuine mathematical gap left in the chain.
require today. Nothing
mathematical — only version skew. lean-rademacher pins Lean v4.27.0-rc1,
Lean-Asymptotic-Statistical-Theory pins v4.29.1, this library is on v4.34.0-rc1.
The bridges above are written so that once the toolchains agree, discharging them is an
exact.Formalised statistical learning theory arrived in force in 2026. Two groups built the finite-sample machinery; one built the asymptotic superstructure. None built the algebra in between, and none can currently state the conclusion that motivates the whole subject.
| Development | What it gives | OP/oP calculus | Ring / ideal |
|---|---|---|---|
| Sonoda et al.ITP 2026 · lean-rademacher · MIT | Rademacher complexity, symmetrization, McDiarmid, Dudley entropy integral, chaining, ℓ₁/ℓ₂ predictor bounds | none | none |
| Zhang, Lee, LiuarXiv 2602.02285 | Gaussian Lipschitz concentration, Dudley for sub-Gaussian processes, sparse least-squares at a sharp rate | none | none |
| Wei, Zheng, Fang, LuarXiv 2606.20642 · 154 files | LAN, Hájek–Le Cam convolution, Donsker via bracketing, semiparametric efficiency, Z-estimators, one-step estimators | ad-hoc Slutsky lemmas; oP appears only in docstrings | none |
| This libraryOpRing · MEstimator · Rates | Asymptotic linearity derived from conditions a, b, c; rate composition; adapters into all three | the calculus, proved once | Subring, Ideal, quotient |
Not “has not yet proved” — cannot express. High-probability bounds at fixed n have no vocabulary for a limit in distribution of a rescaled estimation error. That sentence is what applied statisticians and ML theorists actually quote, and getting to it from a concentration bound is exactly the oP/OP bookkeeping this library performs.
asympLinear_25_54 field is explicitly “not proved here” — and then derive
efficiency from it. That is precisely what this library produces.strong_law_ae_realhc; the only
hypothesis in the chain that is not yet a theorem somewhereA-module, keeping the scalar case