LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

A cyclic permutation of the coordinates of $R^{3}$ preserves Jordan measurability and integrals

Statement

For $k \in {x, y, z}$ let $σ_{k} : R^{3} \to R^{3}$ be given by

$σ_{x} (p) = (p_{y}, p_{z}, p_{x}), σ_{y} (p) = (p_{z}, p_{x}, p_{y}), σ_{z} (p) = (p_{x}, p_{y}, p_{z}) .$

Each $σ_{k}$ is a linear bijection with $\det D σ_{k} = 1$ everywhere. Let $E \subseteq R^{3}$ be compact and Jordan measurable. Then $σ_{k} [E]$ is compact and Jordan measurable, and for every bounded $H : σ_{k} [E] \to R$ the function $H$ is Riemann integrable over $σ_{k} [E]$ if and only if $H \circ σ_{k}$ is Riemann integrable over $E$ ; when either holds, the integral over the permuted set equals the integral of the composite with the permutation over the original set,

$\int_{σ_{k} [E]} H = \int_{E} H \circ σ_{k} .$

Facts & Assumptions

Given: The index $k \in {x, y, z}$ , the map $σ_{k}$ displayed in the Statement, the compact Jordan measurable set $E \subseteq R^{3}$ and the bounded function $H$ on $σ_{k} [E]$ .

[F1]

For a commutative ring $R$ , $n \geq 1$ and $A = (a_{i j}) \in M_{n} (R)$ , $\det A = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{σ (i), i}$ , with columns indexed by $i < n$ and rows by $σ (i)$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[F2]

An inversion of $σ \in S_{n}$ is a pair $(i, j)$ with $i < j < n$ and $σ (i) > σ (j)$ , and $sgn (σ) = (- 1)^{inv (σ)}$ , where $inv (σ)$ is the number of inversions (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

[F3]

For a $C^{1}$ map $g$ of an open subset of $R^{n}$ into $R^{n}$ , the Jacobian determinant is $\det D g (x)$ , and the change-of-variables scale factor is $∣ \det D g (x) ∣$ (The Jacobian determinant of a square-dimensional $C^{1}$ map is the determinant of its Jacobian matrix).

[F4]

If every partial derivative $\partial_{j} f_{i} (a)$ exists, the Jacobian matrix is $J f (a) = (\partial_{j} f_{i} (a))_{i < n, j < m}$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F5]

Integration over a bounded Jordan measurable set is integration of the zero extension over a bounding rectangle (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L1]

Let $U \subseteq R^{n}$ be open, let $g : U \to R^{n}$ be injective and $C^{1}$ with $D g (x)$ invertible for every $x \in U$ , and let $K \subseteq U$ be compact and Jordan measurable. For bounded $f : g (K) \to R$ , integrability of $f$ on $g (K)$ is equivalent to integrability of $x \mapsto f (g (x)) ∣ \det D g (x) ∣$ on $K$ , and when either holds $\int_{g (K)} f (y) d y = \int_{K} f (g (x)) ∣ \det D g (x) ∣ d x$ (Change of variables for an injective $C^{1}$ map on a compact Jordan set).

[L2]

Under those hypotheses, if $K \subseteq U$ is compact and Jordan measurable then $g (K)$ is compact and Jordan measurable (An injective $C^{1}$ map with invertible derivative sends compact Jordan sets to compact Jordan sets).

Proof

technique · direct

1.1givenF4

Each $σ_{k}$ is linear: writing coordinates as indices $0, 1, 2$ for $x, y, z$ , the map $σ_{x}$ sends $p$ to the point with coordinates $(p_{1}, p_{2}, p_{0})$ , so by [F4] its partial derivatives are the constants $\partial_{j} (σ_{x})_{i}$ , and its Jacobian matrix $A_{x}$ at every point has $(A_{x})_{i j} = 1$ exactly for $(i, j) \in {(0, 1), (1, 2), (2, 0)}$ and $0$ elsewhere. Likewise $σ_{y}$ sends $p$ to $(p_{2}, p_{0}, p_{1})$ , with matrix $A_{y}$ having entry $1$ exactly at $(0, 2), (1, 0), (2, 1)$ , and $σ_{z}$ is the identity with matrix the identity matrix. All three matrices have exactly one entry $1$ in each row and in each column, so each $σ_{k}$ is a bijection of $R^{3}$ with $D σ_{k}$ constant and invertible.

1.2F1F2algebra

In the Leibniz sum [F1] for $\det A_{x}$ , a term is nonzero only when $(A_{x})_{σ (i), i} = 1$ for every $i < 3$ , that is when $σ (0) = 2$ , $σ (1) = 0$ and $σ (2) = 1$ ; exactly one permutation does this. Its inversions are $(0, 1)$ , since $2 > 0$ , and $(0, 2)$ , since $2 > 1$ , while $(1, 2)$ is not one, since $0 < 1$ ; so $inv (σ) = 2$ and $sgn (σ) = + 1$ by [F2], giving $\det A_{x} = 1$ .

1.3F1F2algebra

In the Leibniz sum for $\det A_{y}$ , the only nonzero term has $σ (0) = 1$ , $σ (1) = 2$ and $σ (2) = 0$ ; its inversions are $(0, 2)$ , since $1 > 0$ , and $(1, 2)$ , since $2 > 0$ , while $(0, 1)$ is not one, since $1 < 2$ ; so again $inv (σ) = 2$ and $\det A_{y} = 1$ by [F1] and [F2]. For $A_{z}$ the identity matrix, the only nonzero term is the identity permutation, with no inversion, so $\det A_{z} = 1$ .

2.1step 1.1step 1.2step 1.3F3L2

By steps 1.1, 1.2 and 1.3 each $σ_{k}$ is a $C^{1}$ injection of the open set $R^{3}$ into $R^{3}$ whose derivative is invertible at every point, with $\det D σ_{k} = 1$ and hence $∣ \det D σ_{k} ∣ = 1$ by [F3]. So [L2] applies with $U = R^{3}$ , $g = σ_{k}$ and $K = E$ , and $σ_{k} [E]$ is compact and Jordan measurable.

3.1step 2.1L1F3F5∎

With the same data, [L1] gives that $H$ is integrable over $σ_{k} [E]$ if and only if $x \mapsto H (σ_{k} (x)) ∣ \det D σ_{k} (x) ∣ = H (σ_{k} (x))$ is integrable over $E$ , that is if and only if $H \circ σ_{k}$ is, and that in that case $\int_{σ_{k} [E]} H = \int_{E} H (σ_{k} (x)) \cdot 1 d x = \int_{E} H \circ σ_{k}$ , the integrals being those of [F5].

Remarks

Why the cyclic order and not the increasing one. The three maps above send the coordinate $k$ to the last slot and keep the other two in the cyclic order $x \to y \to z \to x$ . Taking instead the two surviving coordinates in increasing order would transpose them in the case $k = y$ , and a transposition has one inversion and hence determinant $- 1$ ; every identity on this page that treats the three directions alike depends on the cyclic choice.

Depends on

Used by

Dependency tree · two levels

46 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

G. Strang and E. Herman, Calculus Volume 3 (OpenStax), section 6.8 (standard reference, not scraped)

A cyclic permutation of the coordinates of R3R3 preserves Jordan measurability and integrals