English
A variant of a triangle counting statement in logical form.
Русский
Вариант леммы подсчёта треугольников в виде логических эквивалентностей.
LaTeX
$$Eq (Exists x => p x) b$$
Lean4
/-- 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 triangle_counting' (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 * #t * #u ≤ #((s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) := by
classical
have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
have : X'.biUnion _ ⊆ (s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
triangle_split_helper _
refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
rw [card_biUnion, Nat.cast_sum]
· apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
rw [nsmul_eq_mul]
have := hst.pos.le
suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s := union_subset (filter_subset _ _) (filter_subset _ _)
rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i), sub_le_sub_iff_left, mul_assoc,
mul_comm ε, two_mul]
refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
rw [Nat.cast_add]
gcongr
rintro a _ b _ t
rw [Function.onFun, disjoint_left]
simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj, exists_imp, and_imp, not_and]
aesop
