TheoremStatement: AI-adaptedProof: AI-generated

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) .$

Statement references

The Axiom of Countable Choice ( ${A C}_{ω}$ )

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)

[L5]

Two measures on $V$ agreeing on a generating pi-system with a common increasing finite-mass exhaustion from that system agree on all Borel sets (Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system).

[L6]

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

Proof

technique · direct

1.1L2L6given

On Borel subsets $E$ of $V$ define $ν (E) : = \int_{U} 1_{E} (T (x)) ∣ \det D T (x) ∣ d λ_{n} (x) .$ This is a measure: the nonnegative Jacobian weight is measurable, inverse images under $T$ take disjoint countable unions to disjoint countable unions, [L6] gives finite additivity, and [L2] passes the increasing finite sums through the integral.

2.1L1L2step 1.1

Let $W = V \cap R$ for a bounded open rectangle $R$ with rational endpoints. Write $d (y, W^{c})$ for Euclidean distance to the complement and $∥ y ∥_{\infty}$ for the maximum coordinate modulus. The functions $φ_{j} (y) = \min {1, \max (0, j d (y, W^{c}) - 1)} \min {1, \max (0, j + 1 - ∥ y ∥_{\infty})}$ are continuous, nonnegative and increase pointwise to $1_{W}$ . Each support is contained in the compact set ${d (y, W^{c}) \geq 1 / j, ∥ y ∥_{\infty} \leq j + 1} \subset W$ , so $φ_{j} ∣_{V}$ has compact support in $V$ . Applying [L1] to each $φ_{j}$ and [L2] to the two monotone limits gives $ν (W) = λ_{n} (W)$ . The empty $W$ is immediate.

3.1L5step 1.1step 2.1

The family $P = {\emptyset} \cup {V \cap R : R is a bounded open rectangle with rational endpoints}$ is nonempty and closed under binary intersections: an intersection is empty or again of the displayed rectangle form. It generates the Borel sigma-algebra of $V$ , since rational open rectangles form a Euclidean base. Both measures give $\emptyset$ mass zero, and step 2.1 proves agreement on every other member. The increasing members $P_{j} = V \cap (- j, j)^{n}$ cover $V$ and satisfy $λ_{n} (P_{j}) < \infty$ ; step 2.1 gives $ν (P_{j}) = λ_{n} (P_{j})$ . Hence [L5] makes $ν (E) = λ_{n} (E)$ for every Borel $E \subseteq V$ . This proves the set formula without assuming that an infinite-measure equality class is closed under decreasing intersections.

4.1L2L4step 3.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 3.1 and null-set invariance in [L4] then give the change-of-variables formula for $s$ .

5.1L2L3step 4.1∎

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

Depends on

Dependency tree · 2 levels

Sources

Gerald B. Folland, Real Analysis, 2nd ed., Theorem 2.47