Erdős Problem 354

Reference: erdosproblems.com/354

noncomputable def Erdos354.FloorMultiples (a γ : ℝ) (n : ℕ) : ℤ

The sequence ⌊a⌋, ⌊γ * a⌋, ⌊γ ^ 2 * a⌋, ..., ⌊γ ^ i * a⌋, ....

Equations

• Erdos354.FloorMultiples a γ n = ⌊γ ^ n * a⌋

noncomputable def Erdos354.FloorMultiples.interleave (a b γ : ℝ) (n : ℕ) : ℤ

The sequence ⌊a⌋, ⌊b⌋, ⌊γ * a⌋, ⌊γ * b⌋, ... ⌊γ ^ i * a⌋, ⌊γ ^ i * b⌋, ...

Equations

• Erdos354.FloorMultiples.interleave a b γ n = if n % 2 = 0 then Erdos354.FloorMultiples a γ (n / 2) else Erdos354.FloorMultiples b γ (n / 2)

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

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?

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

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?