feat: forward direction of Turán's theorem (#11990)

Part of #9317.

Mathlib/Combinatorics/SimpleGraph/Turan.lean

@@ -4,29 +4,49 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Tan
 -/
 import Mathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Order.Partition.Equipartition
 
 /-!
-# The Turán graph
+# Turán's theorem
 
-This file defines the Turán graph and proves some of its basic properties.
+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.
 
 ## 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`.
+
+## References
+
+* https://en.wikipedia.org/wiki/Turán%27s_theorem
 
 ## TODO
 
-* Port the rest of Turán's theorem from https://github.com/leanprover-community/mathlib4/pull/9317
+* Prove the reverse direction of Turán's theorem at
+  https://github.com/leanprover-community/mathlib4/pull/9317
 -/
 
 open Finset
 
 namespace SimpleGraph
+
 variable {V : Type*} [Fintype V] [DecidableEq V] (G H : SimpleGraph V) [DecidableRel G.Adj]
   {n r : ℕ}
 
+section Defs
+
 /-- 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. -/
 def IsTuranMaximal (r : ℕ) : Prop :=
@@ -91,4 +111,175 @@ theorem not_cliqueFree_of_isTuranMaximal (hn : r ≤ Fintype.card V) (hG : G.IsT
   exact hGab <| le_sup_right.trans_eq ((hG.le_iff_eq <| h.sup_edge _ _).1 le_sup_left).symm <|
     (edge_adj ..).2 ⟨Or.inl ⟨rfl, rfl⟩, hab⟩
 
+lemma exists_isTuranMaximal :
+    ∃ H : SimpleGraph V, ∃ _ : DecidableRel H.Adj, H.IsTuranMaximal r := by
+  classical
+  let c := {H : SimpleGraph V | H.CliqueFree (r + 1)}
+  have cn : c.toFinset.Nonempty := ⟨⊥, by
+    simp only [Set.toFinset_setOf, mem_filter, mem_univ, true_and, c]
+    exact cliqueFree_bot (by omega)⟩
+  obtain ⟨S, Sm, Sl⟩ := exists_max_image c.toFinset (·.edgeFinset.card) cn
+  use S, inferInstance
+  rw [Set.mem_toFinset] at Sm
+  refine ⟨Sm, ?_⟩
+  intro I _ cf
+  by_cases Im : I ∈ c.toFinset
+  · convert Sl I Im
+  · rw [Set.mem_toFinset] at Im
+    contradiction
+
+end Defs
+
+section Forward
+
+variable {G} {s t u : V} (h : G.IsTuranMaximal r)
+
+namespace IsTuranMaximal
+
+/-- In a Turán-maximal graph, non-adjacent vertices have the same degree. -/
+lemma degree_eq_of_not_adj (hn : ¬G.Adj s t) : G.degree s = G.degree t := by
+  rw [IsTuranMaximal] at h; contrapose! h; intro cf
+  wlog hd : G.degree t < G.degree s generalizing G t s
+  · replace hd : G.degree s < G.degree t := lt_of_le_of_ne (le_of_not_lt hd) h
+    exact this (by rwa [adj_comm] at hn) hd.ne' cf hd
+  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
+  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
+  omega
+
+/-- In a Turán-maximal graph, non-adjacency is transitive. -/
+lemma not_adj_trans (hst : ¬G.Adj s t) (hsu : ¬G.Adj s u) : ¬G.Adj t u := by
+  have dst := h.degree_eq_of_not_adj hst
+  have dsu := h.degree_eq_of_not_adj hsu
+  rw [IsTuranMaximal] at h; contrapose! h; intro cf
+  use (G.replaceVertex s t).replaceVertex s u, inferInstance,
+    (cf.replaceVertex s t).replaceVertex s u
+  have nst : s ≠ t := fun a ↦ hsu (a ▸ h)
+  have ntu : t ≠ u := G.ne_of_adj h
+  have := (G.adj_replaceVertex_iff_of_ne s nst ntu.symm).not.mpr hsu
+  rw [card_edgeFinset_replaceVertex_of_not_adj _ this,
+    card_edgeFinset_replaceVertex_of_not_adj _ hst, dst, Nat.add_sub_cancel]
+  have l1 : (G.replaceVertex s t).degree s = G.degree s := by
+    unfold degree; congr 1; ext v
+    simp only [mem_neighborFinset, SimpleGraph.irrefl, ite_self]
+    by_cases eq : v = t
+    · simpa only [eq, not_adj_replaceVertex_same, false_iff]
+    · rw [G.adj_replaceVertex_iff_of_ne s nst eq]
+  have l2 : (G.replaceVertex s t).degree u = G.degree u - 1 := by
+    rw [degree, degree, ← card_singleton t, ← card_sdiff (by simp [h.symm])]
+    congr 1; ext v
+    simp only [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]
+    split_ifs <;> simp_all [adj_comm]
+  have l3 : 0 < G.degree u := by rw [G.degree_pos_iff_exists_adj u]; use t, h.symm
+  omega
+
+/-- In a Turán-maximal graph, non-adjacency is an equivalence relation. -/
+theorem equivalence_not_adj : Equivalence fun x y ↦ ¬G.Adj x y where
+  refl x := by simp
+  symm xy := by simp [xy, adj_comm]
+  trans xy yz := by
+    rw [adj_comm] at xy
+    exact h.not_adj_trans xy yz
+
+/-- The non-adjacency setoid over the vertices of a Turán-maximal graph
+induced by `equivalence_not_adj`. -/
+def setoid : Setoid V := ⟨_, h.equivalence_not_adj⟩
+
+instance : DecidableRel h.setoid.r :=
+  inferInstanceAs <| DecidableRel fun v w ↦ ¬G.Adj v w
+
+/-- The finpartition derived from `h.setoid`. -/
+def finpartition : Finpartition (univ : Finset V) := Finpartition.ofSetoid h.setoid
+
+lemma not_adj_iff_part_eq : ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t := by
+  change h.setoid.r s t ↔ _
+  rw [← Finpartition.mem_part_ofSetoid_iff_rel]
+  let fp := h.finpartition
+  change t ∈ fp.part s ↔ fp.part s = fp.part t
+  rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]
+
+lemma degree_eq_card_sub_part_card : G.degree s = Fintype.card V - (h.finpartition.part s).card :=
+  calc
+    _ = (univ.filter fun b ↦ G.Adj s b).card := by
+      simp [← card_neighborFinset_eq_degree, neighborFinset]
+    _ = Fintype.card V - (univ.filter fun b ↦ ¬G.Adj s b).card :=
+      eq_tsub_of_add_eq (filter_card_add_filter_neg_card_eq_card _)
+    _ = _ := by
+      congr; ext; rw [mem_filter]
+      convert Finpartition.mem_part_ofSetoid_iff_rel.symm
+      simp [setoid]
+
+/-- The parts of a Turán-maximal graph form an equipartition. -/
+theorem isEquipartition : h.finpartition.IsEquipartition := by
+  set fp := h.finpartition
+  by_contra hn
+  rw [Finpartition.not_isEquipartition] at hn
+  obtain ⟨large, hl, small, hs, ineq⟩ := hn
+  obtain ⟨w, hw⟩ := fp.nonempty_of_mem_parts hl
+  obtain ⟨v, hv⟩ := fp.nonempty_of_mem_parts hs
+  apply absurd h
+  rw [IsTuranMaximal]; push_neg; intro cf
+  use G.replaceVertex v w, inferInstance, cf.replaceVertex v w
+  have large_eq := fp.part_eq_of_mem hl hw
+  have small_eq := fp.part_eq_of_mem hs hv
+  have ha : G.Adj v w := by
+    by_contra hn; rw [h.not_adj_iff_part_eq, small_eq, large_eq] at hn
+    rw [hn] at ineq; omega
+  rw [G.card_edgeFinset_replaceVertex_of_adj ha,
+    degree_eq_card_sub_part_card h, small_eq, degree_eq_card_sub_part_card h, large_eq]
+  have : large.card ≤ Fintype.card V := by simpa using card_le_card large.subset_univ
+  omega
+
+lemma card_parts_le : h.finpartition.parts.card ≤ r := by
+  by_contra! l
+  obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn
+  have ncf : ¬G.CliqueFree z.card := by
+    refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩
+    contrapose! hn
+    exact hz.injOn hv hw (by rwa [← h.not_adj_iff_part_eq])
+  rw [Finset.card_eq_of_equiv hz.equiv] at ncf
+  exact absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf
+
+/-- 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 card_parts : h.finpartition.parts.card = min (Fintype.card V) r := by
+  set fp := h.finpartition
+  apply le_antisymm (le_min fp.card_parts_le_card h.card_parts_le)
+  by_contra! l
+  rw [lt_min_iff] at l
+  obtain ⟨x, -, y, -, hn, he⟩ :=
+    exists_ne_map_eq_of_card_lt_of_maps_to l.1 fun a _ ↦ fp.part_mem (mem_univ a)
+  apply absurd h
+  rw [IsTuranMaximal]; push_neg; rintro -
+  have cf : G.CliqueFree r := by
+    simp_rw [← cliqueFinset_eq_empty_iff, cliqueFinset, filter_eq_empty_iff, mem_univ,
+      forall_true_left, isNClique_iff, and_comm, not_and, isClique_iff, Set.Pairwise]
+    intro z zc; push_neg; simp_rw [h.not_adj_iff_part_eq]
+    exact exists_ne_map_eq_of_card_lt_of_maps_to (zc.symm ▸ l.2) fun a _ ↦ fp.part_mem (mem_univ a)
+  use G ⊔ edge x y, inferInstance, cf.sup_edge x y
+  convert Nat.lt.base G.edgeFinset.card
+  convert G.card_edgeFinset_sup_edge _ hn
+  rwa [h.not_adj_iff_part_eq]
+
+/-- **Turán's theorem**, forward direction.
+
+Any `r + 1`-cliquefree Turán-maximal graph on `n` vertices is isomorphic to `turanGraph n r`. -/
+theorem nonempty_iso_turanGraph : Nonempty (G ≃g turanGraph (Fintype.card V) r) := by
+  obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
+  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
+  intro a b
+  simp_rw [turanGraph, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
+  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
+  rw [← h.not_adj_iff_part_eq] at this
+  rw [← not_iff_not, not_ne_iff, this, card_parts]
+  rcases le_or_lt r (Fintype.card V) with c | c
+  · rw [min_eq_right c]; rfl
+  · have lc : ∀ x, zm ⟨x, _⟩ < Fintype.card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
+    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
+      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl
+
+end IsTuranMaximal
+
+end Forward
+
 end SimpleGraph

Mathlib/Order/Partition/Finpartition.lean

@@ -498,9 +498,16 @@ theorem existsUnique_mem (ha : a ∈ s) : ∃! t, t ∈ P.parts ∧ a ∈ t := b
 /-- The part of the finpartition that `a` lies in. -/
 def part (a : α) : Finset α := if ha : a ∈ s then choose (hp := P.existsUnique_mem ha) else ∅
 
-theorem part_mem (ha : a ∈ s) : P.part a ∈ P.parts := by simp [part, ha, choose_mem]
+lemma part_mem (ha : a ∈ s) : P.part a ∈ P.parts := by simp [part, ha, choose_mem]
 
-theorem mem_part (ha : a ∈ s) : a ∈ P.part a := by simp [part, ha, choose_property]
+lemma mem_part (ha : a ∈ s) : a ∈ P.part a := by simp [part, ha, choose_property]
+
+lemma part_eq_of_mem (ht : t ∈ P.parts) (hat : a ∈ t) : P.part a = t := by
+  apply P.eq_of_mem_parts (P.part_mem _) ht (P.mem_part _) hat <;> exact mem_of_subset (P.le ht) hat
+
+lemma mem_part_iff_part_eq_part {b : α} (ha : a ∈ s) (hb : b ∈ s) :
+    a ∈ P.part b ↔ P.part a = P.part b :=
+  ⟨fun c ↦ (P.part_eq_of_mem (P.part_mem hb) c), fun c ↦ c ▸ P.mem_part ha⟩
 
 theorem part_surjOn : Set.SurjOn P.part s P.parts := fun p hp ↦ by
   obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp
@@ -521,8 +528,7 @@ def equivSigmaParts : s ≃ Σ t : P.parts, t.1 where
     ext e
     · obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
       dsimp only at mf ⊢
-      have mfs := mem_of_subset (P.le mp) mf
-      rw [P.eq_of_mem_parts mp (P.part_mem mfs) mf (P.mem_part mfs)]
+      rw [P.part_eq_of_mem mp mf]
     · simp
 
 lemma exists_enumeration : ∃ f : s ≃ Σ t : P.parts, Fin t.1.card,