Erdős Problem 920

References:

• erdosproblems.com/166
• erdosproblems.com/920
• erdosproblems.com/986
• erdosproblems.com/1104
• [GrYa68] Graver, Jack E. and Yackel, James, Some graph theoretic results associated with Ramsey's theorem. J. Combinatorial Theory (1968), 125--175.
• [MaVe23] Mattheus, S. and Verstraete, J., The asymptotics of $r(4,t)$. arXiv:2306.04007 (2023).

noncomputable def Erdos920.f (k n : ℕ) : ℕ

$f_k(n)$ is the maximum possible chromatic number of a graph with $n$ vertices which contains no $K_k$.

Equations

• Erdos920.f k n = sSup {x : ℕ | ∃ (G : SimpleGraph (Fin n)) (_ : G.CliqueFree k), G.chromaticNumber = ↑x}

theorem Erdos920.erdos_920 : sorry ↔ ∀ k ≥ 4, ∃ c > 0, (fun (n : ℕ) => ↑n ^ (1 - 1 / (↑k - 1)) / Real.log ↑n ^ c) =O[Filter.atTop] fun (n : ℕ) => ↑(f k n)

Is it true that, for $k\geq 4$, $f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}$ for some constant $c_k>0$?

theorem Erdos920.erdos_920.variants.upper_bound (k : ℕ) (hk : k ≥ 3) : (fun (n : ℕ) => ↑(f k n)) =O[Filter.atTop] fun (n : ℕ) => (↑n * Real.log (Real.log ↑n) / Real.log ↑n) ^ (1 - 1 / (↑k - 1))

Graver and Yackel [GrYa68] proved that $f_k(n) \ll \left(n\frac{\log\log n}{\log n}\right)^{1-\frac{1}{k-1}}.$

theorem Erdos920.erdos_920.variants.k_eq_3 : (fun (n : ℕ) => ↑(f 3 n)) =Θ[Filter.atTop] fun (n : ℕ) => (↑n / Real.log ↑n) ^ (1 / 2)

It is known that $f_3(n)\asymp (n/\log n)^{1/2}$ (see [erdosproblems.com/1104]).

theorem Erdos920.erdos_920.variants.lower_bound_f4 : (fun (n : ℕ) => ↑n ^ (2 / 3) / Real.log ↑n ^ (4 / 3)) =O[Filter.atTop] fun (n : ℕ) => ↑(f 4 n)

The lower bound $R(4,m) \gg m^3/(\log m)^4$ of Mattheus and Verstraete [MaVe23] (see [erdosproblems.com/166]) implies $f_4(n) \gg \frac{n^{2/3}}{(\log n)^{4/3}}$.

theorem Erdos920.erdos_920.variants.lower_bound (k : ℕ) (hk : k ≥ 3) : ∃ c > 0, (fun (n : ℕ) => ↑n ^ (1 - 2 / (↑k + 1)) / Real.log ↑n ^ c) =O[Filter.atTop] fun (n : ℕ) => ↑(f k n)

A positive answer to this question would follow from [erdosproblems.com/986]. The known bounds for that problem imply $f_k(n) \gg \frac{n^{1-\frac{2}{k+1}}}{(\log n)^{c_k}}.$