Erdős Problem 615

A Ramsey–Turán problem of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS93]: does there exist a constant $c > 0$ such that every graph on $n$ vertices with at least $(1/8 - c)n^2$ edges contains either a $K_4$ or an independent set on at least $n/\log n$ vertices? In the notation of Ramsey–Turán theory this asks whether $$\mathrm{rt}(n; 4, n/\log n) < (1/8 - c)n^2.$$

This was disproved by Fox, Loh, and Zhao [FLZ15], who showed that $\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2$ whenever $f(n) = o(\sqrt{\log n/\log\log n})$. In the other direction Sudakov [Su03] had shown that $\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)$ whenever $f(n)/\sqrt{\log n} \to \infty$.

References:

• erdosproblems.com/615
• [EHSSS93] Erdős, P., Hajnal, A., Simonovits, M., Sós, V. T., and Szemerédi, E., Turán-Ramsey theorems and simple asymptotically extremal structures. Combinatorica 13 (1993), 31--56.
• [Su03] Sudakov, B., A few remarks on Ramsey-Turán-type problems. J. Combin. Theory Ser. B 88 (2003), 99--106.
• [FLZ15] Fox, J., Loh, P.-S., and Zhao, Y., The critical window for the classical Ramsey-Turán problem. Combinatorica 35 (2015), 435--476.

theorem Erdos615.erdos_615 : False ↔ ∃ (c : ℝ), 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum

Does there exist some constant $c > 0$ such that for all sufficiently large $n$, if $G$ is a graph with $n$ vertices and at least $(1/8 - c)n^2$ edges then $G$ must contain either a $K_4$ or an independent set on at least $n/\log n$ vertices?

The answer is no, as shown by Fox, Loh, and Zhao [FLZ15].

theorem Erdos615.erdos_615.variants.fox_loh_zhao (f : ℕ → ℝ) (hf : ∀ (n : ℕ), 0 ≤ f n) (hfo : Filter.Tendsto (fun (n : ℕ) => f n / √(Real.log ↑n / Real.log (Real.log ↑n))) Filter.atTop (nhds 0)) (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (G : SimpleGraph (Fin n)), G.CliqueFree 4 ∧ ↑G.indepNum ≤ ↑n * Real.exp (-f n) ∧ (1 / 8 - ε) * ↑n ^ 2 ≤ ↑G.edgeFinset.card

The result of Fox, Loh, and Zhao [FLZ15] disproving the problem: if $f(n) \geq 0$ satisfies $f(n) = o(\sqrt{\log n/\log\log n})$, then for every $\epsilon > 0$ and all sufficiently large $n$ there is a $K_4$-free graph on $n$ vertices with independence number at most $ne^{-f(n)}$ and at least $(1/8 - \epsilon)n^2$ edges; that is, $\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2$. Applied with $f(n) = \log\log n$, this disproves the headline problem, since $ne^{-f(n)} = n/\log n = o(n)$.

theorem Erdos615.erdos_615.variants.sudakov (f : ℕ → ℝ) (hf : Filter.Tendsto (fun (n : ℕ) => f n / √(Real.log ↑n)) Filter.atTop Filter.atTop) (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 4 → ↑G.indepNum ≤ ↑n * Real.exp (-f n) → ↑G.edgeFinset.card ≤ ε * ↑n ^ 2

The complementary result of Sudakov [Su03]: if $f(n)/\sqrt{\log n} \to \infty$ then $\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)$; that is, for every $\epsilon > 0$ and all sufficiently large $n$, every $K_4$-free graph on $n$ vertices with independence number at most $ne^{-f(n)}$ has at most $\epsilon n^2$ edges.

theorem Erdos615.erdos_615.variants.test_bot (n : ℕ) (hn : 3 ≤ n) : ↑n / Real.log ↑n ≤ ↑⊥.indepNum

A sanity check for erdos_615: the empty graph on $n \geq 3$ vertices contains an independent set on at least $n/\log n$ vertices (namely the whole vertex set), so it satisfies the conclusion of the implication in the problem statement.