Erdős Problem 354

Reference: erdosproblems.com/354

def Erdos354.FloorMultiples (a γ : ℝ) : Set ℝ

The set {⌊a⌋, ⌊2 * a⌋, ⌊4 * a⌋, ...}.

Equations

• Erdos354.FloorMultiples a γ = Set.range fun (n : ℕ) => ↑⌊γ ^ n * a⌋

theorem Erdos354.erdos_354.parts.i : (∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddComplete (FloorMultiples α 2 ∪ FloorMultiples β 2)) ↔ sorry

Let $\alpha,\beta\in \mathbb{R}_{>0}$ such that $\alpha/\beta$ is irrational. Is [{ \lfloor \alpha\rfloor,\lfloor 2\alpha\rfloor,\lfloor 4\alpha\rfloor,\ldots}\cup { \lfloor \beta\rfloor,\lfloor 2\beta\rfloor,\lfloor 4\beta\rfloor,\ldots}] complete?

theorem Erdos354.erdos_354.parts.ii : (∃ γ ∈ Set.Ioo 1 2, ∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddComplete (FloorMultiples α γ ∪ FloorMultiples β γ)) ↔ sorry

Let $\alpha,\beta\in \mathbb{R}_{>0}$ such that $\alpha/\beta$ is irrational. Is [{ \lfloor \alpha\rfloor,\lfloor \gamma\alpha\rfloor,\lfloor \gamma^2\alpha\rfloor,\ldots}\cup { \lfloor \beta\rfloor,\lfloor \gamma\beta\rfloor,\lfloor \gamma^2\beta\rfloor,\ldots}] complete?