The Ring of Uniform Tightness

A Lean 4 formalisation of the algebraic structure underlying the stochastic order symbols of asymptotic statistics, and an application to M-estimator asymptotics.

O_P(1) — the uniformly tight sequences of random variables — is a commutative ring. o_P(1) — the sequences converging to zero in probability — is an ideal inside it. Every "= … + o_P(1)" in a statistics paper is therefore an equality in the quotient ring O_P(1) ⧸ o_P(1), and the familiar calculus of order symbols is the closure conditions of that structure.

Overview and browsable index: https://meixide.github.io/tightness-ring/

Status: 6 files, ~1750 lines, zero sorry, axioms only propext, Classical.choice, Quot.sound. Builds against Mathlib master on Lean v4.34.0-rc1.

---

What the formalisation found

Formalising van de Geer's Empirical Process Theory (2022), Lemma 10.2.1 (asymptotic normality of M-estimators) showed that its proof is not self-contained.

The five-line proof absorbs the remainder o(|θ̂ₙ − θ₀|) into o_P(n^{-1/2}). The text reads

0 = o_P(n^{-1/2}) + V(θ̂ₙ − θ₀) + o(|θ̂ₙ − θ₀|) + Pₙψ_θ₀

and the conclusion is read off. That absorption needs √n(θ̂ₙ − θ₀) ∈ O_P(1), and conditions a, b, c do not supply it. Lean refuses the step.

The rate is not absent from the book: Lemma 10.4.1 establishes |θ̂ₙ − θ₀| = O_P(1/√n) from the optimality inequality Pₙ(γ_θ̂ₙ − γ_θ₀) ≤ 0 on the loss. But that argument belongs to the second, stronger condition set aa/bb/cc, and is unavailable from a/b/c, which work with the score ψ. So the precise finding is that Lemma 10.2.1 is not self-contained under its own hypotheses.

This library closes that, without importing the loss-based argument and without assuming √n-consistency. It derives the rate from a, b and c themselves: condition b is rewritten as an exact factorisation

√n Pψ_θ̂  =  √n(θ̂ₙ − θ₀) · (V + u),      u ∈ o_P(1)

and on the event |u| ≤ |V|/2 the second factor is bounded away from zero, so the first inherits tightness from the product (isBigOP_of_mul_add_littleOP). No division by a possibly-zero quantity is needed, and conditions b and c alone suffice, as originally claimed.

---

Layout

file	contents
TightnessRing/OpRing.lean	IsBigOP, IsLittleOP, the calculus rules, OP1 : Subring, oP1 : Ideal, the quotient bridge, rate ideals, properness and non-primality, tightness grounding via Prokhorov, weak LLN
TightnessRing/MEstimator.lean	empirical process, asymptotic linearity of M-estimators (scalar), the CLT hypothesis discharged from Mathlib's CLT, non-vacuity via the sample mean
TightnessRing/Rates.lean	HasRate — finite-sample bounds as ideal membership; composition (add, mul), collapse to o_P(1), ERM oracle inequality, the double-machine-learning product-rate theorem
TightnessRing/Interop.lean	the same ring and ideal over an arbitrary family μ : ∀ n, Measure (α n) (triangular arrays), plus adapters to and from other Lean developments
TightnessRing/MEstimatorArray.lean	the M-estimator theorem on triangular arrays, delivering the linearisation residual in influence-function format
TightnessRing/Equicontinuity.lean	condition c derived from an entropy bound on the shrinking class plus consistency; the M-estimator theorem with no assumed equicontinuity

Headline results

def OP1 (Ω) [MeasureSpace Ω] : Subring (ℕ → Ω → ℝ)          -- O_P(1) is a ring
def oP1 (Ω) [MeasureSpace Ω] : Ideal (OP1 Ω)                 -- o_P(1) is an ideal

theorem asympEq_iff_quotient_eq (X Y : OP1 Ω) :              -- asymptotic equality
    (X : ℕ → Ω → ℝ) ≃ₚ (Y : ℕ → Ω → ℝ) ↔                    -- is equality in A ⧸ I
      Ideal.Quotient.mk (oP1 Ω) X = Ideal.Quotient.mk (oP1 Ω) Y

theorem IsBigOP.of_tendstoInDistribution :                   -- grounded in Mathlib's
    TendstoInDistribution X atTop Z (fun _ => ℙ) μ' → IsBigOP X   -- IsTightMeasureSet

theorem m_estimator_asymptotically_linear … :                -- van de Geer 10.2.1,
    IsLittleOP (fun n ω => √n * (θ n ω - θ₀) + V⁻¹ * empProc Z (ψ θ₀) n ω)

theorem isLittleOP_sqrt_mul_of_product_rate … :              -- double machine learning
    IsLittleOP (fun n ω => √n * B n ω)

theorem isLittleOPA_of_modulusControlled                     -- condition c, derived
    (hdom : ∀ δ > 0, ∀ n x, ‖Δ n x‖ ≤ δ → ‖G n x‖ ≤ M δ n x)
    (hM : ModulusControlled μ M J) (hJ : EntropyVanishing J)
    (hcons : IsLittleOPA μ Δ) : IsLittleOPA μ G

---

Building

git clone https://github.com/meixide/tightness-ring
cd tightness-ring
lake exe cache get   # required on a fresh clone: fetches prebuilt Mathlib
lake build

lake exe cache get is not optional on a fresh clone. It downloads Mathlib's prebuilt .olean files (several GB, a few minutes on a good connection). Skipping it makes lake build compile Mathlib from source, which takes hours. If you are short on disk, note that the download plus the extracted library needs roughly 10 GB free.

The five modules of this library themselves compile in well under a minute once Mathlib is in place.

Continuous integration does the same thing automatically — .github/workflows/ci.yml uses leanprover/lean-action with use-mathlib-cache: true, so no cache step needs to be written by hand there.

Requires Lean v4.34.0-rc1 (see lean-toolchain). Mathlib is pinned in lake-manifest.json at 67c3e4f; lake exe cache get fetches exactly that revision, so builds are reproducible.

Depending on this library

require tightnessRing from git
  "https://github.com/meixide/tightness-ring" @ "main"

Your project must be on a Lean toolchain compatible with the one pinned here.

---

Relationship to other Lean developments

Statistical learning theory arrived in Lean in force during 2026. This library is complementary rather than competing: it supplies the asymptotic layer that the others do not have, and it is designed so that none of their code needs to change.

• Sonoda, Kasaura, Mizuno, Tsukamoto, Onda, Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral, ITP 2026 (arXiv:2503.19605, code, MIT). Finite-sample: Rademacher complexity, symmetrization, McDiarmid, chaining. TightnessRing.Interop's HasRateA.of_tailBound converts a bound of their shape into a rate.
• Zhang, Lee, Liu, Statistical learning theory in Lean 4: Empirical processes from scratch (arXiv:2602.02285). Gaussian Lipschitz concentration, Dudley for sub-Gaussian processes, sparse least squares. Also finite-sample.
• Wei, Zheng, Fang, Lu, Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory (arXiv:2606.20642, code). LAN, Hájek–Le Cam, semiparametric efficiency, Z-estimators. Their EfficientScoreEqAssumptions.asympLinear_25_54 field assumes asymptotic linearity — its docstring notes the empirical-process content is "not proved here". tendstoInProbArray_m_estimator proves exactly that predicate, with influence function −V⁻¹ψ_θ₀.

All three work on triangular arrays — the size-n sample lives in Fin n → Ω under a product measure varying with n. TightnessRing/Interop.lean therefore rebuilds the ring over an arbitrary μ : ∀ n, Measure (α n); the fixed-space library is recovered as the constant array (isBigOPA_const_space_iff).

A real cross-dependency is currently blocked only by toolchain skew: lean-rademacher pins v4.27.0-rc1, Lean-Asymptotic-Statistical-Theory pins v4.29.1, this library is on v4.34.0-rc1. The adapters are written so that once the versions agree, discharging them is an exact.

---

Open

• Condition c is no longer assumed. Equicontinuity.lean derives asymptotic equicontinuity from a controlled modulus of continuity over the shrinking ball (ModulusControlled) whose level vanishes with the radius (EntropyVanishing), together with consistency. What remains is to discharge ModulusControlled itself from lean-rademacher's dudley_entropy_integral_abs — the shapes match (√n · R_n ≲ 12 ∫₀^{c δ} √(log N(x)) dx, with the envelope c δ → 0), so this is a dependency question rather than a mathematical one.
• Vector parameters: ℝᵖ as an O_P(1)-module.
• Mathlib-conformant naming, and a filter-general form of the definitions, prior to proposing any of this upstream.

---

Provenance

The Lean development in this repository was written with substantial assistance from an AI coding assistant (Claude). The author has reviewed every definition and proof and takes full responsibility for the mathematical content and design choices. This is disclosed in line with the Mathlib contribution guidelines on AI-assisted contributions.

Citation

The underlying mathematics is The Ring of Uniform Tightness, C. García Meixide (2025). A preprint describing the formalisation is in preparation; until then, please cite this repository.