TheoremStatement: AI-adaptedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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\ge1$ , let $U\subseteq\mathbb R^n$ be open, let $g:U\to\mathbb R^n$ be injective and $C^1$ , and suppose $Dg(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\mathbb R$ , the following are equivalent:

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

When either condition holds, $\int_{g(K)}f(y)\,dy=\int_K f(g(x))|\det Dg(x)|\,dx.$

Facts & Assumptions

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

[L1]

For each fixed $n\ge1$ , the function $\det:M_n(\mathbb R)\to\mathbb 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)=Dg(f(a))\circ Df(a)$ ), and for $n\ge1$ and $A,B\in M_n(R)$ over a commutative ring one has $\det(AB)=\det(A)\det(B)$ (For same-sized finite square matrices over a commutative ring, $\det(AB)=\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 $\mathbb{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 $Dg$ are continuous; [L1] therefore makes $\det Dg$ and $|\det Dg|$ 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], $DG(g(x))Dg(x)=I$ and $|\det DG(g(x))|\,|\det Dg(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 Dg(a)|(1\pm\varepsilon)^n$ and on which $|\det Dg|$ has arbitrarily small oscillation. A common interior-disjoint grid refinement and [L7] compare $\operatorname{cont}(g(E))$ with the lower and upper sums of $|\det Dg|$ over $E$ . Letting the mesh and $\varepsilon$ tend to zero gives $\operatorname{cont}(g(E))=\int_E|\det Dg|$ .

L2L7step 1.1step 1.2

3.1

First take $f\ge0$ 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 $\operatorname{cont}(F_j)$ into the integral of that coefficient times $|\det Dg|$ over $E_j$ . Hence the pulled-back lower and upper step functions squeeze $(f\circ g)|\det Dg|$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 237 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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 C1C^1C1 map on a compact Jordan set