Measure theory and analysis · existing Mathlib declaration

Fatou's Lemma

For a sequence of measurable nonnegative extended-real functions, the integral of the pointwise lower limit cannot exceed the lower limit of the integrals.

Fatou's lemma
lower Lebesgue integral
limit inferior
extended nonnegative real functions
monotone convergence

The theorem at a glance

Fatou's Lemma — a one-sided lower-limit bound

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

Pointwise tail infima rise to the liminf, and their lower integrals give Fatou's one-sided bound. Generated explanation only; the exact HTML statement and pinned source are authoritative.

Detailed visual description

The poster keeps the original sequence visibly nonmonotone while gold pointwise tail-infimum profiles rise beneath it. The checked route rewrites liminf as a supremum of tail infima, passes that supremum through the lower integral, compares each tail floor with the tail integrals, and reconstructs the liminf.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

Nonnegative function curves form rising tailwise lower envelopes; the area under the liminf envelope is compared by one red less-than-or-equal sign with the limiting integral areas. — Tailwise lower envelopes expose Fatou’s integral inequality.

Complementary intuition

A mathematical landmark

Fatou's lemma is a foundational lower-semicontinuity principle for integration. It controls the integral of a pointwise lower limit without requiring the sequence itself to converge and is a standard gateway to stronger convergence theorems.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem MeasureTheory.lintegral_liminf_le {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) : ∫⁻ a, liminf (fun n => f n a) atTop ∂μ ≤ liminf (fun n => ∫⁻ a, f n a ∂μ) atTop

Selected evidence declaration text

theorem MeasureTheory.lintegral_liminf_le {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) : ∫⁻ a, liminf (fun n => f n a) atTop ∂μ ≤ liminf (fun n => ∫⁻ a, f n a ∂μ) atTop

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

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's Fatou lemma for a sequence of measurable functions f n : α → ℝ≥0∞. It compares the lower Lebesgue integral of the pointwise liminf with the liminf of the lower Lebesgue integrals. Nonnegativity is encoded by the extended nonnegative reals, and the declaration assumes neither convergence of the sequence nor finiteness of the integrals. It does not state equality, a reverse inequality, a signed- or Bochner-integral theorem, or a quantitative rate.

The selected declaration is one-sided: it does not assert equality or the reverse inequality.
It does not assume that the sequence converges, is monotone, or has finite integrals.
It is the ℝ≥0∞-valued lower-Lebesgue-integral form, not a signed- or Bochner-integral statement.
Proof Atlas did not originate Fatou's lemma or Mathlib's declaration.
The generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: MeasureTheory.lintegral_liminf_le in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.fatou-lemma.v001
Source handling: Verified upstream reference; no mirrored source package