Erdős problem 464
Let be a lacunary sequence (so there exists some with for all ). Must there exist an irrational such that is not dense in (where is the distance to the nearest integer)?
Sources
FormalConjectures/ErdosProblems/
464.lean
Let be a lacunary sequence (so there exists some with for all ). Must there exist an irrational such that is not dense in (where is the distance to the nearest integer)?
Solved independently by de Mathan [dM80] and Pollington [Po79b], who showed that, given any such , there exists such a , with This bound was improved by Katznelson [Ka01], Akhunzhanov and Moshchevitin [AkMo04], and Dubickas [Du06], before Peres and Schlag [PeSc10] improved it to and note that the best bound possible here would be .
This problem has consequences for [894](https://www.erdosproblems.com/894).
The conclusion " is not dense in " is formalized as the sequence not being dense modulo one; see the formalization notes above.
True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (k : ℕ), 0 < n k) → IsLacunary n → ∃ θ, Irrational θ ∧ ¬Dense (Set.range fun k => ↑(θ * ↑(n k)))