Existing in Mathlib · Measure theory and analysis

Dominated Convergence Theorem

If a sequence of almost-everywhere strongly measurable vector-valued functions converges almost everywhere and is almost everywhere bounded in norm by the same integrable envelope, then taking the limit and taking the integral commute.

almost-everywhere convergence
dominating functions
Bochner integration
limit interchange
strong measurability

Exact theorem

Exact Mathlib statement

theorem MeasureTheory.tendsto_integral_of_dominated_convergence {α G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {m : MeasurableSpace α} {μ : Measure α} {F : ℕ → α → G} {f : α → G} (bound : α → ℝ) (F_measurable : ∀ n, AEStronglyMeasurable (F n) μ) (bound_integrable : Integrable bound μ) (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ a ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))) : Filter.Tendsto (fun n => ∫ a, F n a ∂μ) Filter.atTop (𝓝 <| ∫ a, f a ∂μ)

The theorem at a glance

Dominated Convergence Theorem at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

An ivory analysis poster shows almost-everywhere strongly measurable functions whose norms are almost everywhere bounded by one integrable envelope, almost-everywhere pointwise convergence, and equality between the limit of integrals and the integral of the limit. — Almost-everywhere convergence plus one integrable dominator permits interchange of limit and Bochner integral.

Statement structure

Statement and scope

Read the exact Mathlib declaration

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

A sequence of varying function profiles remains inside one fixed integrable envelope and settles toward a limit while their accumulated areas converge. — One integrable envelope controls a pointwise-almost-everywhere limit strongly enough to pass the limit through the integral.

Why it matters

A mathematical landmark

The dominated convergence theorem is one of measure theory's central limit-interchange principles. It turns pointwise information plus one global integrable bound into convergence of integrals and supports large parts of modern analysis and probability.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

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.

Proof Atlas did not originate the dominated convergence theorem or Mathlib's declaration.
The selected declaration requires its exact measurability, domination, integrability, and almost-everywhere convergence hypotheses.
The generated explanation and visuals are not proof evidence.

Source and local evidence

Where the theorem comes from

Existing declaration: MeasureTheory.tendsto_integral_of_dominated_convergence in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.dominated-convergence-theorem.v001
Source: Open the pinned upstream reference