Littlewood conjecture

DefinitionDistance to the nearest integer#✓fully proved

For a real number \(x\), this is \(|x - r|\), where \(r\) is the integer nearest to \(x\) (halves rounded up); equivalently, it is the minimum of \(|x - n|\) over all integers \(n\).

noncomputable def distToNearestInt (x : ℝ) : ℝ := |x - round x|

Used by 1

Used byEinsiedler–Katok–Lindenstrauss theorem

TheoremEinsiedler–Katok–Lindenstrauss theorem#●ready to prove

For a real number \(x\), write \(\lVert x \rVert\) for the distance from \(x\) to the nearest integer. The set of pairs \((\alpha, \beta)\) of real numbers with \(\liminf_{n \to \infty} n \cdot \lVert n\alpha \rVert \cdot \lVert n\beta \rVert > 0\), the lower limit taken over natural numbers \(n\), has Hausdorff dimension \(0\) in \(\mathbb{R}^2\).

public theorem_wanted einsiedler_katok_lindenstrauss :
    dimH {(α, β) : ℝ × ℝ | Filter.atTop.liminf
      (fun n : ℕ ↦ n * distToNearestInt (n * α) * distToNearestInt (n * β)) > 0} = 0

Sources

-. Problem einsiedler_katok_lindenstrauss of the lean-eval benchmark.

Uses 1

Statement usesDistance to the nearest integer

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.