Ben Green's Open Problem 94

Reference:

• Ben Green's Open Problem 94
• erdosproblems.com/120

theorem Green94.green_94_outer_measure : False ↔ ∀ (A : Set ℝ), MeasureTheory.volume A > 0 → ∃ (a : ℝ) (b : ℝ), a ≠ 0 ∧ ∀ (n : ℕ), a * (1 / 2 ^ n) + b ∈ A

Let A ⊂ R be a set of positive outer measure. Does $A$ contain an affine copy of {1, 1/2, 1/4, . . . }?

The answer is "no".

theorem Green94.green_94 : True ↔ ∀ (A : Set ℝ), MeasurableSet A ∧ MeasureTheory.volume A > 0 → ∃ (a : ℝ) (b : ℝ), a ≠ 0 ∧ ∀ (n : ℕ), a * (1 / 2 ^ n) + b ∈ A

Let A ⊂ R be a set of positive measure. Does $A$ contain an affine copy of {1, 1/2, 1/4, . . . }?