LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

A translation-invariant Borel measure giving the unit cube measure one gives each generation- $k$ dyadic cube measure $2^{- k n}$

Statement

Let $n \geq 1$ and let $μ$ be a measure on $(R^{n}, B (R^{n}))$ (Measures on sigma-algebras, The Borel sigma-algebra of a topological space) such that

$μ (E + h) = μ (E) for every Borel E and every h \in R^{n}, μ ((0, 1]^{n}) = 1.$

Then $μ (Q) = 2^{- k n}$ for every dyadic cube $Q$ of generation $k$ (Dyadic cubes of generation $k$ in $R^{n}$ ).

Only translates of half-open boxes are used, and those are Borel (The sigma-algebra generated by the half-open boxes of $R^{n}$ is the Borel sigma-algebra), so the invariance hypothesis is applied only where it is unambiguously meaningful.

Facts & Assumptions

Given: A natural number $n \geq 1$ , a natural number $k$ , and a measure $μ$ on the Borel sets of $R^{n}$ that is translation invariant and gives the unit cube measure $1$ .

[L1]

$Q_{k, m} = {x \in R^{n} : m_{i} 2^{- k} < x_{i} \leq (m_{i} + 1) 2^{- k} for every i < n}$ , and $Q_{0, 0} = (0, 1]^{n}$ (Dyadic cubes of generation $k$ in $R^{n}$ , Half-open boxes in $R^{n}$ and their volume, Integer powers $a^{m}$ ).

[L2]

Every $x \in R^{n}$ lies in exactly one dyadic cube of generation $k$ (For each generation, the dyadic cubes of that generation are pairwise disjoint and cover $R^{n}$ ).

[L3]

Every half-open box is a Borel set (The sigma-algebra generated by the half-open boxes of $R^{n}$ is the Borel sigma-algebra).

[F1]

A measure on $(X, A)$ is a function $μ : A \to [0, + \infty]$ with $μ (\emptyset) = 0$ that is countably additive on pairwise disjoint sequences (Measures on sigma-algebras); padding a finite disjoint list with empty sets makes it finitely additive.

[F2]

The translate of $E \subseteq R^{n}$ by $a$ is $E + a : = {x + a : x \in E}$ (Translation of a subset of $R^{n}$ ).

[F3]

$\sum_{k < n} λ = n λ$ , where $n$ denotes the canonical natural of $R$ (Laws of finite sums and finite products, claim 2; Finite sums and finite products, by recursion).

[F4]

For $a \neq 0$ and $m, n \in Z$ , $a^{m + n} = a^{m} a^{n}$ and $(a^{m})^{n} = a^{m n}$ (Laws of integer exponents, claims 1 and 3; Integer powers $a^{m}$ ).

[F5]

Let $S \subseteq N$ ; if $0 \in S$ and $σ (n) \in S$ whenever $n \in S$ , then $S = N$ (The principle of mathematical induction).

[F6]

The order on $Z$ is total and compatible with addition (The integers form a totally ordered ring); the canonical embedding of $N$ into $Z$ has as image exactly the nonnegative integers (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals); and $m < n$ in $N$ exactly when $σ (m) \leq n$ (Discreteness: $σ (n)$ is the immediate successor).

Proof

technique · direct

1.1L1L2F4F6

A generation- $k$ dyadic cube is contained in $(0, 1]^{n}$ exactly when $0 \leq m_{i}$ and $m_{i} + 1 \leq 2^{k}$ for every $i < n$ , and every point of $(0, 1]^{n}$ lies in such a cube: if $x \in (0, 1]^{n}$ and $m$ is the index of the generation- $k$ cube containing $x$ , then $m_{i} < 2^{k} x_{i} \leq 2^{k}$ and $m_{i} + 1 \geq 2^{k} x_{i} > 0$ , so $0 \leq m_{i}$ and $m_{i} + 1 \leq 2^{k}$ by discreteness of $Z$ ; conversely such a cube lies in $(0, 1]^{n}$ because $m_{i} 2^{- k} \geq 0$ and $(m_{i} + 1) 2^{- k} \leq 1$ .

1.2L1L3F2

Every generation- $k$ dyadic cube is a translate of $Q_{k, 0} = (0, 2^{- k}]^{n}$ , namely $Q_{k, m} = Q_{k, 0} + m 2^{- k}$ , and it is a half-open box, hence Borel; so all generation- $k$ cubes receive the same value under $μ$ .

2.1F4F5F6

The indices admitted in step 1.1 are exactly the functions from $n$ to the set ${j \in N : j < 2^{k}}$ , and there are $2^{k n}$ of them: by induction on $n$ , at $n = 0$ there is exactly one such function and $2^{0} = 1$ , while each function on $n + 1$ coordinates is a function on $n$ coordinates together with one of $2^{k}$ values in the new coordinate, so the count is multiplied by $2^{k}$ and $(2^{k})^{n} \cdot 2^{k} = (2^{k})^{n + 1} = 2^{k (n + 1)}$ .

3.1step 1.1step 1.2step 2.1L2F1F3

By steps 1.1 and 2.1 the cube $(0, 1]^{n}$ is the union of a list of $2^{k n}$ pairwise disjoint generation- $k$ dyadic cubes, so finite additivity and step 1.2 give $1 = μ ((0, 1]^{n}) = \sum_{r < 2^{k n}} μ (Q_{k, 0})$ ; no term can be $+ \infty$ , since then the sum would be $+ \infty$ rather than $1$ , so the common value is a real and the sum is $2^{k n} μ (Q_{k, 0})$ .

4.1step 1.2step 3.1F4∎

Dividing by the strictly positive real $2^{k n}$ gives $μ (Q_{k, 0}) = 2^{- k n}$ , and step 1.2 transfers the value to every generation- $k$ dyadic cube.

Depends on

Used by

A translation-invariant measure on the Borel sets of ℝⁿ giving the unit cube measure one is the restriction of Lebesgue measure Theorem

Dependency tree · two levels

75 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.2.23 (standard reference, not scraped)
E. A. Carlen, Notes on Lebesgue Measure on $\mathbb{R}^n$ and $S^{n-1}$ (Rutgers Math 501), Theorem 2.3 (standard reference, not scraped)

A translation-invariant Borel measure giving the unit cube measure one gives each generation-kk dyadic cube measure 2−kn2−kn