Documentation

FormalConjectures.ErdosProblems.«107»

Erdős Problem 107 #

References:

source
def Erdos107.cardSet (n : ℕ) :
Set ℕ

The set of $N$ such that any $N$ points in the plane, no three on a line, contain a convex $n$-gon.

Equations
Instances For
    source
    noncomputable def Erdos107.f (n : ℕ) :
    ℕ

    The function $f(n)$ specified in erdos_107.

    Equations
    Instances For
      source
      theorem Erdos107.erdos_107 :
      (∀ n ≥ 3, f n = 2 ^ (n - 2) + 1) ↔ sorry

      Let $f(n)$ be minimal such that any $f(n)$ points in $ℝ^2$, no three on a line, contain $n$ points which form the vertices of a convex $n$-gon. Prove that $f(n) = 2^{n-2} + 1$.

      source
      theorem Erdos107.nonempty_cardSet (n : ℕ) :
      n ≥ 3 → (cardSet n).Nonempty

      For every $n ≥ 3$, there exists $N$ such that any $N$ points, no three on a line, contain a convex $n$-gon.

      source
      theorem Erdos107.f_zero_eq :
      f 0 = 0

      Depending on details of definitions, the statement is false or trivial for $n < 3$.

      source
      theorem Erdos107.f_three_eq :
      f 3 = 3
      source
      theorem Erdos107.variants.ersz_bounds (n : ℕ) :
      n ≥ 3 → 2 ^ (n - 2) + 1 ≤ f n ∧ f n ≤ (2 * n - 4).choose (n - 2) + 1

      Erdős and Szekeres proved the bounds $$ 2^{n-2} + 1 ≤ f(n) ≤ \binom{2n-4}{n-2} + 1 $$ ([ErSz60] and [ErSz35] respectively).

      [ErSz60] Erdős, P. and Szekeres, G., On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. (1960/61), 53-62.

      [ErSz35] Erdős, P. and Szekeres, G., A combinatorial problem in geometry. Compos. Math. (1935), 463-470.

      source
      theorem Erdos107.variants.su_bound :
      ∃ (r : ℕ → ℝ), (r =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ ∀ n ≥ 3, ↑(f n) ≤ 2 ^ (↑n + r n)

      Suk [Su17] proved $$ f(n) ≤ 2^{(1+o(1))n}. $$

      [Su17] Suk, Andrew, On the Erdős-Szekeres convex polygon problem. J. Amer. Math. Soc. (2017), 1047-1053.

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

      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.