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

A nonnegative integral over a null set vanishes

Statement

Let $f : X \to [0, + \infty]$ be measurable and let $E$ be measurable with $μ (E) = 0$ . Then $\int_{E} f d μ = 0.$

Facts & Assumptions

Given: A nonnegative measurable function $f$ and a measurable null set $E$ .

[L1]

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

[L2]

The integral over a measurable set is defined by $\int_{E} f d μ = \int f χ_{E} d μ$ (Integral over a measurable subset).

[L3]

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

Proof

technique · direct

1.1L1L2given

Let $s = \sum_{j} c_{j} χ_{A_{j}}$ be a nonnegative simple minorant of $f χ_{E}$ , with $c_{j} \geq 0$ . If $c_{j} > 0$ , then $A_{j} \subseteq E$ because $s = 0$ outside $E$ ; hence $μ (A_{j}) = 0$ . The simple-integral formula, equivalently the finite-sum calculation in [L1], gives $\int s d μ = \sum_{j} c_{j} μ (A_{j}) = 0$ , including when the original representation overlaps.

2.1step 1.1L2L3∎

Taking the supremum over all such simple minorants in [L3] gives $\int_{E} f d μ = \int f χ_{E} d μ = 0$ .

Depends on

Used by

A C¹ diffeomorphism satisfies the change-of-variables formula for L¹ functions Corollary
Almost-everywhere monotone convergence Corollary
Polar integration may discard the cut locus Corollary
The obstacle reaction is supported on the contact set under measure regularity Corollary
A step has no locally integrable weak derivative Counterexample
An absolutely continuous finite measure can have an unbounded Radon-Nikodym derivative Counterexample
Lp and Sobolev classes do not determine point values Counterexample
Null-set modifications defeat everywhere representative recovery Counterexample
The complementarity product needs extra regularity Counterexample
Two Radon-Nikodym derivatives can differ on a null set Counterexample
x⁻¹dλ on (0,1) shows finiteness is needed in the epsilon-delta criterion Counterexample
Discrete martingale transform Definition
The standard intertwining operator A(nu) Definition
A boundary atom gives an h1 function without an L1 density Example
A piecewise-quadratic distribution function recovers its density Example
Projective-plane curvature via a hemisphere Example
The absolute value has a weak first derivative Example
The chain rule for Radon-Nikodym derivatives on [0,1] Example
The one-dimensional obstacle reaction is supported on the contact set Example
The positive-type Gaussian on the real line and its cyclic model Example
Weighted interval volume Example
FALSE: absolutely continuous measures always have bounded Radon-Nikodym derivatives False statement
FALSE: the epsilon-delta condition characterises absolute continuity for every measure False statement
FALSE: the Radon-Nikodym derivative is a uniquely determined function False statement
Agreement of Borel overlap integrals Lemma
Bounded compact data give an everywhere finite Newtonian potential Lemma
Continuous lattice-periodic functions are determined by their lattice Fourier coefficients Lemma
K-type eigenvalues of A(nu): recurrence, closed form and nonvanishing Lemma
Orthogonality of the lattice characters over a fundamental domain Lemma
Conditional expectation exists by radon nikodym Theorem
Conditional monotone convergence Theorem
Cut locus of a point has riemannian volume zero Theorem
Dominated convergence Theorem
Every sigma-finite signed measure admits a Lebesgue decomposition relative to a sigma-finite positive measure Theorem
Hardy–Littlewood–Sobolev fractional integration inequality Theorem
Holder's inequality for integrals, including the endpoint cases Theorem
Lower semicontinuity of logarithmic potential and energy Theorem
Measurable essentially bounded operator fields act decomposably Theorem
Measurable integration extends smooth density integration Theorem
Newtonian potentials solve the distributional Poisson equation Theorem

…and 2 more results.

Dependency tree · two levels

12 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, Proposition 6.3(4) (standard reference, not scraped)