Erdős Problem 579

References:

• erdosproblems.com/579
• [EHSS83] P. Erdős, A. Hajnal, V. T. Sós and E. Szemerédi, More results on Ramsey–Turán type problems, Combinatorica 3 (1983), 69–81.

@[reducible, inline]

abbrev Erdos579.octahedron : SimpleGraph ((_ : Fin 3) × Fin 2)

The octahedron $K_{2,2,2}$: the complete tripartite graph with all three parts of size $2$.

Equations

• Erdos579.octahedron = SimpleGraph.completeMultipartiteGraph fun (x : Fin 3) => Fin 2

theorem Erdos579.erdos_579 : sorry ↔ ∀ (δ : ℝ), 0 < δ → ∃ (c : ℝ), 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), octahedron.Free G → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → c * ↑n ≤ ↑G.indepNum

Let $\delta > 0$. If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no $K_{2,2,2}$ (the octahedron) and at least $\delta n^2$ edges, must $G$ contain an independent set of size $\gg_\delta n$?

This is a problem of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]. It is open; they proved the statement for $\delta > 1/8$ (see erdos_579.variants.ehss_large_delta), and the difficulty is to push the edge-density threshold down to an arbitrary $\delta > 0$.

Here $K_{2,2,2}$ is the complete tripartite graph with all parts of size $2$, encoded as completeMultipartiteGraph (fun _ : Fin 3 => Fin 2); "contains no $K_{2,2,2}$" is expressed via SimpleGraph.Free.

theorem Erdos579.erdos_579.variants.ehss_large_delta (δ : ℝ) (hδ : 1 / 8 < δ) : ∃ (c : ℝ), 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), octahedron.Free G → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → c * ↑n ≤ ↑G.indepNum

The partial result of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]: the statement of erdos_579 holds whenever the edge-density coefficient exceeds $1/8$. That is, for every $\delta > 1/8$ there is a $c > 0$ such that for all sufficiently large $n$, every $K_{2,2,2}$-free graph $G$ on $n$ vertices with at least $\delta n^2$ edges has an independent set of size at least $c n$.

theorem Erdos579.erdos_579.variants.octahedron_not_free : ¬octahedron.Free octahedron

Sanity check that the forbidden structure is non-trivial: the octahedron is of course not octahedron-free, since it contains a copy of itself.