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 measure on the Borel sets of giving the unit cube measure one is the restriction of Lebesgue measure
Statement
Let and assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let be a measure on (Measures on sigma-algebras) such that for every Borel set and every , and . Then
The hypothesis is meaningful because a translate of a Borel set is Borel, and it is satisfied by the restriction of to , so the theorem says that measure is the only one satisfying it. Finiteness on bounded sets is a consequence of the normalisation, not a further hypothesis.
Facts & Assumptions
Given: A natural number , the Axiom of Countable Choice, and a translation-invariant measure on with .
If is a measure on the Borel sets of that is translation invariant and gives the unit cube measure , then for every dyadic cube of generation (A translation-invariant Borel measure giving the unit cube measure one gives each generation- dyadic cube measure , Dyadic cubes of generation in ).
Every open is the union of an at most countable family of pairwise disjoint dyadic cubes (Every open subset of is the union of a countable pairwise disjoint family of dyadic cubes).
Assuming countable choice, every Borel subset of is Lebesgue measurable (Assuming countable choice, every Borel subset of is Lebesgue measurable) and is a measure on with for every half-open box (Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume).
Every set with is Lebesgue measurable with (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included).
for every subset , is Lebesgue measurable if and only if is, and for measurable (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, Translation of a subset of ).
Let be a pi-system on generating , and let be measures on that agree on ; suppose there is an increasing sequence in with and for every ; then on (Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system).
A pi-system on is a nonempty family closed under binary intersections (Pi-systems).
The Borel sigma-algebra of is the sigma-algebra generated by its open sets (The Borel sigma-algebra of a topological space), and is the unique smallest sigma-algebra on containing (Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal); a sigma-algebra is closed under complements and countable unions (Sigma-algebras).
A subset is open in when every has a ball (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space); a finite intersection of open sets is open (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, claim 3); and is a metric on ( as the set of functions , and , , are metrics on it).
A measure is countably additive on pairwise disjoint measurable sequences (Measures on sigma-algebras), and an at most countable family may be presented as a sequence (Finite, countably infinite, countable, uncountable).
Every complete ordered field is Archimedean: for every there is a natural number with (Every complete ordered field is Archimedean).
Proof
A translate of a Borel set is Borel: the family of whose translate is Borel contains every open set, since makes and hence open for open , and it is a sigma-algebra because translation commutes with complements and with countable unions; minimality of over the open sets finishes it.
The open subsets of form a pi-system generating : the family is nonempty and closed under binary intersections, and the Borel sigma-algebra is by definition the one it generates.
The restriction of to the Borel sets is a measure satisfying the two hypotheses, by translation invariance and by .
By the dyadic lemma both and give a generation- dyadic cube the value , the latter because a dyadic cube is a half-open box of that volume.
Both measures therefore agree on every open set: such a set is the union of an at most countable pairwise disjoint family of dyadic cubes, which may be presented as a sequence, and countable additivity gives the same value for the two measures.
The open cubes form an increasing sequence of open sets with union , by the Archimedean property, and by step 3.1 and the box theorem; the uniqueness theorem for a sigma-finite generating pi-system therefore gives on , and step 1.1 makes the invariance hypothesis meaningful throughout.
Depends on
A translation-invariant Borel measure giving the unit cube measure one gives each generation- dyadic cube measure
Every open subset of is the union of a countable pairwise disjoint family of dyadic cubes
Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system
Pi-systems
The Borel sigma-algebra of a topological space
Sigma-algebras
Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal
Assuming countable choice, every Borel subset of is Lebesgue measurable
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume
Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
For each generation, the dyadic cubes of that generation are pairwise disjoint and cover
Dyadic cubes of generation in
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed
as the set of functions , and , , are metrics on it
Open ball, closed ball and sphere in a metric space
Translation of a subset of
Measures on sigma-algebras
Finite, countably infinite, countable, uncountable
Every complete ordered field is Archimedean
The Axiom of Countable Choice ()