Skip to content

Erdős problem 354

Let α,β∈R>0\alpha,\beta\in \mathbb{R}_{>0} such that α/β\alpha/\beta is irrational. Is {⌊α⌋,⌊γα⌋,⌊γ2α⌋,…}∪{⌊β⌋,⌊γβ⌋,⌊γ2β⌋,…}\{ \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?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

354.lean

Retained formal statement2 of 2

Let α,β∈R>0\alpha,\beta\in \mathbb{R}_{>0} such that α/β\alpha/\beta is irrational. Is {⌊α⌋,⌊γα⌋,⌊γ2α⌋,…}∪{⌊β⌋,⌊γβ⌋,⌊γ2β⌋,…}\{ \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?

FormalConjectures/ErdosProblems/354.leanErdos354.erdos_354.parts.ii3 linesExact file
True ↔  ∃ γ ∈ Set.Ioo 1 2,    ∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page