English
If a graph G has fewer than triangleRemovalBound(ε)·|V|^3 triangles, then there exists a subgraph G' ≤ G obtained by removing at most ε|V|^2 edges such that G' is triangle-free.
Русский
Если в графе G не слишком много треугольников, то существует подграф G' ≤ G, полученный удалением не более ε|V|^2 ребер, который не содержит треугольников.
LaTeX
$$There exists G' ≤ G with (#G.edgeFinset − #G'.edgeFinset) < ε·(|V|^2) and G' is triangle-free, i.e. G'.CliqueFree 3.$$
Lean4
/-- **Triangle Removal Lemma**. If there are not too many triangles (on the order of `(card α)^3`)
then they can all be removed by removing a few edges (on the order of `(card α)^2`). -/
theorem triangle_removal (hG : #(G.cliqueFinset 3) < triangleRemovalBound ε * card α ^ 3) :
∃ G' ≤ G,
∃ _ : DecidableRel G'.Adj, (#G.edgeFinset - #G'.edgeFinset : ℝ) < ε * (card α ^ 2 : ℕ) ∧ G'.CliqueFree 3 :=
by
by_contra! h
refine hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset
intro G' _ hG hG'
exact le_of_not_gt fun i ↦ h G' hG _ i hG'
