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

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) : (1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑{x ∈ s ×ˢ t ×ˢ u | match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}.card

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) : (1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(G.cliqueFinset 3).card

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.