Skip to content

Erdős problem 495

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

495.lean

Retained formal statement1 of 1

Let α,βR\alpha,\beta \in \mathbb{R}. Is it true thatlim infnnnα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

Search problems.science

Find a Problem, Result, source, or page