English
If a graph G on n vertices is far from triangle-free in the sense of parameter ε > 0, then G contains many triangles: the number of triangles is at least triangleRemovalBound(ε)·n^3.
Русский
Если граф G на n вершинах далеко от треугольникового-фейн, то число треугольников в G не меньше triangleRemovalBound(ε)·n^3.
LaTeX
$$$\\#\\mathrm{Tri}(G) \\ge \\triangleRemovalBound(\\varepsilon) \\cdot (|V|)^3,$ where \\# Tri(G) denotes the number of triangles (3-cliques) in G.$$
Lean4
/-- **Triangle Removal Lemma**. If not all triangles can be removed by removing few edges (on the
order of `(card α)^2`), then there were many triangles to start with (on the order of
`(card α)^3`). -/
theorem le_card_cliqueFinset (hG : G.FarFromTriangleFree ε) :
triangleRemovalBound ε * card α ^ 3 ≤ #(G.cliqueFinset 3) :=
by
cases isEmpty_or_nonempty α
· simp [Fintype.card_eq_zero]
obtain hε | hε := le_or_gt ε 0
· apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans <;> positivity
let l : ℕ := ⌈4 / ε⌉₊
have hl : 4 / ε ≤ l := le_ceil (4 / ε)
rcases le_total (card α) l with hl' | hl'
·
calc
_ ≤ triangleRemovalBound ε * ↑l ^ 3 := by gcongr; exact (triangleRemovalBound_pos hε).le
_ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
_ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'
obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G (by positivity : 0 < ε / 8) hl'
have : 4 / ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)
have k := regularityReduced_edges_card_aux hε hP₁ hP₄ this
rw [mul_assoc] at k
replace k := lt_of_mul_lt_mul_left k zero_le_two
obtain ⟨t, ht⟩ := hG.cliqueFinset_nonempty' regularityReduced_le k
exact triangle_removal_aux hε hG.lt_one.le hP₁ hP₃ ht
