Erdős Problem 120

Reference:

• erdosproblems.com/120
• St20 Steinhaus, Hugo, Sur les distances des points dans les ensembles de measure positive. Fund. Math. (1920), 93-104.

def Erdos120.Erdos120For (A : Set ℝ) : Prop

There exists a set $E \subseteq \mathbb{R}$, dependent on set $A \subseteq \mathbb{R}$, of positive measure which does not contain any set of the shape $a * A + b$ for some $a,b \in \mathbb{R}$ and $a \neq 0$?

Equations

• Erdos120.Erdos120For A = ∃ (E : Set ℝ), 0 < MeasureTheory.volume E ∧ ∀ (a b : ℝ), a ≠ 0 ∧ ¬(fun (x : ℝ) => a * x + b) '' A ⊆ E

theorem Erdos120.erdos_120 : sorry ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120For A

Let $A \subseteq \mathbb{R}$ be an infinite set. Must there be a set $E \subseteq \mathbb{R}$ of positive measure which does not contain any set of the shape $a * A + b$ for some $a,b \in \mathbb{R}$ and $a \neq 0$?

theorem Erdos120.erdos_120.variants.finite_set {A : Set ℝ} (h : A.Finite) : ¬Erdos120For A

Steinhaus [St20] has proved Erdős 120 to be false whenever $A$ is a finite set.