The Erdős-Stone-Simonovits theorem

This file proves the Erdős-Stone-Simonovits theorem for simple graphs.

Main definitions

• SimpleGraph.eventually_completeEquipartiteGraph_isContained_of_minDegree is the proof of the minimal degree version of the Erdős-Stone theorem for simple graphs.

theorem SimpleGraph.eventually_completeEquipartiteGraph_isContained_of_minDegree {ε : ℝ} (hε : 0 < ε) (r t : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj], ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → (completeEquipartiteGraph (r + 1) t).IsContained G

If G has a minimal degree of at least (1 - 1 / r + o(1)) * n, then G contains a copy of a completeEquipartiteGraph in r + 1 parts each of size t.

This is the minimal-degree version of the Erdős-Stone theorem.