Ben Green's Open Problem 94

Reference:

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

theorem Green94.green_94 : sorry ↔ ∀ (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 measure. Does $A$ contain an affine copy of {1, 1/2, 1/4, . . . }?