TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29

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 C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $U, V \subseteq R^{n}$ be open and let $T : U \to V$ be a $C^{1}$ diffeomorphism. For every nonnegative Lebesgue measurable $f : V \to [0, \infty]$ ,

\int_{V} f (y) d λ_{n} (y) = \int_{U} f (T (x)) ∣ \det D T (x) ∣ d λ_{n} (x) .

Facts & Assumptions

Given: The Axiom of Countable Choice, open sets $U, V \subseteq R^{n}$ , a $C^{1}$ diffeomorphism $T : U \to V$ , and a nonnegative Lebesgue measurable function $f : V \to [0, \infty]$ .

[L1]

The formula already holds for continuous compactly supported integrands. (The published Riemann change-of-variables theorem already gives the Lebesgue formula for continuous compactly supported integrands)

[L2]

Monotone convergence passes increasing limits through the integral. (Monotone convergence for the integral)

[L3]

Every nonnegative measurable function admits increasing simple approximations. (Every nonnegative measurable function admits an explicit increasing sequence of simple approximations)

[L4]

Assuming countable choice, Lebesgue measurable sets are Borel up to null sets, and $T$ preserves both null sets and Lebesgue measurability. ( $L (R^{n})$ is exactly the completion of the restriction of $λ_{n}$ to the Borel sets, A C^1 diffeomorphism maps Lebesgue null sets to Lebesgue null sets, A C^1 diffeomorphism maps Lebesgue measurable sets to Lebesgue measurable sets)

[A1]

The class of Borel sets $E \subseteq V$ for which $λ_{n} (E) = \int_{U} 1_{E} (T (x)) ∣ \det D T (x) ∣ d λ_{n} (x)$ is a monotone class containing the open rectangles of $V$ .

Proof

technique · direct

1.1

By [L1], the change-of-variables formula holds for continuous compactly supported functions. Approximating indicators of open rectangles from below by such functions and using [L2] shows that the set formula of [A1] holds for open rectangles. Because the class in [A1] is a monotone class, the monotone class theorem extends the set formula to all Borel sets in $V$ .

L1L2

2.1

Let $s = \sum_{j = 1}^{m} c_{j} 1_{E_{j}}$ be a nonnegative simple Lebesgue measurable function. By [L4], replace each $E_{j}$ by a Borel set differing from it only by a null set. The set formula from step 1.1 and null-set invariance in [L4] then give the change-of-variables formula for $s$ .

L2L4

3.1

Choose simple functions $s_{k} ↑ f$ by [L3]. Step 2.1 applies to each $s_{k}$ , and [L2] lets $k \to \infty$ on both sides. This yields the formula for $f$ .

L2L3step 2.1∎

Depends on

Used by

A C¹ diffeomorphism satisfies the change-of-variables formula for L¹ functions Corollary

Dependency tree · two levels

46 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., Theorem 2.47 (standard reference, not scraped)