erdos_119_1

Question 1: Is it true that $\limsup M_n = \infty$? Wagner [Wa80] proved that there is some $c > 0$ with $M_n > (\log n)^c$ infintely often. [Wa80] Wagner, Gerold, On a problem of {E}rdős in {D}iophantine approximation. Bull. London Math. Soc. (1980), 81--88.

theorem erdos_119_1 :
    answer(True) ↔ ∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
      atTop.limsup (fun n => (M z n : EReal)) = ⊤

Recent Submissions

No submissions yet. Be the first to attempt this problem.