theorem SimpleGraph.CliqueFree.two_mul_r_mul_card_edgeFinset_le {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (cf : G.CliqueFree (r + 1)) : 2 * r * G.edgeFinset.card ≤ (r - 1) * Fintype.card V ^ 2

Integer form of Turán's theorem (Theorem 2.3.6, Turán 1941): any $K_{r+1}$-free graph $G$ on $|V|$ vertices satisfies $2 r \cdot |E(G)| \leq (r - 1) \cdot |V|^2$.

theorem SimpleGraph.CliqueFree.card_edgeFinset_le_real {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (cf : G.CliqueFree (r + 1)) (hr : 0 < r) : ↑G.edgeFinset.card ≤ (1 - 1 / ↑r) * ↑(Fintype.card V) ^ 2 / 2

Real form of Turán's theorem (Theorem 2.3.6): any $K_{r+1}$-free graph on $|V|$ vertices has at most $\left(1 - \tfrac{1}{r}\right) \tfrac{|V|^2}{2}$ edges.