hmpt_bound

The current best bound is due to Holmsen, Mojarrad, Pach, and Tardos [HMPT20], who prove $$ f(n) ≤ 2^{n+O(\sqrt{n\log n})}. $$ [HMPT20] Holmsen, Andreas F. and Mojarrad, Hossein Nassajian and Pach, János and Tardos, Gábor, _Two extensions of the Erdős-Szekeres problem_. J. Eur. Math. Soc. (JEMS) (2020), 3981-3995.

theorem hmpt_bound :
    ∃ r : ℕ → ℝ, r =O[atTop] (fun n => Real.sqrt (n * Real.log n)) ∧
      ∀ n ≥ 3, (f n : ℝ) ≤ 2^(n + r n)

Recent Submissions

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