LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Triangular Borel maps scale Euclidean volume

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 1$ , let $a_{1}, \dots, a_{n} > 0$ be real numbers, and for $i = 1, \dots, n$ let $ψ_{i} : R^{n - i} \to R$ be a Borel function, where $R^{0}$ is a one-point space so that $ψ_{n}$ is a constant. Define the triangular map

$T : R^{n} ⟶ R^{n}, T (x)_{i} = a_{i} x_{i} + ψ_{i} (x_{i + 1}, \dots, x_{n}) (i = 1, \dots, n) .$

Then $T$ is a bijection, $T$ and $T^{- 1}$ are Borel maps, $T (E)$ is a Borel set for every Borel $E \subseteq R^{n}$ , and

$vol (T (E)) = (\prod_{i = 1}^{n} a_{i}) vol (E) .$

Equivalently, the inverse triangular map scales volume by $(\prod_{i} a_{i})^{- 1}$ , and both identities hold with $+ \infty$ allowed.

Facts & Assumptions

Given: The Axiom of Choice, an integer $n \geq 1$ , positive reals $a_{1}, \dots, a_{n}$ , Borel functions $ψ_{i}$ as in the statement, and a Borel set $E \subseteq R^{n}$ . Put $φ_{i} : = ψ_{i} / a_{i}$ and $S_{i} (x) : = x + φ_{i} (x_{i + 1}, \dots, x_{n}) e_{i}$ for $i = 1, \dots, n$ , and let $A (x)_{i} : = a_{i} x_{i}$ be the diagonal scaling.

[A1]

The Axiom of Choice implies the Axiom of Countable Choice (AC implies DC implies countable choice), so the countable-choice hypotheses of [F2] and [F4] are discharged for the whole argument; no further choice is used.

[F1]

Tonelli's theorem: for sigma-finite measure spaces and a product-measurable $f \geq 0$ , the integral over the product equals either iterated integral (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F2]

Under the identification $R^{m + n} = R^{m} \times R^{n}$ , the product measure $λ_{m} \times λ_{n}$ agrees with Lebesgue measure $λ_{m + n}$ on every Borel set (On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}).

[F3]

Lebesgue measure is translation invariant: $λ_{n} (E + h) = λ_{n} (E)$ for every Lebesgue measurable $E$ , and $E$ is measurable if and only if $E + h$ is (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[F4]

For nonzero real $c$ , $λ_{n} (c E) = ∣ c ∣^{n} λ_{n} (E)$ for every Lebesgue measurable $E$ , and $E$ is measurable if and only if $c E$ is (For a nonzero real $c$ , dilation by $c$ multiplies Lebesgue outer measure by $∣ c ∣^{n}$ , and reflection in the origin preserves it).

Proof

1.1given

The factors satisfy $T = A \circ S$ for the shear $S$ given by $S (x)_{i} = x_{i} + φ_{i} (x_{i + 1}, \dots, x_{n})$ : indeed $A (S (x))_{i} = a_{i} S (x)_{i} = a_{i} x_{i} + ψ_{i} (x_{i + 1}, \dots, x_{n})$ .

1.2given

For points written as $(u, t, v) \in R^{i - 1} \times R \times R^{n - i}$ , the shear is $S_{i} (u, t, v) = (u, t + φ_{i} (v), v)$ , a bijection whose inverse $(u, t, v) \mapsto (u, t - φ_{i} (v), v)$ is Borel because $φ_{i}$ is Borel; hence $S_{i} (F)$ is Borel for every Borel $F$ , and for a Borel set $F$ the $t$ -section at fixed $(u, v)$ is the translate of the section of $F$ by $φ_{i} (v)$ .

1.3given

The sections of a Borel set $F \subseteq R^{i - 1} \times R \times R^{n - i}$ are Borel sets, because they are the preimages of $F$ under the continuous maps $t \mapsto (u, t, v)$ ; in particular they are Lebesgue measurable and [F3] applies to them.

1.4given

The diagonal scaling factors as $A = D_{1} \circ \dots \circ D_{n}$ with $D_{i}$ multiplying only the $i$ -th coordinate by $a_{i}$ , and each $D_{i}$ is an invertible linear bijection whose inverse is Borel, so $D_{i} (F)$ is Borel for every Borel $F$ .

2.1F1F2F3step 1.2step 1.3

For each $i$ and every Borel $F \subseteq R^{n}$ one has $vol (S_{i} (F)) = vol (F)$ : writing $f = 1_{S_{i} (F)}$ and using [F2] and [F1], the volume is the iterated integral $\int \int \int f (u, t, v) d u d t d v$ , whose $t$ -integrand at fixed $(u, v)$ equals $1_{F} (u, t - φ_{i} (v), v)$ , and its integral over $t$ equals the $t$ -length of the section of $F$ at $(u, v)$ by [F3] and step 1.3; integrating the unchanged section lengths over $(u, v)$ with [F1] returns $vol (F)$ .

2.2A1F4step 1.4

For each $i$ and every Borel $F \subseteq R^{n}$ , with $f = 1_{D_{i} (F)}$ the $t$ -integrand at fixed $(u, v)$ equals $1_{F} (u, t / a_{i}, v)$ , whose integral over $t$ is the length of the section of $F$ scaled by $a_{i}$ by [F4] in dimension one; the countable-choice hypothesis is supplied by [A1].

2.3step 1.2step 1.1

The shear $S = S_{n} \circ \dots \circ S_{1}$ : applying $S_{1}, \dots, S_{n}$ in that order changes the $i$ -th coordinate by $φ_{i} (x_{i + 1}, \dots, x_{n})$ while the higher coordinates are still the original ones, and $S$ is a Borel bijection with Borel inverse.

3.1F1F2step 2.2

Integrating the section identity of step 2.2 over the remaining coordinates with [F1] and [F2] gives $vol (D_{i} (F)) = a_{i} vol (F)$ for every Borel $F$ .

3.2step 2.1step 2.3

For every Borel $F$ one has $vol (S (F)) = vol (F)$ and $S (F)$ Borel, by applying step 2.1 to the factors of the composition in step 2.3.

4.1step 1.1step 1.4step 3.1step 3.2

Consequently $T = A \circ S$ satisfies $vol (T (E)) = vol (A (S (E))) = (\prod_{i} a_{i}) vol (S (E)) = (\prod_{i} a_{i}) vol (E)$ , and $T (E)$ is Borel, by steps 1.4, 3.1, 3.2 and the factorization of step 1.1.

5.1step 4.1algebra∎

The backward recursion $x_{i} = a_{i}^{- 1} (y_{i} - ψ_{i} (x_{i + 1}, \dots, x_{n}))$ , run from $i = n$ down to $i = 1$ , exhibits $T^{- 1}$ as a composition of Borel functions, so $T$ is a bijection with Borel inverse; applying the identity of step 4.1 to $T^{- 1}$ , which is again a triangular map with coefficients $a_{i}^{- 1}$ and Borel data from the same recursion, gives $vol (T^{- 1} (F)) = (\prod_{i} a_{i})^{- 1} vol (F)$ for Borel $F$ , and $T$ and $T^{- 1}$ being Borel in both directions makes each a Borel isomorphism.

Depends on

Used by

Successive-minima volume deformation and collision avoidance Lemma

Dependency tree · two levels

44 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

Ben Green, Additive Combinatorics, Lecture 3 §3.7 (standard reference, not scraped)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)