Existing in Mathlib · Measure theory and analysis

Fubini's Theorem

When a function on a product space is integrable, its total integral can be computed by first integrating along one coordinate and then integrating the result along the other.

product measures
iterated integrals
Bochner integration
s-finite measures
integrability

Exact theorem

Exact Mathlib statement

theorem MeasureTheory.integral_prod {α β E : Type*} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E] [SFinite ν] [SFinite μ] (f : α × β → E) (hf : Integrable f (μ.prod ν)) : ∫ z, f z ∂μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ

The theorem at a glance

Fubini's Theorem at a glance

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

An ivory measure-theory poster compares one product-measure integral of f on α times β with an iterated integral first over β and then over α. — Product integration equals the selected iterated integration order for an integrable function on s-finite measure spaces.

Statement structure

Statement and scope

Read the exact Mathlib declaration

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

A continuous surface over a product grid is accumulated first along one family of slices and then across the remaining coordinate, matching one total product-space volume. — For an integrable function, product-space accumulation equals accumulation by successive coordinate slices.

Why it matters

A mathematical landmark

Fubini's theorem is the central bridge between integration on product spaces and repeated one-variable integration. It supports multivariable analysis, probability, partial differential equations, and almost every subject that uses product measures.

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 Fubini theorem for a Bochner-integrable real-normed-space-valued function on the product of two s-finite measure spaces. The selected equality integrates first in β with ν and then in α with μ. The declaration does not assume completeness; its substantive Fubini content is the complete-valued case, while Mathlib's Bochner integral is definitionally zero for incomplete codomains. It does not state Tonelli's theorem for nonnegative functions, remove integrability, or include the symmetric order in the same declaration.

Proof Atlas did not originate Fubini's theorem or Mathlib's declaration.
The selected declaration requires integrability on the product measure and records one order of iteration; the symmetric order is a companion theorem.
The generated explanation and visuals are not proof evidence.

Source and local evidence

Where the theorem comes from

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