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.
On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let . Under the identification the product measure and the Euclidean Lebesgue measure agree on every Borel subset of .
Facts & Assumptions
Given: The Axiom of Countable Choice, positive integers , and the identification .
The Borel sigma-algebra on is . (The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n})
The product measure on sigma-finite spaces exists and satisfies the rectangle formula. (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique)
Assuming countable choice, Lebesgue measure of a box is the product of its side lengths. (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
Two measures that agree on a sigma-finite generating pi-system agree on the generated sigma-algebra. (Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system)
Rational half-open boxes, together with the empty set, form a generating pi-system for . The increasing boxes exhaust the space and have finite measure for both measures in the Statement.
Proof
For , the cubes exhaust and have finite measure by [L3], so the sigma-finite product theorem [L2] applies. Let be a rational half-open box. Split it as with and . Then the rectangle formula of [L2] and [L3] give
Each from [A1] has finite -measure by [L3], and finite product measure by [L2] and [L3]; step 1.1 shows these values agree. The same step gives agreement on the whole generating pi-system, while [L1] identifies its generated sigma-algebra with . Therefore [L5] implies on every Borel set.
Depends on
- The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}
- For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system
- Pi-systems
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Not every compact set is conformally removable Counterexample
- The local conservation law need not integrate to a finite conserved energy Counterexample
- The one-dimensional torus and its normalized Haar integral Definition
- Brownian finite-dimensional density Example
- Extremal length of a rectangle and of a round annulus by hand Example
- Hörmander estimate with a Gaussian weight Example
- Archimedean product region, volume and norm bound Lemma
- Bounded primitive integral element for Hermite-Minkowski Lemma
- Schwartz derivatives are integrable Lemma
- Successive-minima volume deformation and collision avoidance Lemma
- The mean-value L² bound for holomorphic functions on a polydisc Lemma
- Triangular Borel maps scale Euclidean volume Lemma
- Weighted monomial integrals and monomial norms for the disc, ball and polydisc Lemma
- Minkowski second theorem on successive minima Theorem
- Polar coordinates decompose Lebesgue measure into rⁿ⁻¹ dr d sigma Theorem
- The Euclidean Lebesgue measure is the completion of the product of the factor Lebesgue measures Theorem
- The logarithmic unit image is a full lattice Theorem
Dependency tree · two levels
41 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
- Terence Tao, An Introduction to Measure Theory, Corollary 1.7.19 (standard reference, not scraped)