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

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

Statement

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

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}(\operatorname{supp}f)$ is compact and lies in $U$ . By [L1], choose compact Jordan $K$ with $C\subseteq\operatorname{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_Kh.$

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 $\mathbb R^n$ .

L3step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 140 results over 24 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)