Smallness of exceptional set to Littlewood's conjecture

Problem statement

Notes: Unavailable.

Source: Unavailable.

Informal solution: Unavailable.

theorem declaration uses `sorry`einsiedler_katok_lindenstrauss :
    dimH {(α, β) : ℝ × ℝ | Filter.atTop.liminf
      (fun n : ℕ ↦ n * distToNearestInt (n * α) * distToNearestInt (n * β)) > 0} = 0 := by⊢ dimH {(α, β) | Filter.liminf (fun n => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop > 0} = 0
  sorryAll goals completed! 🐙