CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

A compactly supported Riemann integrand admits the global change-of-variables formula from a diffeomorphism near the relevant compact preimage

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, and let $g : U \to R^{n}$ be injective and $C^{1}$ , with $D g (x)$ invertible on $U$ . Let $f : R^{n} \to R$ be compactly supported Riemann integrable and suppose $supp f \subseteq g (U)$ . Define $h (x) = {\begin{cases} f (g (x)) ∣ \det D g (x) ∣, & x \in U, \\ 0, & x \notin U . \end{cases}$ Then $h$ is compactly supported Riemann integrable and $\int_{R^{n}} f (y) d y = \int_{R^{n}} h (x) d x .$

Facts & Assumptions

Given: The local diffeomorphism data and compactly supported $f$ in the statement.

[L1]

A compact subset of an open Euclidean set lies in the interior of a compact Jordan neighborhood contained in that open set (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).

[L2]

Compact-Jordan change of variables gives the integral formula on such a neighborhood (Change of variables for an injective $C^{1}$ map on a compact Jordan set).

[L3]

Compactly supported integrals are independent of their bounding rectangles (The Riemann integral of a compactly supported function is independent of its bounding rectangle).

[L4]

The inverse function theorem gives a local $C^{1}$ inverse wherever the derivative is invertible (The Euclidean inverse function theorem).

Proof

technique · reduction

1.1

By [L4] and global injectivity, the local inverses patch to a continuous inverse on $g (U)$ . Thus $C = g^{- 1} (supp f)$ is compact and lies in $U$ . By [L1], choose compact Jordan $K$ with $C \subseteq int K \subseteq K \subseteq U$ .

L1L4given

2.1

The function $f$ vanishes outside $g (K)$ , while $h$ vanishes outside $K$ . Apply [L2] to $f ∣_{g (K)}$ ; its transformed integrand is $h ∣_{K}$ , giving $\int_{g (K)} f = \int_{K} h .$

L2step 1.1

3.1

The support of $h$ is contained in the compact set $C$ , because $f (g (x)) = 0$ away from its preimage. Thus $h$ is compactly supported and [L3] identifies the two integrals in step 2.1 with the corresponding integrals over $R^{n}$ .

L3step 2.1∎

Depends on

Used by

Dependency tree · two levels

39 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)