Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 sharp interval bound for Cantor measure

Statement

Assume the Axiom of Countable Choice. Set s=log⁡2/log⁡3. For every interval I⊆R,

μc(I)≤(diam⁡I)s.

In particular, for every nonempty bounded U⊆R, its induced Cantor outer measure satisfies μc∗(U)≤(diam⁡U)s.

Facts & Assumptions

Given: The objects, conventions, and hypotheses in the statement above.

[F1]

Under the standing Countable Choice hypothesis, every level-m basic Cantor interval has mass 2−m. Cantor basic intervals have their expected masses

[F2]

For α∈R, positive-base powers are differentiable with derivative αxα−1. Continuity and derivatives of positive-base real powers

[F3]

Measures are continuous from below on increasing measurable sequences. Continuity from below for measures

[F4]

Under the standing Countable Choice hypothesis, μc is an atomless probability concentrated on C. The Cantor measure is a singular atomless probability measure concentrated on the Cantor set

Proof

1.1F2

Here 0<s<1 and 3s=2. For a,b,c≥0 with a,c≤b, one has as+cs≤(a+b+c)s. Indeed the function (x+y)s−xs is nonincreasing in x>0 for fixed y≥0, by its derivative; continuity extends this to x=0. Increasing a to b and then c to b can only decrease (a+b+c)s−as−cs, whose final value is bs(3s−2)=0. If b=0 all three numbers are zero.

1.2given

Fix m. For each basic interval J at a level ℓ≤m and each interval I, let NJ(I) count the level-m basic descendants contained in I∩J. We prove 2−mNJ(I)≤diam⁡(I∩J)s by induction upwards from level m. At that level the count is zero or one; a count of one forces diameter at least 3−m and hence the desired bound. Empty intersections have count and diameter zero.

2.1step 1.1step 1.2

For an earlier J, its two children have length b and are separated by a gap of length b. If I meets neither child the count is zero. If I meets only one child, use its inductive bound and diameter monotonicity. If it meets both, put a=diam⁡(I∩Jleft) and c=diam⁡(I∩Jright). Then a,c≤b and diam⁡(I∩J)≥a+b+c. Adding the two inductive bounds and using the first step proves the claim for J. Thus for J=[0,1] the total number Nm(I) of level-m intervals contained in I satisfies 2−mNm(I)≤diam⁡(I)s.

3.1F1F3F4step 2.1

For a bounded open interval I, let Em be the union of all level-m basic intervals wholly contained in I. These sets need not increase as subsets of the line, but Em∩C do increase: each point of C lies in a child of its previous interval. Their union is C∩I because basic diameters tend to zero. They have measure 2−mNm(I) by disjointness, concentration and cylinder masses. Continuity from below therefore gives μc(I)≤diam⁡(I)s.

4.1F4step 3.1∎

Other bounded interval endpoint conventions change at most two points, which have zero mass, so the same bound holds. A singleton has mass zero, and an empty interval has mass zero; an unbounded interval has infinite diameter and the inequality is immediate. Finally a nonempty bounded U lies in [inf⁡U,sup⁡U], whose length is exactly its diameter. This Borel superset bounds μc∗(U) as claimed.

Depends on

Used by

Dependency tree · two levels

22 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