feat(Combinatorics/SimpleGraph): define the Zarankiewicz function (leanprover-community#34633)

Defines the Zarankiewicz function $z(m, n; s, t)$ in terms of bipartite graphs.

Author: mitchell-horner

Mathlib.lean

@@ -3660,6 +3660,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
 public import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
 public import Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
+public import Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
 public import Mathlib.Combinatorics.SimpleGraph.Finite
 public import Mathlib.Combinatorics.SimpleGraph.Finsubgraph
 public import Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Mitchell Horner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mitchell Horner
+-/
+module
+
+public import Mathlib.Algebra.Order.Floor.Semiring
+public import Mathlib.Combinatorics.SimpleGraph.Bipartite
+public import Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Maps
+
+import Mathlib.Algebra.Order.Archimedean.Real.Basic
+import Mathlib.Logic.Equiv.Fin.Basic
+import Mathlib.Tactic.Rify
+
+/-!
+# The Zarankiewicz function
+
+This file defines the **Zarankiewicz function** in terms of bipartite graphs.
+-/
+
+public section
+
+open Finset Fintype
+
+namespace SimpleGraph
+
+/-- The **Zarankiewicz function** of natural numbers `m`, `n`, `s`, and `t` is the maximum
+number of edges in a `completeBipartiteGraph (Fin s) (Fin t)`-free bipartite graph with parts of
+size `m` and `n`.
+
+This is the *extremal graph theory* version of the **Zarankiewicz function**. -/
+noncomputable def zarankiewicz (m n s t : ℕ) : ℕ :=
+  open Classical in
+  sup { G : SimpleGraph (Fin m ⊕ Fin n) | G ≤ completeBipartiteGraph (Fin m) (Fin n)
+    ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G} (#·.edgeFinset)
+
+variable {m n s t : ℕ} {V W α β : Type*} [Fintype V] [Fintype W] [Fintype α] [Fintype β]
+
+open Classical in
+theorem zarankiewicz_of_fintypeCard_eq
+    (hm : card V = m) (hn : card W = n) (hs : card α = s) (ht : card β = t) :
+    zarankiewicz m n s t =
+      sup { G : SimpleGraph (V ⊕ W) | G ≤ completeBipartiteGraph V W
+        ∧ (completeBipartiteGraph α β).Free G} (#·.edgeFinset) := by
+  let e₁ := completeBipartiteGraphCongr
+    (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
+  let K := completeBipartiteGraph (Fin s) (Fin t)
+  let e₂ := completeBipartiteGraphCongr
+    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
+  rw [zarankiewicz, le_antisymm_iff]
+  and_intros
+  on_goal 1 =>
+    let e₁ := e₁.symm
+    let K := completeBipartiteGraph α β
+    let e₂ := e₂.symm
+  all_goals
+    simp_rw [Finset.sup_le_iff, mem_filter, mem_univ, true_and]
+    intro G ⟨h_le, h_free⟩
+    simp_rw [Iso.card_edgeFinset_eq (.map e₁.toEquiv G)]
+    have h' : G.map e₁.toEquiv.toEmbedding ∈ univ.filter fun G ↦
+        G ≤ completeBipartiteGraph _ _ ∧ K.Free G := by
+      rw [mem_filter_univ, map_le_iff_le_comap]
+      refine ⟨fun _ _ hadj ↦ ?_, ?_⟩
+      · replace h_le := h_le hadj
+        rw [← Embedding.map_adj_iff e₁.toEmbedding, ← comap_adj] at h_le
+        exact h_le
+      · rw [Function.Embedding.coeFn_mk, ← free_congr e₂ (.map e₁.toEquiv G)]
+        exact h_free
+    have h_le_sup := @le_sup _ _ _ _ _ (#·.edgeFinset) (G.map e₁.toEquiv.toEmbedding) h'
+    simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢
+    exact h_le_sup
+
+/-- `zarankiewicz m n s t` is at most `x` if and only if every
+`completeBipartiteGraph α β`-free bipartite graph `G` has at most `x` edges. -/
+theorem zarankiewicz_le_iff
+    (hm : card V = m) (hn : card W = n) (hs : card α = s) (ht : card β = t) (x : ℕ) :
+    zarankiewicz m n s t ≤ x ↔
+      ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [DecidableRel G.Adj], G ≤ completeBipartiteGraph V W →
+        (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x := by
+  simp_rw [zarankiewicz_of_fintypeCard_eq hm hn hs ht,
+    Finset.sup_le_iff, mem_filter, mem_univ, true_and]
+  exact ⟨fun h _ _ h_le h_free ↦ (h _ ⟨h_le, h_free⟩).trans_eq' <| by convert rfl,
+    fun h _ ⟨h_le, h_free⟩ ↦ by convert h h_le h_free⟩
+
+/-- `zarankiewicz m n s t` is greater than `x` if and only if there
+exists a `completeBipartiteGraph α β`-free bipartite graph `G` with more than `x` edges. -/
+theorem lt_zarankiewicz_iff
+    (hm : card V = m) (hn : card W = n) (hs : card α = s) (ht : card β = t) (x : ℕ) :
+    x < zarankiewicz m n s t ↔
+      ∃ G : SimpleGraph (V ⊕ W), ∃ _ : DecidableRel G.Adj, G ≤ completeBipartiteGraph V W ∧
+        (completeBipartiteGraph α β).Free G ∧  x < #G.edgeFinset := by
+  simp_rw [zarankiewicz_of_fintypeCard_eq hm hn hs ht,
+    Finset.lt_sup_iff, mem_filter, mem_univ, true_and]
+  exact ⟨fun ⟨_, ⟨h_le, h_free⟩, h_lt⟩ ↦ ⟨_, _, h_le, h_free, by convert h_lt⟩,
+    fun ⟨_, _, ⟨h_le, h_free, h_lt⟩⟩ ↦ ⟨_, ⟨h_le, h_free⟩, h_lt.trans_eq <| by convert rfl⟩⟩
+
+variable {R : Type*} [Semiring R] [LinearOrder R] [FloorSemiring R]
+
+@[inherit_doc zarankiewicz_le_iff]
+theorem zarankiewicz_le_iff_of_nonneg
+    (hm : card V = m) (hn : card W = n) (hs : card α = s) (ht : card β = t) {x : R} (h : 0 ≤ x) :
+    zarankiewicz m n s t ≤ x ↔
+      ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [DecidableRel G.Adj], G ≤ completeBipartiteGraph V W →
+        (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x := by
+  simp_rw [← Nat.le_floor_iff h]
+  exact zarankiewicz_le_iff hm hn hs ht ⌊x⌋₊
+
+@[inherit_doc lt_zarankiewicz_iff]
+theorem lt_zarankiewicz_iff_of_nonneg
+    (hm : card V = m) (hn : card W = n) (hs : card α = s) (ht : card β = t) {x : R} (h : 0 ≤ x) :
+    x < zarankiewicz m n s t ↔
+      ∃ G : SimpleGraph (V ⊕ W), ∃ _ : DecidableRel G.Adj, G ≤ completeBipartiteGraph V W ∧
+        (completeBipartiteGraph α β).Free G ∧  x < #G.edgeFinset := by
+  simp_rw [← Nat.floor_lt h]
+  exact lt_zarankiewicz_iff hm hn hs ht ⌊x⌋₊
+
+open Classical in
+/-- The Zarankiewicz function is at most the corresponding extremal number. -/
+theorem zarankiewicz_le_extremalNumber (hs : card α = s) (ht : card β = t) :
+    zarankiewicz m n s t ≤ extremalNumber (m + n) (completeBipartiteGraph α β) := by
+  conv =>
+    enter [2, 1]
+    rw [← Fintype.card_fin (m + n)]
+  simp_rw [zarankiewicz, Finset.sup_le_iff, mem_filter, mem_univ, true_and]
+  intro B ⟨_, h⟩
+  rw [(Iso.map finSumFinEquiv B).card_edgeFinset_eq]
+  refine card_edgeFinset_le_extremalNumber <|
+    (h.congr_left ?_).congr_right (Iso.map finSumFinEquiv B).symm
+  exact completeBipartiteGraphCongr
+    (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
+
+/-- The symmetric Zarankiewicz function is at least twice a corresponding extremal number. -/
+theorem two_mul_extremalNumber_le_zarankiewicz_symm
+    [Nonempty α] [Nonempty β] (hs : card α = s) (ht : card β = t) :
+    2 * extremalNumber n (completeBipartiteGraph α β) ≤ zarankiewicz n n s t := by
+  conv =>
+    enter [1, 2, 1]
+    rw [← Fintype.card_fin n]
+  rify
+  rw [← le_div_iff₀' (by positivity), extremalNumber_le_iff_of_nonneg _ (by positivity)]
+  intro G _ h
+  rw [le_div_iff₀' (by positivity), ← Nat.cast_two, ← Nat.cast_mul, Nat.cast_le]
+  apply Finset.le_sup_of_le (b := G.bipartiteDoubleCover)
+  · simp_rw [mem_filter, mem_univ, true_and]
+    refine ⟨bipartiteDoubleCover_le, ?_⟩
+    contrapose! h
+    refine completeBipartiteGraph_isContained_bipartiteDoubleCover.mp <|
+      h.trans' ⟨Iso.toCopy ?_⟩
+    exact completeBipartiteGraphCongr
+      (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
+  · convert card_edgeFinset_bipartiteDoubleCover.symm.le
+
+end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -799,6 +799,14 @@ def induceUnivIso (G : SimpleGraph V) : G.induce Set.univ ≃g G where
   map_rel_iff' := by simp only [Equiv.Set.univ, Equiv.coe_fn_mk, comap_adj, Embedding.coe_subtype,
                                 implies_true]
 
+/-- The isomorphism between `completeBipartiteGraph V₁ W₁` and
+`completeBipartiteGraph V₂ W₂` where `V₁ ≃ V₂` and `W₁ ≃ W₂`. -/
+@[simps!]
+def completeBipartiteGraphCongr {V₁ V₂ W₁ W₂ : Type*} (hV : V₁ ≃ V₂) (hW : W₁ ≃ W₂) :
+    completeBipartiteGraph V₁ W₁ ≃g completeBipartiteGraph V₂ W₂ where
+  __ := hV.sumCongr hW
+  map_rel_iff' := by simp
+
 section Finite
 
 variable [Fintype V] {n : ℕ}