Erdős Problem 495

Reference: erdosproblems.com/495

noncomputable def Erdos495.distNearestInt (x : ℝ) : ℝ

The distance from x to the nearest integer, denoted $\|x\|$.

Equations

• Erdos495.distNearestInt x = |x - ↑(round x)|

theorem Erdos495.erdos_495 : sorry ↔ ∀ (α β : ℝ), Filter.liminf (fun (n : ℕ) => ↑n * distNearestInt (↑n * α) * distNearestInt (↑n * β)) Filter.atTop = 0

Let $\alpha,\beta \in \mathbb{R}$. Is it true that[\liminf_{n\to \infty} n | n\alpha | | n\beta| =0]? This is also known as the Littlewood conjecture.