Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation

Statement

Let n1, let hRn, and let E+h be the translate of ERn (Translation of a subset of Rn). Then:

  1. λn(E+h)=λn(E) for every subset E;
  2. E is Lebesgue measurable if and only if E+h is;
  3. λn(E+h)=λn(E) for every Lebesgue measurable E.

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 λn is a measure, not to know that it is translation invariant.

Facts & Assumptions

Given: A natural number n1, a vector hRn, and a subset ERn.

[L1]

λn(E):=inf{k=0μ0(Ak):AkEn for every k and EkAk} (Lebesgue outer measure on Rn, Series in the nonnegative extended real line).

[L2]

B(a,b):={xRn:ai<xibi  for every i<n}; a box is nonempty exactly when ai<bi for every i<n; and for a nonempty box with real parameters vol(B):=i<n(biai), the value being + when a parameter is infinite (Half-open boxes in Rn and their volume).

[L3]

A subset ERn is an elementary set when there are a natural number m and a list B0,,Bm1 of half-open boxes with E=j<mBj (Elementary sets: the finite unions of half-open boxes in Rn), 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).

[L4]

For every n1, elementary volume μ0 on En has value at A the sum of the volumes of the members of any presentation of A 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).

[L5]

A set E is Lebesgue measurable when λn(A)=λn(AE)+λn(AE) for every ARn, and λn is the restriction of λn to the family of these (Lebesgue measurable sets, the family L(Rn), and the restricted set function λn, Carathéodory measurable sets).

[F1]

The translate of ERn by a is E+a:={x+a:xE}; translation by a is the bijection τa(x)=x+a, whose inverse is τa (Translation of a subset of Rn).

[F2]

Addition of a real to an extended real is defined in every case, with a+b:=+ when a=+ and b, and a+b:= when a= and b+ (The extended real line R=R{,+}, its order, and the arithmetic that is left undefined).

Proof

technique · direct
1.1

For a parameter pair (a,b) one has B(a,b)+h=B(a+h,b+h), where a+h is the parameter iai+hi: a point y lies in the left side exactly when yh satisfies ai<yihibi, that is ai+hi<yibi+hi. The translated box is empty exactly when the original is, and has the same volume, because (bi+hi)(ai+hi)=biai when both are real and an infinite parameter stays infinite.

L2F1F2
2.1

Consequently, if A=j<qBj is a presentation of an elementary set by pairwise disjoint half-open boxes, then A+h=j<q(Bj+h) is such a presentation of A+h, so A+h is elementary and μ0(A+h)=μ0(A).

step 1.1L3L4
3.1

A sequence (Ak) of elementary sets covers E if and only if the sequence (Ak+h) covers E+h, 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 h, so the two infima agree and λn(E+h)=λn(E).

step 2.1L1F1
4.1

For test sets, A(E+h)=((Ah)E)+h and A(E+h)=((Ah)E)+h, so by step 3.1 the Carathéodory identity for E+h tested against A is exactly the identity for E tested against Ah; as A ranges over all subsets so does Ah, and therefore E+h is Lebesgue measurable if and only if E is, with λn(E+h)=λn(E+h)=λn(E)=λn(E) in that case.

step 3.1L5F1

Depends on

Used by

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