English
If G is K_{r+1}-free on n vertices (i.e., G.CliqueFree(r+1)), then the number of edges of G is bounded above by the Turán bound: |E(G)| ≤ (n^2 − (n mod r)^2)·(r−1)/(2r) + (n mod r choose 2).
Русский
Пусть G не содержит K_{r+1} на n вершинах; тогда число ребер G не превосходитTurán-границы: |E(G)| ≤ (n^2 − (n mod r)^2)·(r−1)/(2r) + (n mod r choose 2).
LaTeX
$$$|E(G)| \\le \\frac{n^{2} - (n \\bmod r)^{2}}{2r}(r-1) + {n \\bmod r \\choose 2}, \\quad n=|V|$$$
Lean4
theorem 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]
