CorollaryStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Reverse Fatou's lemma under an integrable majorant

Statement

Let $(f_{n})$ be nonnegative measurable functions and let $g$ be a nonnegative measurable function with $\int g d μ < + \infty$ and $f_{n} \leq g$ for every $n$ . Then ${lim sup}_{n \to \infty} \int f_{n} d μ \leq \int {lim sup}_{n \to \infty} f_{n} d μ .$

Facts & Assumptions

Given: Nonnegative measurable functions $f_{n}$ dominated by a nonnegative measurable function $g$ with finite integral.

[L1]

Fatou's lemma applies to every sequence of nonnegative measurable functions (Fatou's lemma).

[L2]

The nonnegative integral is additive (Additivity of the nonnegative Lebesgue integral).

[L3]

The nonnegative integral is monotone (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[L4]

Truncations of nonnegative measurable functions and pointwise limsups of measurable sequences are measurable (Closure properties of measurable functions used by the integral).

[L5]

Monotone convergence holds for the nonnegative integral (Monotone convergence for the integral).

Proof

technique · direct

1.1

For each $m \geq 1$ , put $g_{m} : = g \land m$ and $u_{n, m} : = f_{n} \land m$ . Then $g_{m}$ and $u_{n, m}$ are measurable, $0 \leq u_{n, m} \leq g_{m} \leq m$ , and $g_{m} - u_{n, m}$ is a nonnegative measurable function.

L4givenconstruct

2.1

Apply [L1] to the sequence $g_{m} - u_{n, m}$ . Since $g_{m}$ is finite-valued, ${lim inf}_{n} (g_{m} - u_{n, m}) = g_{m} - {lim sup}_{n} u_{n, m},$ $\int (g_{m} - u_{n, m}) d μ = \int g_{m} d μ - \int u_{n, m} d μ,$ and $\int (g_{m} - {lim sup}_{n} u_{n, m}) d μ = \int g_{m} d μ - \int {lim sup}_{n} u_{n, m} d μ .$ Rearranging Fatou's inequality therefore gives ${lim sup}_{n} \int u_{n, m} d μ \leq \int {lim sup}_{n} u_{n, m} d μ \leq \int {lim sup}_{n} f_{n} d μ .$

step 1.1L1L2L3L4algebra

3.1

Since $0 \leq f_{n} - u_{n, m} \leq g - g_{m}$ , [L2] and [L3] give $\int f_{n} d μ = \int u_{n, m} d μ + \int (f_{n} - u_{n, m}) d μ \leq \int u_{n, m} d μ + \int (g - g_{m}) d μ .$ Taking ${lim sup}_{n}$ and using step 2.1 yields ${lim sup}_{n} \int f_{n} d μ \leq \int {lim sup}_{n} f_{n} d μ + \int (g - g_{m}) d μ .$

step 2.1L2L3algebra

4.1

Because $g_{m} ↑ g$ , [L5] gives $\int g_{m} d μ ↑ \int g d μ$ . Applying [L2] to $g = (g - g_{m}) + g_{m}$ shows $\int (g - g_{m}) d μ = \int g d μ - \int g_{m} d μ ⟶ 0.$ Letting $m \to \infty$ in step 3.1 proves ${lim sup}_{n} \int f_{n} d μ \leq \int {lim sup}_{n} f_{n} d μ .$

step 3.1L2L5algebra∎

Depends on

Used by

Dominated convergence Theorem

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald B. Folland, Real Analysis, 2nd ed., §2.2 (standard reference, not scraped)