Adapted from jtraverso/turan-stability (Palomar-registered source).

The Erdős–Simonovits stability theorem

Erdős–Simonovits stability theorem (Erdős 1967, Simonovits 1968), in the form derived by Füredi (2015) from the regularity method: let L be a finite graph with chromatic number at most p + 1 (i.e. L.Colorable (p + 1)). For every ε > 0 there are δ > 0 and n₀ such that every L-free graph on n ≥ n₀ vertices with at least (1 - 1/p) n² / 2 - δ n² edges differs from some complete p-partite graph on the same vertices in at most ε n² edges.

The proof combines Szemerédi's regularity lemma (through the reduced graph of StabilityLib/CliqueRemoval.lean), the embedding lemma Embedding.exists_embedding_of_isUniform (the reduced graph of an L-free graph is K_{p+1}-free) and Füredi's theorem Furedi.exists_partition_symmDiff_le applied to the reduced graph.

ErdosSimonovits.stability: the theorem above. The complete p-partite graph with parts the fibres of f : W → Fin p is (⊤ : SimpleGraph (Fin p)).comap f; L ⊑ G is Mathlib's SimpleGraph.IsContained.

theorem ErdosSimonovits.regularityReduced_cliqueFree {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {β : Type u_2} [Fintype β] (L : SimpleGraph β) {r : ℕ} (c : β → Fin r) (hc : ∀ (x y : β), L.Adj x y → c x ≠ c y) {P : Finpartition Finset.univ} {B : ℕ} {η d ε : ℝ} (hη : 0 < η) (hd : 0 < d) (hd₁ : d ≤ 1) (hηd : 2 * ↑(Fintype.card β) * η ≤ d ^ Fintype.card β) (hdη : d + η ≤ ε / 4) (hP₁ : P.IsEquipartition) (hP₃ : P.parts.card ≤ B) (hsize : 2 * ↑(Fintype.card β) ≤ d ^ Fintype.card β * (↑(Fintype.card α) / (2 * ↑B))) (hL : ¬L.IsContained G) : (SimpleGraph.regularityReduced P G η (ε / 4)).CliqueFree r

The reduced graph of an L-free graph is K_r-free, provided L is properly r-coloured and the parameters allow the embedding lemma.

theorem ErdosSimonovits.ncard_symmDiff_le {W : Type u_1} [Finite W] {G G' : SimpleGraph W} (h : G' ≤ G) (K : SimpleGraph W) : (symmDiff G K).edgeSet.ncard ≤ (symmDiff G' K).edgeSet.ncard + (G.edgeSet.ncard - G'.edgeSet.ncard)

Edit distance to K grows by at most the number of deleted edges when passing from a subgraph G' to G.

theorem ErdosSimonovits.stability {β : Type} [Finite β] (L : SimpleGraph β) {p : ℕ} (hp : 0 < p) (hL : L.Colorable (p + 1)) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∃ (n₀ : ℕ), ∀ (W : Type) [inst : Fintype W] (G : SimpleGraph W), n₀ ≤ Fintype.card W → ¬L.IsContained G → (1 - 1 / ↑p) * ↑(Fintype.card W) ^ 2 / 2 - δ * ↑(Fintype.card W) ^ 2 ≤ ↑G.edgeSet.ncard → ∃ (f : W → Fin p), ↑(symmDiff G (SimpleGraph.comap f ⊤)).edgeSet.ncard ≤ ε * ↑(Fintype.card W) ^ 2

Erdős–Simonovits stability theorem. Let L be a finite graph that is (p + 1)-colourable. For every ε > 0 there are δ > 0 and n₀ such that every graph G on n ≥ n₀ vertices that does not contain L and has at least (1 - 1/p) n² / 2 - δ n² edges differs from some complete p-partite graph on the same vertices in at most ε n² edges.