Stability with few forbidden copies

This combines the graph removal lemma with Erdős–Simonovits stability. The graph is allowed to contain a small positive density of labelled copies of the forbidden graph.

theorem RemovalExtremalStability.stability_of_few_copies {β : Type} [Fintype β] (H : SimpleGraph β) {p : ℕ} (hp : 0 < p) (hH : H.Colorable (p + 1)) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ) (η : ℝ), 0 < δ ∧ 0 < η ∧ ∃ (n₀ : ℕ), ∀ (W : Type) [inst : Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj], n₀ ≤ Fintype.card W → ↑(G.labelledCopyCount H) < η * ↑(Fintype.card W) ^ Fintype.card β → (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

If H is (p + 1)-colourable, a graph with nearly the Turán number of edges and sufficiently few labelled copies of H is close to a complete p-partite graph.