Lean verification record
Checked Artifact: Dominated Convergence Theorem (mathlib)
Proof Atlas collected build, no-sorry, axiom, and clean-source evidence directly from the pinned upstream declaration.
Verification result
The recorded Lean checks passed
- Build replaypassed with retained transcript
- Unfinished stepsNone found
- Source identityPinned commit and file recorded
- Dependency profileAxiom closure recorded
Reproducibility details
What the checker recorded
- Declaration checked
MeasureTheory.tendsto_integral_of_dominated_convergence- Module
Mathlib.MeasureTheory.Integral.DominatedConvergence- Source file checked
Mathlib/MeasureTheory/Integral/DominatedConvergence.lean- Package commit
5e932f97dd25535344f80f9dd8da3aab83df0fe6- Build transcript
- passed · retained with this record
- Unfinished proof steps
- None found by the recorded no-sorry scan
- Axiom closure
- Classical.choice, Quot.sound, propext
- Collection provenance
- Clean source state recorded
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Evidence boundary
Exact formal statement only
This page indexes Mathlib's sequential dominated-convergence theorem for Bochner integrals of real-normed-space-valued functions. It assumes almost-everywhere strong measurability of every term, one integrable real-valued bound dominating every norm almost everywhere, and almost-everywhere pointwise convergence. The declaration does not assume completeness; its substantive dominated-convergence content is the complete-valued case, while Mathlib's Bochner integral is definitionally zero for incomplete codomains. It does not state monotone convergence, uniform convergence, pointwise-everywhere convergence, or a quantitative rate.
This checker record does not establish novelty, transfer a historical acceptance decision, or authorize publication.