Turán's theorem

In this file we prove Turán's theorem, the first important result of extremal graph theory, which states that the r + 1-cliquefree graph on n vertices with the most edges is the complete r-partite graph with part sizes as equal as possible (turanGraph n r).

The forward direction of the proof performs "Zykov symmetrisation", which first shows constructively that non-adjacency is an equivalence relation in a maximal graph, so it must be complete multipartite with the parts being the equivalence classes. Then basic manipulations show that the graph is isomorphic to the Turán graph for the given parameters.

For the reverse direction we first show that a Turán-maximal graph exists, then transfer the property through turanGraph n r using the isomorphism provided by the forward direction.

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.
• SimpleGraph.IsTuranMaximal.finpartition: The result of Zykov symmetrisation, a finpartition of the vertices such that two vertices are in the same part iff they are non-adjacent.
• SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph: The forward direction, an isomorphism between G satisfying G.IsTuranMaximal r and turanGraph n r.
• isTuranMaximal_of_iso: the reverse direction, G.IsTuranMaximal r given the isomorphism.
• isTuranMaximal_iff_nonempty_iso_turanGraph: Turán's theorem in full.

References

• https://en.wikipedia.org/wiki/Turán%27s_theorem

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

• G.IsTuranMaximal r = (G.CliqueFree (r + 1) ∧ ∀ (H : SimpleGraph V) [inst_1 : DecidableRel H.Adj], H.CliqueFree (r + 1) → H.edgeFinset.card ≤ G.edgeFinset.card)

theorem SimpleGraph.IsTuranMaximal.le_iff_eq {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} {H : SimpleGraph V} (hG : G.IsTuranMaximal r) (hH : H.CliqueFree (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.turanGraph n r).CliqueFree (r + 1)

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

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

theorem SimpleGraph.exists_isTuranMaximal {V : Type u_1} [Fintype V] {r : ℕ} (hr : 0 < r) : ∃ (H : SimpleGraph V) (x : DecidableRel H.Adj), H.IsTuranMaximal r

theorem SimpleGraph.IsTuranMaximal.degree_eq_of_not_adj {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} {s : V} {t : V} (h : G.IsTuranMaximal r) (hn : ¬G.Adj s t) : G.degree s = G.degree t

In a Turán-maximal graph, non-adjacent vertices have the same degree.

theorem SimpleGraph.IsTuranMaximal.not_adj_trans {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} {s : V} {t : V} {u : V} (h : G.IsTuranMaximal r) (hts : ¬G.Adj t s) (hsu : ¬G.Adj s u) : ¬G.Adj t u

In a Turán-maximal graph, non-adjacency is transitive.

theorem SimpleGraph.IsTuranMaximal.equivalence_not_adj {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) : Equivalence fun (x1 x2 : V) => ¬G.Adj x1 x2

In a Turán-maximal graph, non-adjacency is an equivalence relation.

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

The non-adjacency setoid over the vertices of a Turán-maximal graph induced by equivalence_not_adj.

Equations

• h.setoid = { r := fun (x1 x2 : V) => ¬G.Adj x1 x2, iseqv := ⋯ }

instance SimpleGraph.IsTuranMaximal.instDecidableRelR {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) : DecidableRel ⇑h.setoid

Equations

• h.instDecidableRelR = inferInstanceAs (DecidableRel fun (x1 x2 : V) => ¬G.Adj x1 x2)

def SimpleGraph.IsTuranMaximal.finpartition {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) [DecidableEq V] : Finpartition Finset.univ

The finpartition derived from h.setoid.

Equations

• h.finpartition = Finpartition.ofSetoid h.setoid

theorem SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} {s : V} {t : V} (h : G.IsTuranMaximal r) [DecidableEq V] : ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t

theorem SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} {s : V} (h : G.IsTuranMaximal r) [DecidableEq V] : G.degree s = Fintype.card V - (h.finpartition.part s).card

theorem SimpleGraph.IsTuranMaximal.isEquipartition {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) [DecidableEq V] : h.finpartition.IsEquipartition

The parts of a Turán-maximal graph form an equipartition.

theorem SimpleGraph.IsTuranMaximal.card_parts_le {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) [DecidableEq V] : h.finpartition.parts.card ≤ r

theorem SimpleGraph.IsTuranMaximal.card_parts {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) [DecidableEq V] : h.finpartition.parts.card = min (Fintype.card V) r

There are min n r parts in a graph on n vertices satisfying G.IsTuranMaximal r. min handles the n < r case, when G is complete but still r + 1-cliquefree for having insufficiently many vertices.

theorem SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r) : Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)

Turán's theorem, forward direction.

Any r + 1-cliquefree Turán-maximal graph on n vertices is isomorphic to turanGraph n r.

theorem SimpleGraph.isTuranMaximal_of_iso {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {n : ℕ} {r : ℕ} (f : G ≃g SimpleGraph.turanGraph n r) (hr : 0 < r) : G.IsTuranMaximal r

Turán's theorem, reverse direction.

Any graph isomorphic to turanGraph n r is itself Turán-maximal if 0 < r.

theorem SimpleGraph.IsTuranMaximal.iso {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} {W : Type u_2} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (h : G.IsTuranMaximal r) (f : G ≃g H) (hr : 0 < r) : H.IsTuranMaximal r

Turán-maximality with 0 < r transfers across graph isomorphisms.

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

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

theorem SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) : G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)

Turán's theorem. turanGraph n r is, up to isomorphism, the unique r + 1-cliquefree Turán-maximal graph on n vertices.