Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

If a Lebesgue measurable subset of Rn has positive measure, its difference set contains an open ball about the origin

Statement

Let n≥1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let E⊆Rn be Lebesgue measurable with λn(E)>0, and put

E−E  :=  { x−y  :  x,y∈E }.

Then there is a real r>0 with B(0,r)⊆E−E, the open Euclidean ball of centre the origin and radius r (Open ball, closed ball and sphere in a metric space, Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it).

Facts & Assumptions

Given: A natural number n≥1, the Axiom of Countable Choice, and a Lebesgue measurable set E⊆Rn with λn(E)>0.

[L1]

Assuming countable choice, a Lebesgue measurable F with 0<λn(F)<+∞ and a real θ with 0<θ<1 admit a dyadic cube Q with λn(F∩Q)>θ λn(Q) (A measurable set of positive finite measure occupies more than any prescribed proportion of some dyadic cube, Dyadic cubes of generation k in Rn).

[L2]

λn(S+h)=λn(S) for every Lebesgue measurable S and every h, and S+h is measurable exactly when S is (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation, Translation of a subset of Rn).

[F1]

Let (Ek)k∈N be an increasing sequence of measurable sets for a measure μ; then μ(⋃k∈NEk)=sup⁡k∈Nμ(Ek) (Continuity from below for measures).

[F2]

A measure is countably additive on pairwise disjoint measurable sequences, hence finitely additive (Measures on sigma-algebras), and monotone (Measures are monotone).

[F3]

For a>0 and rational r=m/q with q≥1, ar:=(a1/q)m, where a1/q is the unique nonnegative q-th root of a (Rational powers ar of a positive base, Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a), and the value does not depend on the representative (Rational powers do not depend on the representative).

[F4]

If 0≤a<b and n≥1 then an<bn; if 0≤a≤1 then an≤1 (Monotonicity of x↦xn and of n↦an, claims 2 and 3; Integer powers am), and (ab)n=anbn (Laws of integer exponents, claim 1).

Proof

technique · direct
1.1L3L4F1

The sets E∩(−k,k]n for k∈N are Lebesgue measurable, increase with k and have union E, so continuity from below gives sup⁡kλn(E∩(−k,k]n)=λn(E)>0 and some k has λn(E∩(−k,k]n)>0; that set is bounded, hence of finite measure. Replacing E by it shrinks E−E, so it suffices to prove the theorem when 0<λn(E)<+∞.

1.2F3F4

Put t:=(3/2)1/n, the unique nonnegative n-th root of 3/2; then t>1, since t≤1 would give t n≤1<3/2, and η:=(t−1)/2 is a strictly positive real with 1+2η=t and (1+2η)n=3/2.

2.1step 1.1L1L3

Assume 0<λn(E)<+∞ and apply the density lemma with θ:=3/4: there is a dyadic cube Q, of some generation k and side s:=2−k, with λn(E∩Q)>34s n, since λn(Q)=s n.

3.1step 1.2step 2.1L2L3F4F5

Let h∈Rn with d2(0,h)<ηs, so that ∣hi∣<ηs in every coordinate. Writing Q=B(a,b) with bi−ai=s, both E∩Q and (E∩Q)+h are contained in the half-open box P with parameter pairs (ai−ηs, bi+ηs], whose measure is (s(1+2η))n=s nt n=32s n.

4.1step 2.1step 3.1L2L4F2

The two sets are Lebesgue measurable with the same measure, by translation invariance, so if they were disjoint then additivity and monotonicity inside P would give 32s n=λn(P)≥2λn(E∩Q)>2⋅34s n=32s n, which is impossible; hence they meet, and a common point z=w+h with z,w∈E∩Q exhibits h=z−w∈E−E.

5.1step 1.2step 4.1F5∎

Therefore B(0,ηs)⊆E−E, and r:=ηs is a strictly positive real.

Depends on

Used by

Dependency tree · two levels

126 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