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.

This definition is meant to be used for small values of ε, and in particular is junk for values of ε greater than or equal to 1. The junk value is chosen to be positive, so that 0 < ε → 0 < triangleRemovalBound ε regardless of whether ε < 1 or not.

Equations

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

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

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

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

theorem SimpleGraph.triangleRemovalBound_le {ε : ℝ} (hε₁ : ε ≤ 1) : triangleRemovalBound ε ≤ (1 - ε / 4) * (ε / (16 * ↑(SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3

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 - ↑(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 ε) : 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 < 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 : PositivityExt

Extension for the positivity tactic: SimpleGraph.triangleRemovalBound ε is positive if ε is.

This exploits the positivity of the junk value of triangleRemovalBound ε for ε ≥ 1.

Equations

• One or more equations did not get rendered due to their size.