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

The embedding lemma

Let L be a finite graph on k vertices with a proper colouring c by r colours, and let s : Fin r → Finset α be parts of a graph G that are pairwise dense in a robust sense (or pairwise ε-uniform and dense). Then L embeds into G with every vertex x of L mapped into the part s (c x). This is the "key lemma" of the regularity method, proved by greedy embedding.

• Embedding.exists_embedding: embedding lemma, robust-density form.
• Embedding.exists_embedding_of_isUniform: embedding lemma, uniform form.
• Embedding.isContained_of_isUniform: in the uniform setting, L ⊑ G.

theorem Embedding.exists_embedding {α : Type u_1} (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) (s : Fin r → Finset α) {η d : ℝ} (hη : 0 < η) (hη₁ : η ≤ 1) (hd : 0 < d) (hd₁ : d ≤ 1) (hηd : 2 * ↑(Fintype.card β) * η ≤ d ^ Fintype.card β) (hsize : ∀ (i : Fin r), 2 * ↑(Fintype.card β) ≤ d ^ Fintype.card β * ↑(s i).card) (hs : ∀ (i j : Fin r), i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * ↑(s i).card ≤ ↑A.card → η * ↑(s j).card ≤ ↑B.card → d ≤ ↑(G.edgeDensity A B)) : ∃ (f : β → α), Function.Injective f ∧ (∀ (x : β), f x ∈ s (c x)) ∧ ∀ (x y : β), L.Adj x y → G.Adj (f x) (f y)

Embedding lemma, robust-density form. Let L be a graph on a finite type β with k = card β vertices and a proper colouring c : β → Fin r. Suppose that for all colours i ≠ j, all subsets A ⊆ s i, B ⊆ s j with #A ≥ η #(s i) and #B ≥ η #(s j) have edge density at least d, where 0 < η ≤ 1, 0 < d ≤ 1, 2 k η ≤ d ^ k, and every part has at least 2 k / d ^ k vertices. Then there is an injective map f : β → α sending each x into s (c x) and edges of L to edges of G.

theorem Embedding.exists_embedding_of_isUniform {α : Type u_1} (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) (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hd₁ : d ≤ 1) (hεd : 2 * ↑(Fintype.card β) * ε ≤ d ^ Fintype.card β) (hsize : ∀ (i : Fin r), 2 * ↑(Fintype.card β) ≤ d ^ Fintype.card β * ↑(s i).card) (hu : ∀ (i j : Fin r), i ≠ j → G.IsUniform ε (s i) (s j)) (hdens : ∀ (i j : Fin r), i ≠ j → d + ε ≤ ↑(G.edgeDensity (s i) (s j))) : ∃ (f : β → α), Function.Injective f ∧ (∀ (x : β), f x ∈ s (c x)) ∧ ∀ (x y : β), L.Adj x y → G.Adj (f x) (f y)

Embedding lemma, uniform form. Under the hypotheses of exists_embedding, with the robust density condition replaced by: every pair of distinct parts is ε-uniform with edge density at least d + ε, and 2 k ε ≤ d ^ k.

theorem Embedding.isContained_of_isUniform {α : Type u_1} (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) (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hd₁ : d ≤ 1) (hεd : 2 * ↑(Fintype.card β) * ε ≤ d ^ Fintype.card β) (hsize : ∀ (i : Fin r), 2 * ↑(Fintype.card β) ≤ d ^ Fintype.card β * ↑(s i).card) (hu : ∀ (i j : Fin r), i ≠ j → G.IsUniform ε (s i) (s j)) (hdens : ∀ (i j : Fin r), i ≠ j → d + ε ≤ ↑(G.edgeDensity (s i) (s j))) : L.IsContained G

Embedding lemma, containment form. Under the hypotheses of exists_embedding_of_isUniform, L is contained in G (L ⊑ G, Mathlib's SimpleGraph.IsContained).