English
The Triangle Counting Lemma in standard form: under density and uniformity, the same lower bound on triangles holds.
Русский
Лемма подсчета треугольников в стандартной форме: при плотности и равномерности выполняется тот же главный предел на треугольники.
LaTeX
$$Triangle counting lemma in standard form$$
Lean4
/-- 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. -/
theorem triangle_counting (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 * #t * #u ≤ #(G.cliqueFinset 3) :=
by
apply (G.triangle_counting' dst ust dsu usu dtu utu).trans _
rw [Nat.cast_le]
refine card_le_card_of_injOn (fun (x, y, z) ↦ { x, y, z }) ?_ ?_
· rintro ⟨x, y, z⟩
simp +contextual [is3Clique_triple_iff]
rintro ⟨x₁, y₁, z₁⟩ h₁ ⟨x₂, y₂, z₂⟩ h₂ t
simp only [mem_coe, mem_filter, mem_product] at h₁ h₂
apply triple_eq_triple_of_mem hst hsu htu t <;> tauto
