English
The exact number of edges of the Turán graph T(n,r) is given by a closed formula in terms of n and r, namely |E(T(n,r))| = (n^2 − (n mod r)^2)·(r−1)/(2r) + (n mod r choose 2).
Русский
Точное число ребер графа Турана T(n,r) задаётся формулой: |E(T(n,r))| = (n^2 − (n mod r)^2)·(r−1)/(2r) + (n mod r choose 2).
LaTeX
$$$|E(\\mathrm{turanGraph}(n,r))| = \\frac{n^{2} - (n \\bmod r)^{2}}{2r}(r-1) + {n \\bmod r \\choose 2}$$$
Lean4
/-- 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]
