Littlewood conjectures

References:

• Wikipedia
• [Bernard Mathan and Olivier Touli´e, Problem`emes diophantiens simultan´es][mathantoilie2004]

@[reducible, inline]

noncomputable abbrev LittlewoodConjecture.distToNearestInt (x : ℝ) : ℝ

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

Equations

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

theorem LittlewoodConjecture.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 $\||x\|| := \min(|x - \lfloor x \rfloor|, |x - \lceil x \rceil|)$ is the distance to the nearest integer.

theorem LittlewoodConjecture.padic_littlewood_conjecture (α : ℝ) (p : ℕ) (hp : Nat.Prime p) : Filter.liminf (fun (n : ℕ) => ↑n * ↑(padicNorm p ↑n) * distToNearestInt (↑n * α)) Filter.atTop = 0

For real number $\alpha$ and prime $p$, $$ \liminf_{n \to\infty} n |n|_{p}\||n\alpha\|| = 0 $$ where $\||x\|| := \min(|x - \lfloor x \rfloor|, |x - \lceil x \rceil|)$ is the distance to the nearest integer, and $|x|_{p}$ is the $p$-adic norm.