PropositionStatement: 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.

Monotonicity and nonnegative homogeneity of the nonnegative integral

Statement

Let $f, g : X \to [0, + \infty]$ be measurable and let $c \geq 0$ .

If $f \leq g$ , then $\int f d μ \leq \int g d μ$ .
$\int c f d μ = c \int f d μ$ .

Facts & Assumptions

Given: Nonnegative measurable functions $f, g$ and a scalar $c \geq 0$ .

[L1]

The nonnegative integral is the supremum of simple minorants (The nonnegative Lebesgue integral).

[L2]

On simple functions, the nonnegative and simple integrals agree (The nonnegative integral agrees with the simple integral on simple functions).

Proof

technique · direct

1.1

If $f \leq g$ , every simple minorant of $f$ is also a simple minorant of $g$ . [L1, given] Taking suprema in [L1] gives $\int f d μ \leq \int g d μ$ .

1.2

If $c = 0$ , both sides are $0$ . Assume $c > 0$ . Multiplication by $c$ carries [L1, L2, given, algebra] simple minorants of $f$ bijectively onto simple minorants of $c f$ , and [L2] scales their integrals by the same factor. Taking suprema in [L1] yields $\int c f d μ = c \int f d μ$ .

2.1

Steps 1.1 and 1.2 prove the monotonicity and nonnegative homogeneity rules.

step 1.1step 1.2∎

Depends on

Used by

A nonnegative measurable function with finite integral is finite almost everywhere Corollary
Reverse Fatou's lemma under an integrable majorant Corollary
A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere Theorem
Absolute continuity of the integral Theorem
Chebyshev-Markov inequality for the integral Theorem
Dominated convergence Theorem
Fatou's lemma Theorem
Integrable simple functions are dense in L¹(μ) Theorem
Integrating against a density agrees with integrating the product Theorem
Monotone convergence for the integral Theorem
The Lebesgue integral is linear on L¹(μ) Theorem
The modulus of an integral is bounded by the integral of the modulus Theorem

Dependency tree · two levels

7 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

John K. Hunter, Measure Theory Notes, Proposition 4.5 (standard reference, not scraped)