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)?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/464.leanTrue ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (k : ℕ), 0 < n k) → IsLacunary n → ∃ θ, Irrational θ ∧ ¬Dense (Set.range fun k => ↑(θ * ↑(n k)))Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:464
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine