zarankiewicz_ks_t_problem
Provedalgebracombinatoricsextremal-combinatoricsgraph-theoryready-to-formalize
Zarankiewicz problem for K_{s,t}-free graphs: Maximum edges in an n-vertex graph with no complete bipartite subgraph K_{s,t}. Kővári–Sós–Turán gives O(n^{2-1/s}). The exact exponent and constant (achieved by algebraic constructions) are open for most s, t.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem zarankiewicz_ks_t_problem (s t : ℕ) (hs : 2 ≤ s) (ht : 2 ≤ t) :
∀ eps : ℝ, 0 < eps →
∃ C : ℝ, 0 < C ∧
∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
(¬∃ (A B : Finset (Fin n)), A.card = s ∧ B.card = t ∧
∀ a ∈ A, ∀ b ∈ B, G.Adj a b) →
G.edgeFinset.card ≤ C * n ^ (2 - 1/s + eps) := by
sorrySource