Triangle removal lemma

In this file, we prove the triangle removal lemma.

References

[Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]

noncomputable def SimpleGraph.triangleRemovalBound (ε : ℝ) : ℝ

An explicit form for the constant in the triangle removal lemma.

Note that this depends on SzemerediRegularity.bound, which is a tower-type exponential. This means triangleRemovalBound is in practice absolutely tiny.

Equations

• SimpleGraph.triangleRemovalBound ε = min (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ ((1 - ε / 4) * (ε / (16 * ↑(SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3)

theorem SimpleGraph.triangleRemovalBound_pos {ε : ℝ} (hε : 0 < ε) (hε₁ : ε ≤ 1) : 0 < SimpleGraph.triangleRemovalBound ε

theorem SimpleGraph.triangleRemovalBound_nonpos {ε : ℝ} (hε : ε ≤ 0) : SimpleGraph.triangleRemovalBound ε ≤ 0

theorem SimpleGraph.triangleRemovalBound_mul_cube_lt {ε : ℝ} (hε : 0 < ε) : SimpleGraph.triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1

theorem SimpleGraph.regularityReduced_edges_card_aux {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] {P : Finpartition Finset.univ} {ε : ℝ} [Nonempty α] (hε : 0 < ε) (hP : P.IsEquipartition) (hPε : P.IsUniform G (ε / 8)) (hP' : 4 / ε ≤ ↑P.parts.card) : 2 * (↑G.edgeFinset.card - ↑(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).edgeFinset.card) < 2 * ε * ↑(Fintype.card α ^ 2)

theorem SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : ℝ} (hG : G.FarFromTriangleFree ε) : SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card

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 SimpleGraph.triangle_removal {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : ℝ} (hG : ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3) : ∃ G' ≤ G, ∃ (x : DecidableRel G'.Adj), ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3

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).

def Mathlib.Meta.Positivity.evalTriangleRemovalBound : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: SimpleGraph.triangleRemovalBound ε is positive if 0 < ε ≤ 1.

Note this looks for ε ≤ 1 in the context.