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.
Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
Statement
Let , let , and let be the translate of (Translation of a subset of ). Then:
- for every subset ;
- is Lebesgue measurable if and only if is;
- for every Lebesgue measurable .
No choice principle is used. Lebesgue outer measure is defined as an infimum and the Carathéodory condition is a family of equations between its values, so all three clauses are statements about objects that exist in ZF; countable choice is needed to know that is a measure, not to know that it is translation invariant.
Facts & Assumptions
Given: A natural number , a vector , and a subset .
for every and (Lebesgue outer measure on , Series in the nonnegative extended real line).
; a box is nonempty exactly when for every ; and for a nonempty box with real parameters , the value being when a parameter is infinite (Half-open boxes in and their volume).
A subset is an elementary set when there are a natural number and a list of half-open boxes with (Elementary sets: the finite unions of half-open boxes in ), and every elementary set is the union of a finite list of pairwise disjoint half-open boxes (Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement).
For every , elementary volume on has value at the sum of the volumes of the members of any presentation of by a finite list of pairwise disjoint half-open boxes (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition).
A set is Lebesgue measurable when for every , and is the restriction of to the family of these (Lebesgue measurable sets, the family , and the restricted set function , Carathéodory measurable sets).
The translate of by is ; translation by is the bijection , whose inverse is (Translation of a subset of ).
Addition of a real to an extended real is defined in every case, with when and , and when and (The extended real line , its order, and the arithmetic that is left undefined).
Proof
For a parameter pair one has , where is the parameter : a point lies in the left side exactly when satisfies , that is . The translated box is empty exactly when the original is, and has the same volume, because when both are real and an infinite parameter stays infinite.
Consequently, if is a presentation of an elementary set by pairwise disjoint half-open boxes, then is such a presentation of , so is elementary and .
A sequence of elementary sets covers if and only if the sequence covers , and the two covering costs are equal by step 2.1; the correspondence is a bijection between the two families of covers, with inverse given by translating by , so the two infima agree and .
For test sets, and , so by step 3.1 the Carathéodory identity for tested against is exactly the identity for tested against ; as ranges over all subsets so does , and therefore is Lebesgue measurable if and only if is, with in that case.
Depends on
- Lebesgue outer measure on $\mathbb{R}^n$
- Half-open boxes in $\mathbb{R}^n$ and their volume
- Elementary sets: the finite unions of half-open boxes in $\mathbb{R}^n$
- The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition
- Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement
- Translation of a subset of $\mathbb{R}^n$
- Lebesgue measurable sets, the family $\mathcal{L}(\mathbb{R}^n)$, and the restricted set function $\lambda_n$
- Carathéodory measurable sets
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Series in the nonnegative extended real line
Used by
- A shear sends the unit cube to a set of Lebesgue measure one Lemma
- A translation-invariant measure on the Borel sets of ℝⁿ giving the unit cube measure one is the restriction of Lebesgue measure 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
37 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
- John K. Hunter, Measure Theory (UC Davis lecture notes), Proposition 2.16 (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)