The Zarankiewicz function

This file defines the Zarankiewicz function in terms of bipartite graphs.

noncomputable def SimpleGraph.zarankiewicz (m n s t : ℕ) : ℕ

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.

Equations

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

theorem SimpleGraph.zarankiewicz_of_fintypeCard_eq {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype V] [Fintype W] [Fintype α] [Fintype β] (hm : Fintype.card V = m) (hn : Fintype.card W = n) (hs : Fintype.card α = s) (ht : Fintype.card β = t) : zarankiewicz m n s t = {G : SimpleGraph (V ⊕ W) | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun (x : SimpleGraph (V ⊕ W)) => x.edgeFinset.card

theorem SimpleGraph.zarankiewicz_le_iff {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype V] [Fintype W] [Fintype α] [Fintype β] (hm : Fintype.card V = m) (hn : Fintype.card W = n) (hs : Fintype.card α = s) (ht : Fintype.card β = t) (x : ℕ) : zarankiewicz m n s t ≤ x ↔ ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj], G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → G.edgeFinset.card ≤ x

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 SimpleGraph.lt_zarankiewicz_iff {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype V] [Fintype W] [Fintype α] [Fintype β] (hm : Fintype.card V = m) (hn : Fintype.card W = n) (hs : Fintype.card α = s) (ht : Fintype.card β = t) (x : ℕ) : x < zarankiewicz m n s t ↔ ∃ (G : SimpleGraph (V ⊕ W)) (x_1 : DecidableRel G.Adj), G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < G.edgeFinset.card

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 SimpleGraph.zarankiewicz_le_iff_of_nonneg {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype V] [Fintype W] [Fintype α] [Fintype β] {R : Type u_5} [Semiring R] [LinearOrder R] [FloorSemiring R] (hm : Fintype.card V = m) (hn : Fintype.card W = n) (hs : Fintype.card α = s) (ht : Fintype.card β = t) {x : R} (h : 0 ≤ x) : ↑(zarankiewicz m n s t) ≤ x ↔ ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj], G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → ↑G.edgeFinset.card ≤ x

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 SimpleGraph.lt_zarankiewicz_iff_of_nonneg {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype V] [Fintype W] [Fintype α] [Fintype β] {R : Type u_5} [Semiring R] [LinearOrder R] [FloorSemiring R] (hm : Fintype.card V = m) (hn : Fintype.card W = n) (hs : Fintype.card α = s) (ht : Fintype.card β = t) {x : R} (h : 0 ≤ x) : x < ↑(zarankiewicz m n s t) ↔ ∃ (G : SimpleGraph (V ⊕ W)) (x_1 : DecidableRel G.Adj), G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < ↑G.edgeFinset.card

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 SimpleGraph.zarankiewicz_le_extremalNumber {m n s t : ℕ} {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (hs : Fintype.card α = s) (ht : Fintype.card β = t) : zarankiewicz m n s t ≤ extremalNumber (m + n) (completeBipartiteGraph α β)

The Zarankiewicz function is at most the corresponding extremal number.

theorem SimpleGraph.two_mul_extremalNumber_le_zarankiewicz_symm {n s t : ℕ} {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (hs : Fintype.card α = s) (ht : Fintype.card β = t) : 2 * extremalNumber n (completeBipartiteGraph α β) ≤ zarankiewicz n n s t

The symmetric Zarankiewicz function is at least twice a corresponding extremal number.