The Turán graph

This file defines the Turán graph and proves some of its basic properties.

Main declarations

• SimpleGraph.IsTuranMaximal: G.IsTuranMaximal r means that G has the most number of edges for its number of vertices while still being r + 1-cliquefree.
• SimpleGraph.turanGraph n r: The canonical r + 1-cliquefree Turán graph on n vertices.

TODO

• Port the rest of Turán's theorem from https://github.com/leanprover-community/mathlib4/pull/9317

def SimpleGraph.IsTuranMaximal {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℕ) : Prop

An r + 1-cliquefree graph is r-Turán-maximal if any other r + 1-cliquefree graph on the same vertex set has the same or fewer number of edges.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.IsTuranMaximal.le_iff_eq {V : Type u_1} [Fintype V] {G : SimpleGraph V} {H : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hG : SimpleGraph.IsTuranMaximal G r) (hH : SimpleGraph.CliqueFree H (r + 1)) : G ≤ H ↔ G = H

def SimpleGraph.turanGraph (n : ℕ) (r : ℕ) : SimpleGraph (Fin n)

The canonical r + 1-cliquefree Turán graph on n vertices.

Equations

• SimpleGraph.turanGraph n r = { Adj := fun (v w : Fin n) => ↑v % r ≠ ↑w % r, symm := ⋯, loopless := ⋯ }

instance SimpleGraph.turanGraph.instDecidableRelAdj {n : ℕ} {r : ℕ} : DecidableRel (SimpleGraph.turanGraph n r).Adj

Equations

• SimpleGraph.turanGraph.instDecidableRelAdj = id inferInstance

@[simp]

theorem SimpleGraph.turanGraph_zero {n : ℕ} : SimpleGraph.turanGraph n 0 = ⊤

@[simp]

theorem SimpleGraph.turanGraph_eq_top {n : ℕ} {r : ℕ} : SimpleGraph.turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

theorem SimpleGraph.turanGraph_cliqueFree {n : ℕ} {r : ℕ} (hr : 0 < r) : SimpleGraph.CliqueFree (SimpleGraph.turanGraph n r) (r + 1)

theorem SimpleGraph.isTuranMaximal_turanGraph {n : ℕ} {r : ℕ} (hr : 0 < r) (h : n ≤ r) : SimpleGraph.IsTuranMaximal (SimpleGraph.turanGraph n r) r

For n ≤ r and 0 < r, turanGraph n r is Turán-maximal.

theorem SimpleGraph.not_cliqueFree_of_isTuranMaximal {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) (hn : r ≤ Fintype.card V) (hG : SimpleGraph.IsTuranMaximal G r) : ¬SimpleGraph.CliqueFree G r

An r + 1-cliquefree Turán-maximal graph is not r-cliquefree if it can accommodate such a clique.