LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

All-generation dyadic cubes: partition, volume and nesting

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Let $n \geq 1$ and use the all-generations dyadic cubes of Dyadic cubes of all generations in R^n. Then:

For every $k \in Z$ the generation- $k$ dyadic cubes are pairwise disjoint and cover $R^{n}$ , and each has volume $∣ Q_{k, m} ∣ = 2^{- k n}$ .
Every dyadic cube $Q$ of generation $k$ has, for each $j < k$ , exactly one ancestor dyadic cube of generation $j$ containing $Q$ ; in particular the parent of $Q$ has generation $k - 1$ and volume $2^{n} ∣ Q ∣$ .
If dyadic cubes $Q, Q^{'}$ of generations $k \leq k^{'}$ intersect, then $Q^{'} \subseteq Q$ ; consequently two dyadic cubes are either disjoint or one contains the other, and cubes of one generation are equal or disjoint.

Facts & Assumptions

Given: An integer $n \geq 1$ ; dyadic cubes $Q = Q_{k, m}$ and $Q^{'} = Q_{k^{'}, m^{'}}$ of generations $k \leq k^{'}$ ; an ancestor generation $j < k$ ; Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) is assumed only in claim 1, for the identification of the box volume with Lebesgue measure.

[L1]

$Q_{k, m} = {x \in R^{n} : m_{i} 2^{- k} < x_{i} \leq (m_{i} + 1) 2^{- k} for every i < n}$ with $k \in Z$ , the side length is $2^{- k}$ , and every dyadic cube is nonempty (Dyadic cubes of all generations in R^n).

[L2]

$B (a, b) = {x \in R^{n} : a_{i} < x_{i} \leq b_{i} for every i < n}$ for real parameters; when $a_{i} < b_{i}$ for every $i < n$ , its box volume is $vol (B) = \prod_{i < n} (b_{i} - a_{i})$ . Empty boxes have volume zero (Half-open boxes in $R^{n}$ and their volume).

[F1]

For every real $t$ there is exactly one integer $m$ with $m \leq t < m + 1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[F2]

For $a \neq 0$ and integers $r, s$ one has $a^{r + s} = a^{r} a^{s}$ and $(a^{r})^{s} = a^{r s}$ ; in particular $2^{k} 2^{- k} = 1$ and $2^{k} > 0$ for every $k \in Z$ (Laws of integer exponents, Integer powers $a^{m}$ ).

[F3]

The order on $Z$ is total and compatible with addition, and $x \leq y$ implies $x + z \leq y + z$ (The integers form a totally ordered ring); the canonical embedding $N \to Z$ is injective, preserves the order, and has image exactly the nonnegative integers, so every positive integer is the image of a unique natural number $\geq 1$ (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[F4]

Finite products are defined by the recursion $Π_{0} = 1$ , $Π_{σ (n)} = Π_{n} \cdot a_{n}$ , and $\prod_{i < n} (a_{i} b_{i}) = (\prod_{i < n} a_{i}) (\prod_{i < n} b_{i})$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[F5]

Every half-open box $B (a, b)$ with real parameters satisfying $a_{i} \leq b_{i}$ for every $i < n$ is Lebesgue measurable with $λ_{n} (B (a, b)) = \prod_{i < n} (b_{i} - a_{i})$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

Proof

technique · direct

1.1F1F3algebra

For a real $t$ there is exactly one integer $m$ with $m < t \leq m + 1$ : applying [F1] to $- t$ gives a unique $p$ with $p \leq - t < p + 1$ , and $m : = - p - 1$ satisfies $m < t \leq m + 1$ ; uniqueness follows because any integer $m^{'}$ with $m^{'} < t \leq m^{'} + 1$ gives $- m^{'} - 1 \leq - t < - m^{'}$ , so $- m^{'} - 1 = p$ and $m^{'} = m$ .

1.2F2givenalgebra

For $k \in Z$ and real $x_{i}$ , the condition $m_{i} 2^{- k} < x_{i} \leq (m_{i} + 1) 2^{- k}$ is equivalent to $m_{i} < 2^{k} x_{i} \leq m_{i} + 1$ , because $2^{k} > 0$ and $2^{k} \cdot 2^{- k} = 1$ by [F2]; multiplying the chain by $2^{k}$ preserves the two inequalities.

1.3F3algebra

For integers $u < v$ one has $u + 1 \leq v$ : by [F3] the positive integer $v - u$ is the image of a natural number $d \neq 0$ , and every nonzero natural number satisfies $1 \leq d$ (its predecessor is a natural number), so $v - u \geq 1$ . Consequently, if integers $A < B$ and $C$ , and a real $t$ , satisfy $A < t \leq B$ and $C < t \leq C + 1$ , then $A \leq C$ and $C + 1 \leq B$ : if $C < A$ then $C + 1 \leq A$ and $t \leq C + 1 \leq A < t$ , a contradiction, and if $B < C + 1$ then $B \leq C < t$ , contradicting $t \leq B$ .

1.4L2F2F4F5algebra

The box $Q_{k, m}$ has Lebesgue measure $∣ Q_{k, m} ∣ = \prod_{i < n} ((m_{i} + 1) 2^{- k} - m_{i} 2^{- k}) = \prod_{i < n} 2^{- k} = (2^{- k})^{n} = 2^{- k n}$ , the last two equalities by the finite-product recursion and the power laws; here $∣ Q ∣$ denotes Lebesgue measure, identified with the box volume by [F5].

2.1L1step 1.1step 1.2step 1.4

Given $x \in R^{n}$ , step 1.1 applied in each coordinate to the real $2^{k} x_{i}$ produces exactly one integer $m_{i}$ with $m_{i} < 2^{k} x_{i} \leq m_{i} + 1$ ; by step 1.2 the function $m$ is the unique index of a generation- $k$ dyadic cube containing $x$ . Hence the generation- $k$ cubes cover $R^{n}$ and no two distinct ones share a point, and by step 1.4 each has volume $2^{- k n}$ .

2.2L1L2F2step 1.3algebra

Put $d : = k^{'} - k \geq 0$ and $M_{i} : = m_{i} 2^{d} \in Z$ ; by [F2], $m_{i} 2^{- k} = M_{i} 2^{- k^{'}}$ and $(m_{i} + 1) 2^{- k} = (M_{i} + 2^{d}) 2^{- k^{'}}$ , so in coordinate $i$ the cube $Q$ is cut out by $M_{i} 2^{- k^{'}} < x_{i} \leq (M_{i} + 2^{d}) 2^{- k^{'}}$ while $Q^{'}$ is cut out by $m_{i}^{'} 2^{- k^{'}} < x_{i} \leq (m_{i}^{'} + 1) 2^{- k^{'}}$ . If $x \in Q \cap Q^{'}$ , step 1.3 with $A : = M_{i}$ , $B : = M_{i} + 2^{d}$ , $C : = m_{i}^{'}$ and $t : = 2^{k^{'}} x_{i}$ gives $M_{i} \leq m_{i}^{'}$ and $m_{i}^{'} + 1 \leq M_{i} + 2^{d}$ in every coordinate, so $Q^{'} \subseteq Q$ .

3.1L1F2step 1.4step 2.1step 2.2algebra

Fix $j < k$ and take the upper corner $x_{i} = (m_{i} + 1) 2^{- k}$ of $Q$ ; the half-open convention places $x$ in $Q$ . By step 2.1 there is exactly one generation- $j$ cube $P$ containing $x$ . Since $P$ and $Q$ intersect and $j < k$ , step 2.2 gives $Q \subseteq P$ . If $P^{'}$ is another generation- $j$ cube containing $Q$ , it contains $x$ , hence $P^{'} = P$ by step 2.1. This proves unique ancestry without any erroneous scaling of the integer index. For the parent $j = k - 1$ , step 1.4 gives $∣ P ∣ = 2^{- (k - 1) n} = 2^{n} 2^{- k n} = 2^{n} ∣ Q ∣$ .

4.1step 2.1step 2.2step 3.1∎

Claim 1 is steps 2.1 and 1.4, claim 2 is step 3.1, and claim 3 is step 2.2 together with its same-generation special case; this proves the lemma.

Depends on

Used by

Dependency tree · two levels

64 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

Loukas Grafakos, Classical Fourier Analysis, third edition (standard reference, not scraped)
Juha Kinnunen, Harmonic Analysis (standard reference, not scraped)