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.

Change of variables on bounded open Jordan sets when both integrands are bounded and Riemann integrable

Statement

Let $n \geq 1$ , let $W \subseteq R^{n}$ be open, let $U$ be a bounded open Jordan set with $\overline{U} \subseteq W$ , and let $g : W \to R^{n}$ be injective and $C^{1}$ , with invertible derivative throughout $W$ . Put $V = g (U)$ and assume $V$ is a bounded open Jordan set. If $f : V \to R$ and $h (x) = f (g (x)) ∣ \det D g (x) ∣ (x \in U)$ are both bounded and Riemann integrable on their respective Jordan sets, then $\int_{V} f (y) d y = \int_{U} h (x) d x .$ No improper-integral convention is implicit in this statement.

Facts & Assumptions

Given: The bounded open Jordan sets, map, and two bounded integrable functions in the statement.

[L1]

A bounded open Jordan set has a compact grid exhaustion with vanishing-content remainder (A bounded open Jordan set has an increasing exhaustion by compact finite unions of grid rectangles with vanishing content remainder).

[L2]

Compact-Jordan change of variables applies to every member of that exhaustion (Change of variables for an injective $C^{1}$ map on a compact Jordan set).

[L3]

On a bounding rectangle, the absolute value of an integral is bounded by the integral of the absolute value (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ); zero extension gives the corresponding supremum-times-content bound on a Jordan subset.

[L4]

For a $C^{1}$ map the derivative entries are continuous (Continuously differentiable maps, local inverses, and local diffeomorphisms); the determinant is a polynomial in those entries (For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries), finite algebra preserves continuity (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), and a continuous real function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · exhaustion

1.1

If $U = \emptyset$ , then $V = \emptyset$ and both integrals are $0$ . Otherwise choose the compact grid exhaustion $K_{j} ↑ U$ from [L1]. For every $j$ , [L2] gives $\int_{g (K_{j})} f = \int_{K_{j}} h .$

L1L2given

2.1

A bound $M_{h}$ for $∣ h ∣$ gives source error at most $M_{h} cont (U ∖ K_{j})$ , which tends to zero by [L1] and [L3].

L1L3givenstep 1.1

3.1

The compact set $\overline{U}$ is nonempty, and [L4] gives a bound $M_{D}$ for $∣ \det D g ∣$ on it. Apply [L2] to the compact Jordan remainder $\overline{U} ∖ int K_{j}$ with the constant-one function. Its content tends to zero with $cont (U ∖ K_{j})$ , so $cont (V ∖ g (K_{j})) \leq M_{D} cont (\overline{U} ∖ int K_{j}) \to 0$ . A bound for $∣ f ∣$ and [L3] make the image error tend to zero as well. Passing to the limit in step 1.1 proves the formula.

L2L3L4givenstep 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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