Adapted from jtraverso/graph-removal-lemma (Palomar-registered source).

The graph removal lemma for every fixed graph

Let H be a fixed finite graph on k vertices.

• GraphRemoval.card_copies_ge: counting lemma for H. If parts s x (one per vertex x of H, possibly repeated) are pairwise dense in a robust sense along the edges of H, and large enough, then the number of injective maps f with f x ∈ s x sending edges of H to edges of G is at least (d^k / 4)^k ∏ₓ #(s x).
• GraphRemoval.le_labelledCopyCount_of_deleteFar: graph removal lemma, far form. For every ε > 0 there is δ > 0 such that a graph on n vertices from which one must delete at least ε n² edges to destroy all copies of H (Mathlib's SimpleGraph.DeleteFar and SimpleGraph.Free) has at least δ n^k labelled copies of H (Mathlib's SimpleGraph.labelledCopyCount).
• GraphRemoval.graph_removal: graph removal lemma. A graph on n vertices with fewer than δ n^k labelled copies of H can be made H-free by deleting fewer than ε n² edges.

The quantitative copy-count formulation is stated in Conlon–Fox, Graph removal lemmas, Theorem 1.1. For fixed H, changing from unlabelled copies to injective labelled copies changes only a factor depending on H, which is absorbed into δ. The far form is the contrapositive. Erdős–Frankl–Rödl (1986), Theorems 1.5 and 1.5′, give related precursors: starting from an H-free graph, they remove few edges to exclude a clique or a homomorphic image.

theorem GraphRemoval.card_copies_ge {α : Type u_1} {β : Type u_2} [Fintype β] (L : SimpleGraph β) (G : SimpleGraph α) [DecidableRel G.Adj] (s : β → Finset α) {η d : ℝ} (hη : 0 < η) (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) (hηd : 2 * ↑(Fintype.card β) * η ≤ d ^ Fintype.card β) (hsize : ∀ (x : β), 4 * ↑(Fintype.card β) ≤ d ^ Fintype.card β * ↑(s x).card) (hs : ∀ (x y : β), L.Adj x y → ∀ A ⊆ s x, ∀ B ⊆ s y, η * ↑(s x).card ≤ ↑A.card → η * ↑(s y).card ≤ ↑B.card → d ≤ ↑(G.edgeDensity A B)) : (d ^ Fintype.card β / 4) ^ Fintype.card β * ∏ x : β, ↑(s x).card ≤ ↑(Nat.card { f : β ↪ α // (∀ (x : β), f x ∈ s x) ∧ ∀ (x y : β), L.Adj x y → G.Adj (f x) (f y) })

Counting lemma for a fixed graph. Let L be a graph on a finite type β with k = card β vertices, and s : β → Finset α parts of a graph G such that for every edge xy of L, all subsets A ⊆ s x, B ⊆ s y with #A ≥ η #(s x), #B ≥ η #(s y) have edge density at least d, where 0 < η ≤ 1, 0 < d ≤ 1, 2 k η ≤ d ^ k and every part has at least 4 k / d ^ k elements. Then there are at least (d ^ k / 4) ^ k ∏ₓ #(s x) injective maps f : β → α with f x ∈ s x for every x that send edges of L to edges of G.

theorem GraphRemoval.le_labelledCopyCount_of_deleteFar {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (α : Type) [inst : Fintype α] [DecidableEq α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj], G.DeleteFar (fun (G' : SimpleGraph α) => H.Free G') (ε * ↑(Fintype.card α ^ 2)) → δ * ↑(Fintype.card α) ^ Fintype.card β ≤ ↑(G.labelledCopyCount H)

Graph removal lemma, far form. The contrapositive of Conlon–Fox, Graph removal lemmas, Theorem 1.1. For every finite graph H and every ε > 0 there is δ > 0 such that every finite graph on n vertices that is ε n²-far from being H-free has at least δ n ^ (card β) labelled copies of H.

theorem GraphRemoval.graph_removal {β : Type} [Fintype β] (H : SimpleGraph β) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (α : Type) [inst : Fintype α] [DecidableEq α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj], ↑(G.labelledCopyCount H) < δ * ↑(Fintype.card α) ^ Fintype.card β → ∃ G' ≤ G, ∃ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ H.Free G'

Graph removal lemma. See Conlon–Fox, Graph removal lemmas, Theorem 1.1. For every finite graph H and every ε > 0 there is δ > 0 such that every finite graph on n vertices with fewer than δ n ^ (card β) labelled copies of H has an H-free subgraph obtained by deleting fewer than ε n² edges.