Littlewood conjecture

Reference: Wikipedia

@[reducible, inline]

noncomputable abbrev distToNearestInt (x : ℝ) : ℝ

The distance to the nearest integer is the function $\||x\|| := \min(|x - \lfloor x \rfloor|, |x - \lceil x \rceil|)$.

Equations

• distToNearestInt x = |x - ↑(round x)|

theorem littlewood_conjecture (α β : ℝ) : Filter.liminf (fun (n : ℕ) => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop = 0

For any two real numbers $\alpha$ and $\beta$, $$ \liminf_{n\to\infty} n\||n\alpha\||\||n\beta\|| = 0 $$ where $\||nx\|| := \min(|x - \lfloor x \rfloor|, |x - \lceil x \rceil|)$ is the distance to the nearest integer.