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