Skip to content

Erdős problem 495

Start work

Let α,β∈R\alpha,\beta \in \mathbb{R}. Is it true thatlim inf⁡n→∞n∥nα∥∥nβ∥=0\liminf_{n\to \infty} n \| n\alpha \| \| n\beta\| =0? This is also known as the Littlewood conjecture.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

495.lean

Retained formal statement1 of 1

Let α,β∈R\alpha,\beta \in \mathbb{R}. Is it true thatlim inf⁡n→∞n∥nα∥∥nβ∥=0\liminf_{n\to \infty} n \| n\alpha \| \| n\beta\| =0? This is also known as the Littlewood conjecture.

FormalConjectures/ErdosProblems/495.leanErdos495.erdos_4951 lineExact file
True ↔ ∀ (α β : ℝ), Filter.liminf (fun n => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop = 0
OpenStatement only, no proof