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.
The Cantor set has dimension log 2 / log 3 and critical measure one
Statement
Assume the Axiom of Countable Choice. For the middle-thirds Cantor set and ,
These values use the unnormalised diameter-power convention.
Facts & Assumptions
Given: The objects, conventions, and hypotheses in the statement above.
Under the standing Countable Choice hypothesis, for the Cantor probability measure, every nonempty bounded set has at . The sharp interval bound for Cantor measure
Under the standing Countable Choice hypothesis, a finite Borel measure with outer mass on positive and diameter bound gives . The mass distribution principle
Finite positive Hausdorff measure at forces dimension . Hausdorff dimension is the unique critical exponent
consists exactly of the ternary expansions using only zero and two. The Cantor set is exactly the set of with every , and this gives a bijection with
Positive real powers obey the multiplication and power-of-power laws. The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
Under the standing Countable Choice hypothesis, is a probability measure concentrated on . The Cantor measure is a singular atomless probability measure concentrated on the Cantor set
Under Countable Choice, , where the extended Cantor function is nondecreasing and right-continuous on . The Cantor measure
Under Countable Choice, the Lebesgue–Stieltjes measure of a nondecreasing right-continuous real function is a Borel measure on . Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on
Proof
The length- basic intervals cover and have total -cost . At each positive scale take sufficiently large. Thus , including the level-zero cover at its own scale.
The defining function in F7 satisfies F8, so is a Borel measure; F6 makes it finite with total mass one and . Every Borel superset of has by monotonicity, hence . Thus the Borel-hull outer measure in F2 satisfies . F1 supplies its diameter bound with constant one, in particular for every nonempty set of diameter less than . F2 gives . Together with step 1.1 this gives finite positive measure one, so F3 gives .
Depends on
- The sharp interval bound for Cantor measure
- The mass distribution principle
- Hausdorff dimension is the unique critical exponent
- The Cantor set is exactly the set of $\sum_{k \ge 1} a_k 3^{-k}$ with every $a_k \in \{0,2\}$, and this gives a bijection with $\{0,1\}^{\mathbb{N}}$
- The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents
- The Cantor measure is a singular atomless probability measure concentrated on the Cantor set
- The Cantor measure
- Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on $\mathbb{R}$
Used by
Dependency tree · two levels
52 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
- Fremlin, Measure Theory, 264J (standard reference, not scraped)
- Hunter, Measure Theory, Theorem 2.34 and Example 2.37 (standard reference, not scraped)