Triangle counting lemma #
In this file, we prove the triangle counting lemma.
References #
[Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]
theorem
SimpleGraph.triangle_counting'
{α : Type u_1}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{ε : ℝ}
{s t u : Finset α}
(dst : 2 * ε ≤ ↑(G.edgeDensity s t))
(hst : G.IsUniform ε s t)
(dsu : 2 * ε ≤ ↑(G.edgeDensity s u))
(usu : G.IsUniform ε s u)
(dtu : 2 * ε ≤ ↑(G.edgeDensity t u))
(utu : G.IsUniform ε t u)
:
The Triangle Counting Lemma. If G is a graph and s, t, u are sets of vertices such
that each pair is ε-uniform and 2 * ε-dense, then a proportion of at least
(1 - 2 * ε) * ε ^ 3 of the triples (a, b, c) ∈ s × t × u are triangles.
theorem
SimpleGraph.triangle_counting
{α : Type u_1}
(G : SimpleGraph α)
[DecidableRel G.Adj]
{ε : ℝ}
{s t u : Finset α}
[DecidableEq α]
[Fintype α]
(dst : 2 * ε ≤ ↑(G.edgeDensity s t))
(ust : G.IsUniform ε s t)
(hst : Disjoint s t)
(dsu : 2 * ε ≤ ↑(G.edgeDensity s u))
(usu : G.IsUniform ε s u)
(hsu : Disjoint s u)
(dtu : 2 * ε ≤ ↑(G.edgeDensity t u))
(utu : G.IsUniform ε t u)
(htu : Disjoint t u)
:
The Triangle Counting Lemma. If G is a graph and s, t, u are disjoint sets of
vertices such that each pair is ε-uniform and 2 * ε-dense, then G contains at least
(1 - 2 * ε) * ε ^ 3 * |s| * |t| * |u| triangles.