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

Füredi's stability theorem for Turán's theorem

For a finite simple graph G and a map f : V → Fin p, the graph (⊤ : SimpleGraph (Fin p)).comap f is the complete p-partite graph whose parts are the fibres of f; G \ (⊤.comap f) consists of the edges of G inside the parts.

• Furedi.card_edgeSet_add_le: Füredi (2015), partition inequality. If G is K_{p+1}-free, there is a partition f with e(G) + Σᵢ e(G[Vᵢ]) ≤ e(K(V₁, …, V_p)).
• Furedi.furedi: Füredi (2015). A K_{p+1}-free graph with at least turanNumber n p - t edges has a p-partite subgraph with at least e(G) - t edges.
• Furedi.exists_partition_symmDiff_le: such a graph is at edit distance at most 3 t from a complete p-partite graph, with at most t edges inside the parts.
• Furedi.erdos_simonovits_stability: Erdős–Simonovits stability for cliques. For every ε > 0 there is δ > 0 such that every K_{p+1}-free graph with at least (1 - 1/p) n² / 2 - δ n² edges can be turned into a complete p-partite graph by changing at most ε n² edges.

def Furedi.lhsCount {W : Type u_2} (G : SimpleGraph W) [DecidableRel G.Adj] (S : Finset W) (f : W → ℕ) : ℕ

Ordered count of G-edges plus G-edges inside fibres of f, within S.

Equations

• Furedi.lhsCount G S f = ∑ u ∈ S, ∑ v ∈ S, ((if G.Adj u v then 1 else 0) + if G.Adj u v ∧ f u = f v then 1 else 0)

def Furedi.rhsCount {W : Type u_2} (S : Finset W) (f : W → ℕ) : ℕ

Ordered count of pairs in S with different f-values.

Equations

• Furedi.rhsCount S f = ∑ u ∈ S, ∑ v ∈ S, if f u ≠ f v then 1 else 0

theorem Furedi.key_ineq {W : Type u_2} (G : SimpleGraph W) [DecidableRel G.Adj] (p : ℕ) (S : Finset W) : (∀ t ⊆ S, ¬G.IsNClique (p + 1) t) → ∃ (f : W → ℕ), (∀ w ∈ S, f w < p) ∧ lhsCount G S f ≤ rhsCount S f

theorem Furedi.two_mul_ncard_edgeSet {W : Type u_2} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] : 2 * H.edgeSet.ncard = ∑ u : W, ∑ v : W, if H.Adj u v then 1 else 0

theorem Furedi.card_edgeSet_add_le {W : Type u_2} [Finite W] (G : SimpleGraph W) {p : ℕ} (hp : 0 < p) (hG : G.CliqueFree (p + 1)) : ∃ (f : W → Fin p), G.edgeSet.ncard + (G \ SimpleGraph.comap f ⊤).edgeSet.ncard ≤ (SimpleGraph.comap f ⊤).edgeSet.ncard

Füredi's partition inequality. Every K_{p+1}-free finite graph has a partition into p parts (the fibres of f) such that the number of edges of G plus the number of edges of G inside the parts is at most the number of edges of the complete p-partite graph on these parts.

theorem Furedi.ncard_comap_le_turanNumber {V : Type u_1} [Fintype V] {p : ℕ} (f : V → Fin p) : (SimpleGraph.comap f ⊤).edgeSet.ncard ≤ SimpleGraph.turanNumber (Fintype.card V) p

theorem Furedi.furedi {V : Type u_1} [Fintype V] (G : SimpleGraph V) {p t : ℕ} (hp : 0 < p) (hG : G.CliqueFree (p + 1)) (ht : SimpleGraph.turanNumber (Fintype.card V) p ≤ G.edgeSet.ncard + t) : ∃ H ≤ G, H.Colorable p ∧ G.edgeSet.ncard ≤ H.edgeSet.ncard + t

Füredi's theorem (2015). If G is a K_{p+1}-free graph on n vertices with at least turanNumber n p - t edges, then G has a p-colourable (i.e. p-partite) subgraph H with at least e(G) - t edges.

theorem Furedi.exists_partition_symmDiff_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) {p t : ℕ} (hp : 0 < p) (hG : G.CliqueFree (p + 1)) (ht : SimpleGraph.turanNumber (Fintype.card V) p ≤ G.edgeSet.ncard + t) : ∃ (f : V → Fin p), (G \ SimpleGraph.comap f ⊤).edgeSet.ncard ≤ t ∧ (symmDiff G (SimpleGraph.comap f ⊤)).edgeSet.ncard ≤ 3 * t

Füredi's theorem, edit-distance form. Under the hypotheses of furedi, there is a partition into p parts with at most t edges of G inside the parts, and G differs from the complete p-partite graph on these parts in at most 3 t edges.

theorem Furedi.erdos_simonovits_stability {p : ℕ} (hp : 0 < p) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (W : Type) [inst : Fintype W] (G : SimpleGraph W), G.CliqueFree (p + 1) → (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 for cliques (Erdős 1967, Simonovits 1968), in the form obtained from Füredi's theorem: for every ε > 0 there is δ > 0 such that every K_{p+1}-free graph on 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.