LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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 volume-preserving diffeomorphism preserves its induced Borel measure

Statement

Assume countable choice. Let $M$ be a Hausdorff second-countable smooth $n$ -manifold and let $η$ be a positive smooth density, with Borel coefficients as in Pointwise Borel nonnegative densities. Let $μ_{η}$ be the intrinsic chart-gluing Borel measure of Intrinsic density measure and its chart restriction. If $ϕ : M \to M$ is a $C^{1}$ diffeomorphism satisfying $ϕ^{*} η = η$ , then $μ_{η} (ϕ^{- 1} (E)) = μ_{η} (E)$ for every Borel set $E \subseteq M$ . The total measure may be infinite.

Facts & Assumptions

Given: Countable choice, a positive smooth density on a Hausdorff second-countable smooth manifold, and a $C^{1}$ diffeomorphism preserving that density.

[A1]

Adopt ${A C}_{ω}$ as stated in The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[F1]

Intrinsic density measure and its chart restriction: under ${A C}_{ω}$ , the positive density induces an intrinsic Borel measure, and in every chart the measure of a Borel subset is the Lebesgue integral of the chart coefficient of $η$ .

[F2]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: under ${A C}_{ω}$ , a $C^{1}$ diffeomorphism between open Euclidean sets transforms nonnegative Lebesgue integrals by its absolute Jacobian.

Proof

Given: [A1], [F1], and [F2].

1.1A1F1construct

Choose a countable chart cover $(U_{i}, x_{i})_{i \geq 1}$ , and replace it by the disjoint Borel partition $A_{i} = U_{i} ∖ ⋃_{k < i} U_{k}$ . Choose a countable chart cover $(V_{j}, y_{j})_{j \geq 1}$ for the target and form $B_{j} = V_{j} ∖ ⋃_{ℓ < j} V_{ℓ}$ . These are Borel partitions of $M$ . For fixed $i, j$ , the coordinate map $T_{j i} = y_{j} \circ ϕ \circ x_{i}^{- 1}$ is a $C^{1}$ diffeomorphism from the open set $x_{i} (U_{i} \cap ϕ^{- 1} (V_{j}))$ onto the open set $y_{j} (ϕ (U_{i}) \cap V_{j})$ . The pieces $S_{i j} = A_{i} \cap ϕ^{- 1} (B_{j} \cap E)$ are Borel subsets of its coordinate domain.

2.1A1F1F2step 1.1∎

By [F1] and countable additivity, $μ_{η} (ϕ^{- 1} E)$ is the sum over $i, j$ of the chart integrals of $η$ on $S_{i j}$ . The equality $ϕ^{*} η = η$ says in these charts that $η_{x_{i}} (u) = η_{y_{j}} (T_{j i} (u)) ∣ \det D T_{j i} (u) ∣$ . Applying [F2] to the indicator of $T_{j i} (x_{i} (S_{i j}))$ times the nonnegative coefficient $η_{y_{j}}$ makes each chart integral equal the integral of $η$ on $ϕ (S_{i j})$ . The latter sets, as $i$ varies for a fixed $j$ , partition $B_{j} \cap E$ because $ϕ$ is bijective; summing over $i, j$ therefore gives $μ_{η} (E)$ . All sums have nonnegative terms, so the argument also holds when either total is infinite.

Remarks

The coordinate comparison used in step 2.1 is the commuting square below. The proof uses its coordinate-map Jacobian through [F2]; the diagram is only an aid to locating that map.

S_{ij}\subseteq U_i \arrow[r,"\phi"] \arrow[d,"x_i"'] &
\phi(S_{ij})\subseteq V_j \arrow[d,"y_j"] \\
x_i(S_{ij}) \arrow[r,"y_j\circ\phi\circ x_i^{-1}"'] &
y_j(\phi(S_{ij}))

Depends on

Dependency tree · 2 levels

Sources

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