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.
Dyadic cubes of generation in
Definition
Fix . For and a function (The integers as equivalence classes of pairs of naturals), whose values are read inside along the canonical embedding, the dyadic cube of generation and index is the half-open box (Half-open boxes in and their volume)
that is , the powers being the integer powers of Integer powers . A dyadic cube is a set of this form for some and ; its generation is and its side length is .
Every dyadic cube is nonempty, since for every , so by Half-open boxes in and their volume its parameters are determined by the set; the generation and the index are therefore determined by the cube as well. At the cubes are the translates of the unit cube by integer vectors, and .
Remarks
-
The half-open convention is what makes the family a tiling. The cubes of a fixed generation are pairwise disjoint and cover (For each generation, the dyadic cubes of that generation are pairwise disjoint and cover ), which would fail for closed cubes, whose faces overlap, and for open cubes, which miss the grid points.
-
Generations are natural numbers here, so the side lengths are at most and there is a coarsest generation. Nothing below needs cubes larger than the unit cube, and bounding the generations below is what makes the maximal-cube selection of Every open subset of is the union of a countable pairwise disjoint family of dyadic cubes work.
Depends on
Used by
- A measurable set of positive finite measure occupies more than any prescribed proportion of some dyadic cube Lemma
- A translation-invariant Borel measure giving the unit cube measure one gives each generation-k dyadic cube measure 2⁻ᵏⁿ Lemma
- Countable covers by closed boxes, by open boxes and by closed cubes all compute Lebesgue outer measure Lemma
- For each generation, the dyadic cubes of that generation are pairwise disjoint and cover ℝⁿ Lemma
- The sigma-algebra generated by the half-open boxes of ℝⁿ is the Borel sigma-algebra Lemma
- Two dyadic cubes are either disjoint or one contains the other Lemma
- A translation-invariant measure on the Borel sets of ℝⁿ giving the unit cube measure one is the restriction of Lebesgue measure Theorem
- Every open subset of ℝⁿ is the union of a countable pairwise disjoint family of dyadic cubes Theorem
- If a Lebesgue measurable subset of ℝⁿ has positive measure, its difference set contains an open ball about the origin Theorem
Dependency tree · two levels
20 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
- T. Tao, An Introduction to Measure Theory (GSM 126), Exercise 1.1.14 (standard reference, not scraped)
- John K. Hunter, Measure Theory (UC Davis lecture notes), Chapter 2 (standard reference, not scraped)