Claim evidence, explained
Last reviewed: April 30, 2026 · Lean mapping 2026-05-07
TheoremPath records exact mappings from governed claims to checked Lean theorem artifacts. The current formal layer covers selected probability, statistics, and learning-theory results, with broader public claims kept in source review until their Lean wrappers are present.
Lean-checked entries
56
TheoremPath declarations that compile in CI with zero recorded sorry/admit markers.
Formalized claims
28
Checked formal statements whose recorded scope matches the governed claim.
Dependency formalized
28
Checked supporting lemmas that do not by themselves prove the full public claim.
sorry / admit
0
Lean placeholders across these checked entries: sorry=0, admit=0.
A serious evidence record should be inspectable. This example shows the informal claim, the formal theorem, and the boundary of that mapping.
| Claim ID | claim:concentration-inequalities::markov-inequality |
|---|---|
| Informal claim | For a nonnegative random variable, tail probability is bounded by expectation divided by the threshold. |
| Formalized as | real-valued integrable Markov inequality with explicit nonnegativity, integrability, and positive-threshold assumptions |
| Lean declaration | TheoremPath.Probability.Concentration.markovInequalityRealIntegrable |
| Boundary | This Lean wrapper verifies the recorded real-valued Markov statement; broader concentration variants have separate claim records. |
Lean theorem statement
theorem markovInequalityRealIntegrable
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X : Ω → ℝ} {t : ℝ}
(hNonneg : 0 ≤ᵐ[μ] X) (hIntegrable : Integrable X μ) (ht : 0 < t) :
μ.real {ω | t ≤ X ω} ≤ (∫ ω, X ω ∂μ) / tReproducibility: from verification/lean, run lake build. The public counts are derived from the checked Lean mapping and require zero recorded sorry or admit.
Each card records the checked declaration, the theorem scope, and whether it formalizes the governed claim or only a dependency.
concentration inequalities
In plain English
A nonnegative random variable with small expectation cannot be large very often.
Role in the graph
This is the first tail-bound bridge from averages to probability guarantees.
Exact claim-facing mathlib wrapper for Markov's inequality in real-valued integrable form. The finite weighted-support theorem remains a bridge proof, not the canonical verification target.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
concentration inequalities
In plain English
A bounded finite sum has an exponential one-sided deviation bound under the recorded assumptions.
Role in the graph
This is the concentration step behind finite-class generalization arguments.
Exact claim-facing wrapper for the one-sided finite-sum Hoeffding bound for bounded independent real random variables.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
subgaussian random variables
In plain English
A bounded centered random variable has a sub-Gaussian moment-generating-function bound.
Role in the graph
This is the standard bridge from bounded variables to Hoeffding-style tails.
Exact mathlib wrapper for Hoeffding's lemma in sub-Gaussian MGF form. Source review now permits claim-level display without implying the whole page is Lean verified.
Checked April 29, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
measure theoretic probability
In plain English
If event probabilities are summable, the limsup event has probability zero in the mathlib formulation.
Role in the graph
This turns a previous finite bridge into a direct probability theorem wrapper.
Exact claim-facing mathlib wrapper for the first Borel-Cantelli lemma in limsup-measure-zero form. The finite union-bound artifacts remain supporting bridge proofs, not the source of verification.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
kolmogorov probability axioms
In plain English
The probability of a finite union is at most the sum of the individual probabilities.
Role in the graph
This is a foundational tool used throughout concentration and learning theory.
Exact claim-facing wrapper for the finite union bound for probability measures.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
common inequalities
In plain English
The absolute inner product is bounded by the product of the two norms.
Role in the graph
This is a reusable inequality across linear algebra, statistics, and optimization.
Exact claim-facing mathlib wrapper for the core Cauchy-Schwarz inequality in real inner product spaces. Equality, probability, and finite-sum variants remain separate explanatory scopes until governed separately.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
vc dimension
In plain English
A finite set family with bounded VC dimension cannot shatter too many subsets.
Role in the graph
This is a core combinatorial bridge behind classical learning-theory capacity bounds.
Exact claim-facing mathlib wrapper for the finite set-family Sauer-Shelah binomial-sum bound. The common (em/d)^d analytic estimate is treated as a downstream corollary, not as part of this verified claim.
Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
uniform convergence
In plain English
The checked artifact is a scoped reduction step toward the finite-class uniform convergence theorem.
Role in the graph
It is useful evidence, but it is deliberately not labeled as the full stochastic theorem.
Scoped bridge artifact for finite-class uniform convergence. It proves the risk-facing high-probability reduction from paired one-sided true-risk/empirical-risk deviation tail bounds and a delta-sized finite-class union-bound expression to a simultaneous epsilon-representative failure bound, and now includes fixed-hypothesis empirical-average upper- and lower-tail Hoeffding bridges with explicit sample-size hypotheses plus ENNReal adapters for the measure-valued union-bound layer; it does not verify iid sampling as the data-generating model or the closed-form sqrt/log sample-complexity display.
Checked April 30, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c
A diagnostic item can be mapped to the exact assumption or theorem it tests. The Hoeffding slice records separate links for independence, the boundedness-to-sub-Gaussian step, and the finite-class union-bound step.
These mappings are evidence for learner state. They are not public theorem badges, and they should be audited like any other claim-to-source or claim-to-Lean link.
For the rules behind this page, see methodology. For all 56 verified theorems, see the Lean verification dashboard. For the theorem list, see key theorems.