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

The clique removal lemma

This file generalises Mathlib's triangle removal lemma (SimpleGraph.triangle_removal, SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset) from triangles to cliques of any size r, using Szemerédi's regularity lemma (SzemerediRegularity, szemeredi_regularity), Mathlib's reduced graph SimpleGraph.regularityReduced and the clique counting lemma CliqueCounting.card_cliqueFinset_ge.

• CliqueRemoval.le_card_cliqueFinset_of_deleteFar: clique removal lemma, far form. For every r and ε > 0 there is δ > 0 such that every finite graph from which one must delete at least ε n² edges to destroy all r-cliques has at least δ n^r cliques of size r.
• CliqueRemoval.clique_removal: clique removal lemma. For every r and ε > 0 there is δ > 0 such that every finite graph on n vertices with fewer than δ n^r cliques of size r can be made K_r-free by deleting fewer than ε n² edges.

theorem CliqueRemoval.aux_lt_two_mul {n k : ℕ} (hk : 0 < k) (hn : k ≤ n) : n < 2 * k * (n / k)

Arithmetic helper: n < 2 k (n / k) when 0 < k ≤ n.

theorem CliqueRemoval.card_bound {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} {B : ℕ} {s : Finset α} (hP₁ : P.IsEquipartition) (hP₃ : P.parts.card ≤ B) (hX : s ∈ P.parts) : ↑(Fintype.card α) / (2 * ↑B) ≤ ↑s.card

Parts of an equipartition with at most B parts have size at least card α / (2 B).

theorem CliqueRemoval.unreduced_edges_subset' {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] {P : Finpartition Finset.univ} {η δ : ℝ} : {x ∈ Finset.univ ×ˢ Finset.univ | match x with | (x, y) => G.Adj x y ∧ ¬(SimpleGraph.regularityReduced P G η δ).Adj x y} ⊆ ((P.nonUniforms G η).biUnion fun (x : Finset α × Finset α) => match x with | (U, V) => U ×ˢ V) ∪ P.parts.biUnion Finset.offDiag ∪ (P.sparsePairs G δ).biUnion fun (x : Finset α × Finset α) => match x with | (U, V) => G.interedges U V

Generalisation of SimpleGraph.unreduced_edges_subset to arbitrary parameters.

theorem CliqueRemoval.regularityReduced_edges_card_aux' {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] {P : Finpartition Finset.univ} [Nonempty α] {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (hηε : η ≤ ε / 8) (hP : P.IsEquipartition) (hPε : P.IsUniform G η) (hP' : 4 / ε ≤ ↑P.parts.card) : ↑G.edgeFinset.card - ↑(SimpleGraph.regularityReduced P G η (ε / 4)).edgeFinset.card < ε * ↑(Fintype.card α ^ 2)

Generalisation of SimpleGraph.regularityReduced_edges_card_aux to a uniformity parameter η ≤ ε / 8.

theorem CliqueRemoval.card_cliqueFinset_ge_of_mem_reduced {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] {P : Finpartition Finset.univ} {r B : ℕ} {ε η d : ℝ} (hη : 0 < η) (hd : 0 < d) (hηd : 2 * ↑r * η ≤ d ^ (r - 1)) (hdη : d + η ≤ ε / 4) (hP₁ : P.IsEquipartition) (hP₃ : P.parts.card ≤ B) {t : Finset α} (ht : (SimpleGraph.regularityReduced P G η (ε / 4)).IsNClique r t) : d ^ r.choose 2 / 2 ^ r * (↑(Fintype.card α) / (2 * ↑B)) ^ r ≤ ↑(G.cliqueFinset r).card

An r-clique of the reduced graph yields many r-cliques of G.

theorem CliqueRemoval.le_card_cliqueFinset_of_deleteFar (r : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj], G.DeleteFar (fun (H : SimpleGraph α) => H.CliqueFree r) (ε * ↑(Fintype.card α ^ 2)) → δ * ↑(Fintype.card α) ^ r ≤ ↑(G.cliqueFinset r).card

Clique removal lemma, far form. For every r and ε > 0 there is δ > 0 such that a finite graph on n vertices that is ε n²-far from being K_r-free (in the sense of Mathlib's SimpleGraph.DeleteFar) has at least δ n^r cliques of size r.

theorem CliqueRemoval.clique_removal (r : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj], ↑(G.cliqueFinset r).card < δ * ↑(Fintype.card α) ^ r → ∃ G' ≤ G, ∃ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree r

Clique removal lemma. For every r and ε > 0 there is δ > 0 such that every finite graph on n vertices with fewer than δ n^r cliques of size r has a K_r-free subgraph obtained by deleting fewer than ε n² edges.