Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26
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 a C1 map injective and regular only on the interior of a compact Jordan set

Statement

Let n≥1, let W⊆Rn be open, let ψ:W→Rn be C1, and let D⊆W be compact and Jordan measurable. Suppose ψ is injective on the interior of D and has nonvanishing Jacobian determinant there, and put V:=ψ[D∘]. Then

  1. ψ[D] is compact and Jordan measurable, V is bounded, open and Jordan measurable, and ψ[D]∖V has content zero;
  2. for every continuous h:ψ[D]→R the three integrals below exist and

∫Dh(ψ(x)) ∣det⁡Dψ(x)∣ dx=∫Vh(y) dy=∫ψ[D]h(y) dy.

No injectivity and no invertibility of the derivative is assumed at any point of ∂D.

Facts & Assumptions

Given: The data of the Statement: W, ψ, the compact Jordan set D⊆W, the injectivity and nonvanishing Jacobian determinant of ψ on D∘, the set V=ψ[D∘], and a continuous h:ψ[D]→R.

[F1]

The boundary of A is ∂A:=A‾∖int⁡(A) (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[F2]

A set has content zero when it can be covered by finitely many closed cubes of arbitrarily small total volume, and content zero passes to subsets (Measure zero and content zero in Rm by countable and finite cube covers).

[F3]

For a C1 map g of an open subset of Rn into Rn, its Jacobian determinant is det⁡Dg(x) (The Jacobian determinant of a square-dimensional C1 map is the determinant of its Jacobian matrix).

[F4]

For bounded Jordan measurable E, bounded f:E→R and a nondegenerate rectangle Q⊇E, the function f is Riemann integrable over E when its zero extension f~Q is integrable over Q, and then ∫Ef=∫Qf~Q (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L1]

If f:U→Rn is C1 on an open U and Df(a) is invertible, then there are open sets V′,W′ with a∈V′⊆U and f(a)∈W′ such that f∣V′:V′→W′ is bijective, and its inverse is C1 (The Euclidean inverse function theorem).

[L2]

A metric-bounded set E⊆Rm is Jordan measurable if and only if its boundary ∂E is null, equivalently has content zero (A bounded set in Rm is Jordan measurable iff its boundary is null, equivalently of content zero).

[L3]

If ψ is C1 on an open W⊆Rm with values in Rm and A⊆W is compact with content zero, then ψ[A] is compact and has content zero (A C1 map sends a compact set of content zero to a set of content zero).

[L4]

For a bounded, open, Jordan measurable V′⊆Rn there are compact Jordan sets K1⊆K2⊆⋯⊆V′, each a finite union of closed grid rectangles, such that every compact C⊆V′ lies in some Kj and cont⁡(V′∖Kj)→0 (A bounded open Jordan set has an increasing exhaustion by compact finite unions of grid rectangles with vanishing content remainder).

[L5]

Let U⊆Rn be open, let g:U→Rn be injective and C1 with Dg(x) invertible for every x∈U, and let K⊆U be compact and Jordan measurable. For bounded f:g(K)→R, integrability of f on g(K) is equivalent to integrability of x↦f(g(x))∣det⁡Dg(x)∣ on K, and when either holds ∫g(K)f(y) dy=∫Kf(g(x))∣det⁡Dg(x)∣ dx (Change of variables for an injective C1 map on a compact Jordan set).

[L6]

Under the hypotheses of [L5], if K⊆U is compact and Jordan measurable then g(K) is compact and Jordan measurable (An injective C1 map with invertible derivative sends compact Jordan sets to compact Jordan sets).

[L7]

For integrable f,g on a nondegenerate rectangle Q and scalars α,β: αf+βg is integrable with integral α∫Qf+β∫Qg; if f≤g then ∫Qf≤∫Qg; and ∣f∣ is integrable with ∣∫Qf∣≤∫Q∣f∣ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L8]

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

[L9]

If bounded Jordan measurable E,F have E∩F of content zero, then cont⁡(E∪F)=cont⁡(E)+cont⁡(F) (Jordan content is finitely additive when the overlap has content zero).

[L10]

For continuous f:X→Y between metric spaces, the image of a compact subset of X is a compact subset of Y (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L11]

A metric-bounded E⊆Rm is Jordan measurable if and only if its indicator 1E is Riemann integrable on a fixed nondegenerate bounding rectangle Q, and then ∫Q1E=cont⁡(E) (A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content).

[L12]

Let E be bounded and Jordan measurable and let f,g:E→R be bounded with {x∈E:f(x)≠g(x)} of content zero. Then f is integrable over E if and only if g is, and their integrals then agree (Changing a bounded integrand on a content-zero set does not change its Riemann integral).

[L14]

For every real square matrix A, det⁡(A)≠0 if and only if A is invertible (A finite square real matrix is invertible if and only if its determinant is nonzero).

Proof

technique · direct
1.1givenF1L2L7L8L11

Suppose first D∘=∅. Then V=∅ and, by [F1], D=∂D, which has content zero by [L2]; so cont⁡(D)=0 by [L11], the parameter integrand is continuous on the compact Jordan D and hence integrable by [L8], and [L7] with [L11] bounds its integral in absolute value by sup⁡D∣h(ψ)det⁡Dψ∣⋅cont⁡(D)=0. All three integrals are then 0 and both assertions hold. Assume D∘≠∅ for the rest of the proof.

1.2givenF1L2L3L13

The set ∂D is a closed subset of the compact D by [F1], hence compact by [L13], and it has content zero by [L2] since D is Jordan measurable. So [L3] gives that ψ[∂D] is compact and has content zero.

2.1step 1.2F1F2L2

By [F1] the interior D∘ is open and bounded, and ∂(D∘)=D∘‾∖D∘⊆D∖D∘=∂D because D∘‾⊆D‾=D. So ∂(D∘) has content zero by step 1.2 and [F2], and D∘ is Jordan measurable by [L2].

2.2step 1.1givenF3L1L14

On D∘ the map ψ is injective and det⁡Dψ≠0, so [F3] and [L14] make each Dψ(c) invertible, and then [L1] makes ψ carry an open neighbourhood of each c∈D∘ onto an open set. Hence ψ[D∘]=V is open, and ψ∣D∘:D∘→V is a bijection whose inverse is C1, in particular continuous, on V.

3.1step 1.2step 2.2F1F2L2L10L13

By [L10] the set ψ[D] is compact, hence closed and bounded by [L13]. Since D=D∘∪∂D by [F1], ψ[D]=V∪ψ[∂D], so ψ[D]∖V⊆ψ[∂D] has content zero by step 1.2 and [F2]. As V is open with V⊆ψ[D], we get ∂V=V‾∖V⊆ψ[D]∖V and ∂(ψ[D])=ψ[D]∖int⁡(ψ[D])⊆ψ[D]∖V; both therefore have content zero, and [L2] makes V and ψ[D] Jordan measurable.

3.2step 2.1step 2.2L4L5L6L8

Apply [L4] to the bounded open Jordan set D∘ of step 2.1, obtaining compact Jordan sets K1⊆K2⊆⋯⊆D∘ with every compact subset of D∘ contained in some Kj and cont⁡(D∘∖Kj)→0. By step 2.2 the hypotheses of [L5] hold with U=D∘ and g=ψ∣D∘, so for each j the set ψ[Kj] is compact and Jordan measurable by [L6] and ∫ψ[Kj]h=∫Kjh(ψ(x)) ∣det⁡Dψ(x)∣ dx, both integrals existing because h is continuous on the compact Jordan ψ[Kj], hence integrable there by [L8].

4.1step 3.1F4L8L12

The set ψ[D] is compact and Jordan measurable by step 3.1 and h is continuous on it, so [L8] makes h integrable over ψ[D] and, ψ[D] being compact, ∣h∣≤M there for some M≥0. Fix a nondegenerate rectangle Q⊇ψ[D]. The zero extensions of h∣V and of h from ψ[D] differ only on ψ[D]∖V, which has content zero by step 3.1, so [L12] applied on Q makes the first integrable too, with ∫Vh=∫ψ[D]h by [F4].

4.2step 1.2step 3.2F1L2L7L8L9L11

The map x↦h(ψ(x))∣det⁡Dψ(x)∣ is continuous on the compact Jordan D, hence integrable over D and over each compact Jordan Kj by [L8], and bounded there by some M′≥0. Fix a nondegenerate rectangle Q′⊇D. Because ∂(D∖Kj)⊆∂D∪∂Kj — a point outside both boundaries lies either in int⁡Kj, whose neighbourhood misses D∖Kj, or outside Kj‾ and inside int⁡D, whose neighbourhood lies in D∖Kj — the set D∖Kj is Jordan measurable by [L2] and [F1]. The two zero extensions differ only on D∖Kj and by at most M′, so [L7] and [L11] give ∣∫Dh(ψ)∣det⁡Dψ∣−∫Kjh(ψ)∣det⁡Dψ∣∣≤M′cont⁡(D∖Kj). Now D∖Kj=∂D∪(D∘∖Kj) is a union of two disjoint Jordan sets, ∂D having content zero by step 1.2, so [L9] gives cont⁡(D∖Kj)=cont⁡(D∘∖Kj), which tends to 0 by step 3.2. Hence those integrals converge to ∫Dh(ψ)∣det⁡Dψ∣.

5.1step 2.2step 3.1step 3.2L4L7L10L11

Apply [L4] to the bounded open Jordan set V of step 3.1, obtaining compact Jordan C1⊆C2⊆⋯⊆V with cont⁡(V∖Cl)→0 and every compact subset of V inside some Cl. Fix l. By step 2.2 the inverse of ψ∣D∘ is continuous, so (ψ∣D∘)−1[Cl] is a compact subset of D∘ by [L10], and step 3.2 puts it inside some Kj(l); applying ψ gives Cl⊆ψ[Kj(l)] and hence V∖ψ[Kj]⊆V∖Cl for every j≥j(l), the sets Kj being increasing. Both sets are Jordan measurable by step 3.1, step 3.2 and the boundary inclusion of step 4.2, so [L7] and [L11] give cont⁡(V∖ψ[Kj])≤cont⁡(V∖Cl); letting l grow, cont⁡(V∖ψ[Kj])→0.

6.1step 4.1step 5.1L7L11

With M and Q as in step 4.1, the zero extensions of h∣V and of h∣ψ[Kj] differ only on V∖ψ[Kj] and by at most M, so [L7] and [L11] give ∣∫Vh−∫ψ[Kj]h∣≤Mcont⁡(V∖ψ[Kj]), which tends to 0 by step 5.1. Hence ∫ψ[Kj]h→∫Vh.

7.1step 4.2step 6.1∎

By step 3.2 the two sequences of integrals agree term by term; by step 4.2 the parameter side converges to ∫Dh(ψ)∣det⁡Dψ∣ and by step 6.1 the image side converges to ∫Vh, so those two numbers are equal, and step 4.1 identifies ∫Vh with ∫ψ[D]h. With step 3.1 this is both assertions of the Statement.

Remarks

  • What the published compact theorem cannot do here. [L5] requires the derivative to be invertible at every point of an open set containing the compact domain. A spherical octant, parametrized by polar angle and azimuth, has vanishing projected Jacobian determinant along the parameter boundary, so no such open set exists and [L5] does not apply to it. Everything above is the work of pushing the degeneracy into ∂D, where [L3] makes its image negligible.

  • The conclusion is about the open image, and that is not a defect. The set ψ[D] may fold its boundary onto itself, and no injectivity is assumed there; what the identity says is that the fold contributes nothing, because ψ[D]∖V has content zero.

Depends on

Used by

Dependency tree · two levels

103 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