feat: number of edges in the Turán graph (leanprover-community#25788)

We provide two theorems, the first `card_edgeFinset_turanGraph` providing the exact number of edges and the other `mul_card_edgeFinset_turanGraph_le` providing a (slightly) looser bound whose main advantage is its lack of division/modulus operations.

The bound in `mul_card_edgeFinset_turanGraph_le` is also the bound provided in [Motzkin and Straus (1965)](https://doi.org/10.4153%2FCJM-1965-053-6).

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Author: Parcly-Taxel

Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Tan
 -/
 import Mathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 import Mathlib.Order.Partition.Equipartition
 
 /-!
@@ -255,8 +256,7 @@ theorem card_parts [DecidableEq V] : #h.finpartition.parts = min (Fintype.card V
   have cf : G.CliqueFree r := by
     simp_rw [← cliqueFinset_eq_empty_iff, cliqueFinset, filter_eq_empty_iff, mem_univ,
       forall_true_left, isNClique_iff, and_comm, not_and, isClique_iff, Set.Pairwise]
-    #adaptation_note /-- 2025-07-19 added `-congrConsts` -/
-    intro z zc; push_neg; simp_rw -congrConsts [h.not_adj_iff_part_eq]
+    intro z zc; push_neg; simp_rw [h.not_adj_iff_part_eq]
     exact exists_ne_map_eq_of_card_lt_of_maps_to (zc.symm ▸ l.2) fun a _ ↦
       fp.part_mem.2 (mem_univ a)
   use G ⊔ edge x y, inferInstance, cf.sup_edge x y
@@ -310,4 +310,110 @@ theorem isTuranMaximal_iff_nonempty_iso_turanGraph (hr : 0 < r) :
     G.IsTuranMaximal r ↔ Nonempty (G ≃g turanGraph (Fintype.card V) r) :=
   ⟨fun h ↦ h.nonempty_iso_turanGraph, fun h ↦ isTuranMaximal_of_iso h.some hr⟩
 
+/-! ### Number of edges in the Turán graph -/
+
+private lemma sum_ne_add_mod_eq_sub_one {c : ℕ} :
+    ∑ w ∈ range r, (if c % r ≠ (n + w) % r then 1 else 0) = r - 1 := by
+  rcases r.eq_zero_or_pos with rfl | hr; · simp
+  suffices #{i ∈ range r | c % r = (n + i) % r} = 1 by
+    rw [← card_filter, ← this]; apply Nat.eq_sub_of_add_eq'
+    rw [filter_card_add_filter_neg_card_eq_card, card_range]
+  apply le_antisymm
+  · change #{i ∈ range r | _ ≡ _ [MOD r]} ≤ 1
+    rw [card_le_one_iff]; intro w x mw mx
+    simp only [mem_filter, mem_range] at mw mx
+    have := mw.2.symm.trans mx.2
+    rw [Nat.ModEq.add_iff_left rfl] at this
+    change w % r = x % r at this
+    rwa [Nat.mod_eq_of_lt mw.1, Nat.mod_eq_of_lt mx.1] at this
+  · rw [one_le_card]; use ((r - 1) * n + c) % r
+    simp only [mem_filter, mem_range]; refine ⟨Nat.mod_lt _ hr, ?_⟩
+    rw [Nat.add_mod_mod, ← add_assoc, ← one_add_mul, show 1 + (r - 1) = r by omega,
+      Nat.mul_add_mod_self_left]
+
+lemma card_edgeFinset_turanGraph_add :
+    #(turanGraph (n + r) r).edgeFinset =
+    #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2 := by
+  rw [← mul_right_inj' two_ne_zero]
+  simp_rw [mul_add, ← sum_degrees_eq_twice_card_edges,
+    degree, neighborFinset_eq_filter, turanGraph, card_filter]
+  conv_lhs =>
+    enter [2, v]
+    rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]
+  rw [sum_add_distrib,
+    Fin.sum_univ_eq_sum_range fun v ↦ ∑ w ∈ range n, if v % r ≠ w % r then 1 else 0,
+    Fin.sum_univ_eq_sum_range fun v ↦ ∑ w ∈ range r, if v % r ≠ (n + w) % r then 1 else 0,
+    sum_range_add, sum_range_add, add_assoc, add_assoc]
+  congr 1; · simp [← Fin.sum_univ_eq_sum_range]
+  rw [← add_assoc, sum_comm]; simp_rw [ne_comm, ← two_mul]; congr
+  · conv_rhs => rw [← card_range n, ← smul_eq_mul, ← sum_const]
+    congr!; exact sum_ne_add_mod_eq_sub_one
+  · rw [mul_comm 2, Nat.choose_two_right, Nat.div_two_mul_two_of_even (Nat.even_mul_pred_self r)]
+    conv_rhs => enter [1]; rw [← card_range r]
+    rw [← smul_eq_mul, ← sum_const]
+    congr!; exact sum_ne_add_mod_eq_sub_one
+
+/-- The exact formula for the number of edges in `turanGraph n r`. -/
+theorem card_edgeFinset_turanGraph {n r : ℕ} :
+    #(turanGraph n r).edgeFinset =
+    (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2 := by
+  rcases r.eq_zero_or_pos with rfl | hr
+  · rw [Nat.mod_zero, tsub_self, zero_mul, Nat.zero_div, zero_add]
+    have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
+    rw [Fintype.card_fin] at this; convert this; exact turanGraph_zero
+  · have ring₁ (n) : (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) =
+        n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2 := by
+      nth_rw 1 [← Nat.mod_add_div n r, Nat.sq_sub_sq, add_tsub_cancel_left,
+        show (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
+          (2 * ((n % r) * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r by grind]
+      rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]
+    rcases lt_or_ge n r with h | h
+    · rw [Nat.mod_eq_of_lt h, tsub_self, zero_mul, Nat.zero_div, zero_add]
+      have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
+      rw [Fintype.card_fin] at this; convert this
+      rw [turanGraph_eq_top]; exact .inr h.le
+    · let n' := n - r
+      have n'r : n = n' + r := by omega
+      rw [n'r, card_edgeFinset_turanGraph_add, card_edgeFinset_turanGraph, ring₁, ring₁,
+        add_rotate, ← add_assoc, Nat.add_mod_right, Nat.add_div_right _ hr]
+      congr 1
+      have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd
+      rw [← Nat.div_mul_right_comm rd, ← Nat.div_mul_right_comm rd, ← Nat.choose_two_right]
+      have ring₂ : n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
+          n' % r * (n' / r + 1) * (r - 1) + r.choose 2 +
+          r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2 := by grind
+      rw [ring₂, ← add_assoc]; congr 1
+      rw [← add_rotate, ← add_rotate _ _ (r.choose 2)]; congr 1
+      rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
+        ← add_rotate, add_comm _ (_ *_)]; congr 1
+      rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]
+
+/-- A looser (but simpler than `card_edgeFinset_turanGraph`) bound on the number of edges in
+`turanGraph n r`. -/
+theorem mul_card_edgeFinset_turanGraph_le :
+    2 * r * #(turanGraph n r).edgeFinset ≤ (r - 1) * n ^ 2 := by
+  rw [card_edgeFinset_turanGraph, mul_add]
+  apply (Nat.add_le_add_right (Nat.mul_div_le ..) _).trans
+  rw [tsub_mul, ← Nat.sub_add_comm]; swap
+  · exact mul_le_mul_right' (pow_le_pow_left' (Nat.mod_le ..) _) _
+  rw [Nat.sub_le_iff_le_add, mul_comm, Nat.add_le_add_iff_left, Nat.choose_two_right,
+    ← Nat.mul_div_assoc _ (Nat.even_mul_pred_self _).two_dvd, mul_assoc,
+    mul_div_cancel_left₀ _ two_ne_zero, ← mul_assoc, ← mul_rotate, sq, ← mul_rotate (r - 1)]
+  refine mul_le_mul_right' ?_ _
+  rcases r.eq_zero_or_pos with rfl | hr; · omega
+  rw [Nat.sub_one_mul, Nat.sub_one_mul, mul_comm]
+  exact Nat.sub_le_sub_left (Nat.mod_lt _ hr).le _
+
+theorem CliqueFree.card_edgeFinset_le (cf : G.CliqueFree (r + 1)) :
+    let n := Fintype.card V;
+    #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2 := by
+  rcases r.eq_zero_or_pos with rfl | hr
+  · rw [cliqueFree_one, ← Fintype.card_eq_zero_iff] at cf
+    simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]
+    exact card_edgeFinset_le_card_choose_two
+  · obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr
+    convert maxH.2 _ cf
+    rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
+      card_edgeFinset_turanGraph]
+
 end SimpleGraph

Mathlib/Data/Nat/ModEq.lean

@@ -141,6 +141,10 @@ protected theorem add_left_cancel (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b +
 protected theorem add_left_cancel' (c : ℕ) (h : c + a ≡ c + b [MOD n]) : a ≡ b [MOD n] :=
   ModEq.rfl.add_left_cancel h
 
+@[simp]
+protected theorem add_iff_left (h : a ≡ b [MOD n]) : a + c ≡ b + d [MOD n] ↔ c ≡ d [MOD n] :=
+  ⟨h.add_left_cancel, h.add⟩
+
 protected theorem add_right_cancel (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
     a ≡ b [MOD n] := by
   rw [add_comm a, add_comm b] at h₂
@@ -149,6 +153,10 @@ protected theorem add_right_cancel (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b
 protected theorem add_right_cancel' (c : ℕ) (h : a + c ≡ b + c [MOD n]) : a ≡ b [MOD n] :=
   ModEq.rfl.add_right_cancel h
 
+@[simp]
+protected theorem add_iff_right (h : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n] ↔ a ≡ b [MOD n] :=
+  ⟨h.add_right_cancel, (.add · h)⟩
+
 protected lemma sub' (h : c ≤ a ↔ d ≤ b) (hab : a ≡ b [MOD n]) (hcd : c ≡ d [MOD n]) :
     a - c ≡ b - d [MOD n] := by
   obtain hac | hca := lt_or_ge a c