TheoremStatement: AI-adaptedProof: Literature-sourcedprecheck passaudited 2026-08-11

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.

Change of variables for an injective $C^{1}$ map on a compact Jordan set

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, let $g : U \to R^{n}$ be injective and $C^{1}$ , and suppose $D g (x)$ is invertible for every $x \in U$ . Let $K \subseteq U$ be compact and Jordan measurable. For a bounded function $f : g (K) \to R$ , the following are equivalent:

$f$ is Riemann integrable on $g (K)$ ;
$x \mapsto f (g (x)) ∣ \det D g (x) ∣$ is Riemann integrable on $K$ .

When either condition holds, $\int_{g (K)} f (y) d y = \int_{K} f (g (x)) ∣ \det D g (x) ∣ d x .$

Facts & Assumptions

Given: The map $g$ , compact Jordan set $K$ , and bounded $f$ in the statement.

[L1]

For each fixed $n \geq 1$ , the function $\det : M_{n} (R) \to R$ is evaluation of a polynomial in the $n^{2}$ matrix-entry variables (For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries), and componentwise continuity gives continuity of maps assembled from finitely many continuous components (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[L2]

Local $C^{1}$ volume distortion is bounded by factors arbitrarily close to the absolute determinant of the derivative (On a small cube, a $C^{1}$ diffeomorphism distorts Jordan content by factors arbitrarily close to its linearized absolute determinant), with finite Jordan cover bounds controlling upper and lower sums (Finite Jordan covers bound upper integrals, while interior-disjoint Jordan subfamilies bound lower integrals).

[L3]

The image $g (K)$ is compact Jordan (An injective $C^{1}$ map with invertible derivative sends compact Jordan sets to compact Jordan sets), while the inverse function theorem supplies local $C^{1}$ inverses (The Euclidean inverse function theorem).

[L4]

The chain rule multiplies derivatives (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ), and for $n \geq 1$ and $A, B \in M_{n} (R)$ over a commutative ring one has $\det (A B) = \det (A) \det (B)$ (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[L5]

The Riemann integral is linear, monotone, and stable under absolute value (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ), with Jordan-set values independent of the bounding rectangle (The Riemann integral over a Jordan set is independent of the bounding rectangle).

[L6]

Every continuous real function on a compact Jordan set is Riemann integrable there (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

[L7]

Finite Jordan covers bound upper integrals, and interior-disjoint Jordan subfamilies bound lower integrals (Finite Jordan covers bound upper integrals, while interior-disjoint Jordan subfamilies bound lower integrals).

Proof

technique · local-to-global

1.1

The entries of $D g$ are continuous; [L1] therefore makes $\det D g$ and $∣ \det D g ∣$ continuous on $K$ , and [L6] makes the absolute determinant bounded and Riemann integrable. By [L3], $g (K)$ is also a compact Jordan set.

L1L3L6

1.2

Global injectivity and [L3] patch the local inverses into a $C^{1}$ inverse $G : g (U) \to U$ . By [L4], $D G (g (x)) D g (x) = I$ and $∣ \det D G (g (x)) ∣ ∣ \det D g (x) ∣ = 1$ .

L3L4

2.1

Let $E \subseteq K$ be compact Jordan. Cover it by finitely many cubes on which [L2] gives volume factors $∣ \det D g (a) ∣ (1 \pm ε)^{n}$ and on which $∣ \det D g ∣$ has arbitrarily small oscillation. A common interior-disjoint grid refinement and [L7] compare $cont (g (E))$ with the lower and upper sums of $∣ \det D g ∣$ over $E$ . Letting the mesh and $ε$ tend to zero gives $cont (g (E)) = \int_{E} ∣ \det D g ∣$ .

L2L7step 1.1step 1.2

3.1

First take $f \geq 0$ integrable on $g (K)$ . A fine rectangular grid of a bounding rectangle cuts $g (K)$ , up to content-zero shared faces, into compact Jordan pieces $F_{j}$ on which the lower and upper Darboux step functions have arbitrarily small integral gap. Their preimages $E_{j} = G (F_{j})$ are compact Jordan by [L3]. Step 2.1 turns every coefficient times $cont (F_{j})$ into the integral of that coefficient times $∣ \det D g ∣$ over $E_{j}$ . Hence the pulled-back lower and upper step functions squeeze $(f \circ g) ∣ \det D g ∣$ with the same arbitrarily small gap, proving its integrability and the formula. Applying this implication to $G$ and using step 1.2 proves the converse.

L3L5step 1.2step 2.1

4.1

For signed $f$ , apply step 3.1 to $f^{+} = \max (f, 0)$ and $f^{-} = \max (- f, 0)$ . Stability under absolute value and linearity in [L5] give both integrability implications and the formula for $f = f^{+} - f^{-}$ . Bounding-rectangle independence also follows from [L5].

L5step 3.1∎

Depends on

Used by

Dependency tree · two levels

88 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

A. Leibman, Multidimensional Real Analysis, Theorem 5.5.7 (standard reference, not scraped)
J. Lebl, Basic Analysis II, Theorem 10.7.2 (standard reference, not scraped)

Change of variables for an injective C1C1 map on a compact Jordan set