TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)

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.

Monotone convergence for the integral

Statement

Let $0 \leq f_{1} \leq f_{2} \leq \dots$ be measurable and suppose $f_{n} (x) ↑ f (x)$ for every $x$ . Then $\int f_{n} d μ ↑ \int f d μ .$

Facts & Assumptions

Given: A nondecreasing sequence $(f_{n})$ of nonnegative measurable functions with pointwise limit $f$ .

[L1]

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

[L2]

For a nonnegative simple function $s$ , the set function $A \mapsto \int_{A} s d μ$ is a measure (The indefinite integral of a nonnegative simple function is a measure).

[L3]

Measures are continuous from below on increasing measurable sets (Continuity from below for measures).

[L4]

The nonnegative integral agrees with the simple integral on simple functions, and the latter is homogeneous on nonnegative simple functions (The nonnegative integral agrees with the simple integral on simple functions, The simple integral is monotone, homogeneous, and additive).

Proof

technique · direct

1.1givenL1

By [L1], the integrals $\int f_{n} d μ$ increase and are bounded above by $\int f d μ$ . Write $L = \sup_{n} \int f_{n} d μ$ , so $L \leq \int f d μ$ in $[0, + \infty]$ .

1.2givenL2L3

Fix a finite-valued nonnegative simple function $s \leq f$ and $0 < c < 1$ . Set $A_{n} = {f_{n} \geq c s}$ . The sets $A_{n}$ increase to $X$ : where $s = 0$ membership is automatic, and where $s > 0$ , the limit $f \geq s > c s$ eventually forces $f_{n} \geq c s$ . Since $A \mapsto \int_{A} s d μ$ is a measure [L2], continuity from below [L3] gives $\int_{A_{n}} s d μ ↑ \int s d μ$ .

2.1step 1.2L1L4algebra

On $A_{n}$ , $c s \leq f_{n}$ , hence $c s χ_{A_{n}} \leq f_{n}$ everywhere. By monotonicity [L1] and simple-integral agreement and homogeneity [L4], $c \int_{A_{n}} s d μ \leq \int f_{n} d μ \leq L$ . Letting $n \to \infty$ in step 1.2 yields $c \int s d μ \leq L$ . Letting a fixed sequence $c_{m} ↑ 1$ shows $\int s d μ \leq L$ , also when the simple integral is infinite.

3.1step 1.1step 2.1∎

The inequality from step 2.1 holds for every admissible simple minorant $s \leq f$ . Taking their supremum, as in The nonnegative Lebesgue integral, gives $\int f d μ \leq L$ . Combine this with step 1.1 to obtain $\int f_{n} d μ ↑ \int f d μ$ .

Depends on

Used by

A C¹ diffeomorphism satisfies the change-of-variables formula for L¹ functions Corollary
Additivity of the nonnegative Lebesgue integral Corollary
Almost-everywhere monotone convergence Corollary
Beppo Levi's theorem for nonnegative series Corollary
Brownian paths have infinite total variation Corollary
Distribution of a one-sided Brownian hitting time Corollary
Dominated convergence is a Vitali corollary Corollary
Expected duration of symmetric gambler's ruin Corollary
Finite propagation for scalar conservation laws Corollary
Global L¹ contraction from the local estimate Corollary
Law of the Brownian maximum Corollary
Polar integration may discard the cut locus Corollary
Reverse Fatou's lemma under an integrable majorant Corollary
Uniqueness, comparison and order preservation of entropy solutions Corollary
Unitary groups converge under strong resolvent convergence Corollary
Vector Levy characterization Corollary
Wald first equation under integrable stopping Corollary
A BMO function need not be globally integrable Counterexample
A decreasing sequence need not satisfy a monotone convergence theorem without an integrable start Counterexample
A limit of discrete series is not square-integrable Counterexample
A nonintegrable observable with divergent ergodic averages Counterexample
A radial Poisson limit does not control a tangential path Counterexample
A random variable need not have a finite expectation Counterexample
An unbounded predictable transform may lose integrability Counterexample
An unbounded stopped exponential martingale needs uniform integrability Counterexample
Hilbert transform is not strong type (1,1) Counterexample
Iid strong law fails at infinite absolute mean Counterexample
Infinite variance can defeat square-root-n CLT scaling Counterexample
Integrable stopping time alone does not suffice for arbitrary martingale increments Counterexample
Subcritical W^1,p is not closed under multiplication Counterexample
Taking out an unbounded factor needs integrability Counterexample
The sine integral is improperly Riemann integrable and not Lebesgue integrable Counterexample
Continuous covariant model and measurable completion Definition
Green kernel of a transient chain Definition
Invariant and stationary distribution for a Markov kernel Definition
The one-dimensional torus and its normalized Haar integral Definition
A Brownian hitting time has infinite mean Example
A Dirac mass has precisely sufficiently negative Sobolev order Example
A square-integrable discrete-series matrix coefficient Example
An explicit ∂̄ solution with an L² estimate Example

…and 182 more results.

Dependency tree · two levels

17 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

Richard F. Bass, Real Analysis for Graduate Students, Theorem 7.1 (standard reference, not scraped)
John K. Hunter, Measure Theory Notes, Theorem 4.6 (standard reference, not scraped)
Gerald B. Folland, Real Analysis, 2nd ed., Theorem 2.14 (standard reference, not scraped)