Skip to content

Erdős problem 464

Let A={n1<n2<}NA=\{n_1<n_2<\cdots\}\subset \mathbb{N} be a lacunary sequence (so there exists some ϵ>0\epsilon>0 with nk+1(1+ϵ)nkn_{k+1}\geq (1+\epsilon)n_k for all kk). Must there exist an irrational θ\theta such that {θnk:k1}\{ \|\theta n_k\| : k\geq 1\} is not dense in [0,1][0,1] (where x\| x\| is the distance to the nearest integer)?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

464.lean

Retained formal statement1 of 1

Let A={n1<n2<}NA=\{n_1<n_2<\cdots\}\subset \mathbb{N} be a lacunary sequence (so there exists some ϵ>0\epsilon>0 with nk+1(1+ϵ)nkn_{k+1}\geq (1+\epsilon)n_k for all kk). Must there exist an irrational θ\theta such that {θnk:k1}\{ \|\theta n_k\| : k\geq 1\} is not dense in [0,1][0,1] (where x\| x\| is the distance to the nearest integer)?

Solved independently by de Mathan [dM80] and Pollington [Po79b], who showed that, given any such AA, there exists such a θ\theta, with infk1θnkϵ4log(1/ϵ).\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon^4}{\log(1/\epsilon)}. This bound was improved by Katznelson [Ka01], Akhunzhanov and Moshchevitin [AkMo04], and Dubickas [Du06], before Peres and Schlag [PeSc10] improved it to infk1θnkϵlog(1/ϵ),\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon}{\log(1/\epsilon)}, and note that the best bound possible here would be ϵ\gg \epsilon.

This problem has consequences for [894](https://www.erdosproblems.com/894).

The conclusion "{θnk}\{\|\theta n_k\|\} is not dense in [0,1][0,1]" is formalized as the sequence (θnk)(\theta n_k) not being dense modulo one; see the formalization notes above.

FormalConjectures/ErdosProblems/464.leanErdos464.erdos_4643 linesExact file
True  ∀ (n : ℕ → ℕ),    StrictMono n → (∀ (k : ℕ), 0 < n k) → IsLacunary n → ∃ θ, Irrational θ ∧ ¬Dense (Set.range fun k => ↑(θ * ↑(n k)))
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page