LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-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.

Archimedean product region, volume and norm bound

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let integers $r_{1}, r_{2} \geq 0$ with $n = r_{1} + 2 r_{2} \geq 1$ and a real $t > 0$ be given, and in $R^{r_{1}} \times C^{r_{2}} ≅ R^{n}$ put

$X_{t} = {(x, z) : \sum_{i = 1}^{r_{1}} ∣ x_{i} ∣ + 2 \sum_{j = 1}^{r_{2}} ∣ z_{j} ∣ \leq t} .$

Then:

$X_{t}$ is compact, convex and centrally symmetric with nonempty interior;
$vol (X_{t}) = 2^{r_{1}} (\frac{π}{2})^{r_{2}} \frac{t^{n}}{n!}$ ;
every point of $X_{t}$ satisfies $\prod_{i = 1}^{r_{1}} ∣ x_{i} ∣ \prod_{j = 1}^{r_{2}} ∣ z_{j} ∣^{2} \leq (\frac{t}{n})^{n}$ .

Facts & Assumptions

Given: The Axiom of Choice, integers $r_{1}, r_{2} \geq 0$ with $n = r_{1} + 2 r_{2} \geq 1$ and a real $t > 0$ , with $X_{t}$ as in the statement and the identification of Unscaled Minkowski embedding.

[A1]

The Axiom of Choice gives the Axiom of Countable Choice (AC implies DC implies countable choice), which discharges the Countable Choice hypotheses of the volume facts [F6], [F1] and [F3], invoked in steps 1.4, 2.1 and 3.1 respectively; no further choice is used.

[F1]

Polar coordinates: for Borel $f \geq 0$ on $R^{m}$ , $\int_{R^{m}} f d λ_{m} = \int_{0}^{\infty} \int_{S^{m - 1}} f (r ω) r^{m - 1} d σ (ω) d r$ , where $σ$ is the polar surface set function on $S^{m - 1}$ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F2]

Tonelli's theorem for sigma-finite product spaces (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F3]

Under $R^{p + q} = R^{p} \times R^{q}$ , the product measure agrees with Lebesgue measure on Borel sets (On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}).

[F4]

AM-GM: for $a_{1}, \dots, a_{n} \geq 0$ with $n \geq 1$ , $\prod_{k} a_{k} \leq (\frac{1}{n} \sum_{k} a_{k})^{n}$ (The arithmetic mean, geometric mean inequality).

[F5]

The unit disc has area $λ_{2} (B^{2}) = π$ : the unit-ball volume formula $V_{m} (1) = π^{m / 2} / Γ (m / 2 + 1)$ at $m = 2$ gives $π / Γ (2) = π$ (The closed form for the volume of the unit $n$ -ball).

[F6]

Invertible linear maps scale Lebesgue measure by the absolute value of their determinant (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not).

[F7]

The polar surface set function of The polar surface set function on the unit sphere is defined by $σ (E) = n λ_{n} ({r ω : ω \in E, 0 < r \leq 1})$ ; for $E = S^{m - 1}$ the set on the right is the unit ball $B^{m}$ up to the null set ${0}$ , so $σ (S^{m - 1}) = m λ_{m} (B^{m})$ (The polar surface set function on the unit sphere).

Proof

1.1given

The function $N (x, z) = \sum_{i} ∣ x_{i} ∣ + 2 \sum_{j} ∣ z_{j} ∣$ is continuous, convex and even, so $X_{t} = N^{- 1} ([0, t])$ is closed, convex and centrally symmetric; it is bounded because every coordinate of a point of $X_{t}$ has absolute value at most $t$ , hence compact, and the origin is interior because a small ball around the origin satisfies $\sum_{i} ∣ x_{i} ∣ + 2 \sum_{j} ∣ z_{j} ∣ < t$ .

1.2algebra

(Weighted simplex integral.) For integers $p \geq 0$ and nonnegative integer weights $c_{1}, \dots, c_{p}$ , define $J_{p} (t) = \int_{y_{1}, \dots, y_{p} \geq 0, \sum_{k} y_{k} \leq t} \prod_{k} y_{k}^{c_{k}} d y$ ; then $J_{p} (t) = t^{p + C} \prod_{k} c_{k}! / (p + C)!$ with $C = \sum_{k} c_{k}$ .

1.3F5F7given

For each complex coordinate the polar surface value is $σ (S^{1}) = 2 λ_{2} (B^{2}) = 2 π$ , by [F7] with $m = 2$ and [F5].

1.4F6A1given

(Sign splitting.) The region ${(x, z) : \sum_{i} ∣ x_{i} ∣ + 2 \sum_{j} ∣ z_{j} ∣ \leq t}$ is the union over the $2^{r_{1}}$ sign choices of the pieces with prescribed signs of $x_{1}, \dots, x_{r_{1}}$ , and coordinate reflections carry each piece to the piece with all signs positive while preserving Lebesgue measure by [F6], whose Countable Choice hypothesis is supplied by [A1]; intersections lie in coordinate hyperplanes, which have measure zero.

1.5F4givenalgebra

For $(x, z) \in X_{t}$ apply [F4] with $n$ arguments equal to $∣ x_{1} ∣, \dots, ∣ x_{r_{1}} ∣$ and to the two copies each of $∣ z_{1} ∣, \dots, ∣ z_{r_{2}} ∣$ : their sum is at most $t$ , so their product satisfies $\prod_{i} ∣ x_{i} ∣ \prod_{j} ∣ z_{j} ∣^{2} \leq (t / n)^{n}$ .

2.1A1F1step 1.3given

(Radial reduction.) Using step 1.3 and the polar formula [F1] with $m = 2$ , the substitution $u = 2 ρ$ gives $\int_{C} F (2 ∣ z ∣) d z = 2 π \int_{0}^{\infty} F (2 ρ) ρ d ρ = (π / 2) \int_{0}^{\infty} F (u) u d u$ for Borel $F \geq 0$ , the Countable Choice hypothesis of [F1] being supplied by [A1].

2.2F2step 1.2algebra

(Induction for step 1.2.) The identity of step 1.2 is proved by induction on $p$ : for $p = 0$ both sides are $1$ ; for $p \geq 1$ Tonelli slices the last variable, $J_{p} (t) = \int_{0}^{t} y^{c_{p}} J_{p - 1} (t - y) d y$ , and the induction hypothesis reduces the claim to the one-variable identity $\int_{0}^{t} y^{a} (t - y)^{b} d y = a! b! t^{a + b + 1} / (a + b + 1)!$ , which follows by induction on $b$ from $\int_{0}^{t} y^{a} d y = t^{a + 1} / (a + 1)$ and $y^{a} (t - y)^{b + 1} = t y^{a} (t - y)^{b} - y^{a + 1} (t - y)^{b}$ , both elementary antiderivative computations for polynomials on a compact interval.

3.1F2F3A1step 2.1step 1.4

Applying step 2.1 in each complex coordinate and [F2] together with [F3] to the resulting iterated integrals, then applying step 1.4 to the real coordinates, gives $vol (X_{t}) = 2^{r_{1}} (π / 2)^{r_{2}} D (t)$ with $D (t) = J_{r_{1} + r_{2}} (t)$ for the weight vector with $c_{k} = 0$ on the first $r_{1}$ indices and $c_{k} = 1$ on the remaining $r_{2}$ indices, the Countable Choice hypothesis of [F3] being supplied by [A1].

4.1step 1.2step 3.1step 2.2algebra

For the weight vector of step 3.1 one has $p + C = (r_{1} + r_{2}) + r_{2} = n$ , so $D (t) = t^{n} / n!$ and $vol (X_{t}) = 2^{r_{1}} (π / 2)^{r_{2}} t^{n} / n!$ .

5.1step 1.1step 4.1step 1.5∎

Step 1.1 proves the compactness, convexity and symmetry clause, step 4.1 the volume formula and step 1.5 the norm bound, so the three assertions of the statement hold.

Depends on

Used by

Small nonzero element in a number-field ideal Theorem

Dependency tree · two levels

87 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

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)