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.
Elementary lower and upper bounds on a unit cube
Statement
Assume the Axiom of Countable Choice. For every integer and in the Euclidean metric,
Only coordinate boxes, not the isodiametric inequality, are needed.
Facts & Assumptions
Given: The objects, conventions, and hypotheses in the statement above.
Hausdorff measure is the supremum of diameter-power covering infima. Unnormalised Hausdorff measure
Under Countable Choice Lebesgue outer measure is countably subadditive and agrees with elementary volume. Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume
Under the standing Countable Choice hypothesis, a finite coordinate box of any endpoint convention has measure the product of its side lengths, including zero side lengths. A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Positive real powers obey product and power-of-power laws. The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
Proof
If a nonempty bounded has diameter , its th coordinate ranges between an infimum and supremum with . Hence and . If this is a zero-volume singleton box.
For every finite-scale cover of , countable subadditivity gives . Infimising and then taking the small-scale supremum gives the lower bound; absent covers give the same inequality with infinity on the right. The empty set has both values zero.
Partition into half-open cubes of side . Each has diameter (the supremum of corner distances), so the total cost is . Choose large for any prescribed positive scale. Thus the upper bound holds, while the lower bound is the unit box volume one. For both bounds equal one.
Depends on
- Unnormalised Hausdorff measure
- Lebesgue outer measure on $\mathbb{R}^n$
- Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume
- 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
- The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
Used by
Dependency tree · two levels
29 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
- Falconer §1.2 p.8 cube upper estimate; §1.4 pp.12–13 volume covers; Fremlin 264H(b) (standard reference, not scraped)