English
For Turán graphs T(n+r,r), the number of edges satisfies the recurrence |E(T(n+r,r))| = |E(T(n,r))| + n(r−1) + C(r,2).
Русский
Для графов Турана T(n+r, r) число ребер удовлетворяет равенству |E(T(n+r,r))| = |E(T(n,r))| + n(r−1) + C(r,2).
LaTeX
$$$|E(\\mathrm{turanGraph}(n+r,r))| = |E(\\mathrm{turanGraph}(n,r))| + n\\,(r-1) + {r \\choose 2}.$$$
Lean4
theorem 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
