mitchell-hornerErdosStoneSimonovitsKovariSosTuran0.1.0

Formalising the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean
#math

Formalising the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean

Lean Action CI

This repository contains a formalisation of the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean. The statements of the results are as follows:

The Erdős-Stone theorem (minimal degree version)

Suppose is a positive real number, and are natural numbers, and is a simple graph. If the number of vertices is sufficiently large and the minimal degree , then contains a copy of the complete equipartite graph .

theorem completeEquipartiteGraph_isContained_of_minDegree
  {ε : ℝ} (hε : 0 < ε) (r t : ℕ) :
  ∃ N, ∀ n ≥ N, ∀ {G : SimpleGraph (Fin n)} [DecidableRel G.Adj],
    G.minDegree ≥ (1 - 1 / r + ε) * n
      → completeEquipartiteGraph (r + 1) t ⊑ G

The Erdős-Stone theorem

Suppose is a positive real number, and are natural numbers, and is a simple graph. If the number of vertices is sufficiently large and the number of edges , then contains a copy of the complete equipartite graph .

theorem completeEquipartiteGraph_isContained_of_card_edgeFinset
  {ε : ℝ} (hε_pos : 0 < ε) (r t : ℕ) :
  ∃ N, ∀ n ≥ N, ∀ {G : SimpleGraph (Fin n)} [DecidableRel G.Adj],
    #G.edgeFinset ≥ (1 - 1 / r + ε) * n ^ 2 / 2
    → completeEquipartiteGraph (r + 1) t ⊑ G

The Erdős-Stone theorem (colorable subgraph version)

Suppose is a positive real number and is a simple graph. If the number of vertices is sufficiently large and the number of edges , then contains a copy of any -colorable simple graph .

theorem isContained_of_card_edgeFinset_of_colorable
  {r : ℕ} (hc : H.Colorable (r + 1)) {ε : ℝ} (hε_pos : 0 < ε) :
  ∃ N, ∀ n ≥ N, ∀ {G : SimpleGraph (Fin n)} [DecidableRel G.Adj],
    #G.edgeFinset ≥ (1 - 1 / r + ε) * n ^ 2 / 2 → H ⊑ G

The Erdős-Stone-Simonovits theorem

Suppose is a simple graph and is a positive real number. If the chromatic number , then the extremal numbers of satisfy

for sufficiently large .

theorem lt_extremalNumber_le_of_chromaticNumber {ε : ℝ} (hε : 0 < ε)
  {r : ℕ} (hr_pos : 0 < r) (hχ : H.chromaticNumber = r + 1) :
  ∃ N, ∀ n > N, (1 - 1 / r - ε) * n ^ 2 / 2 < extremalNumber n H ∧
    extremalNumber n H ≤ (1 - 1 / r + ε) * n ^ 2 / 2

The Erdős-Stone-Simonovits theorem (little-O version)

Suppose is a simple graph. If the chromatic number , then the extremal numbers of satisfy

as .

theorem isLittleO_extremalNumber_of_chromaticNumber
  {r : ℕ} (hr_pos : 0 < r) (hχ : H.chromaticNumber = r + 1) :
  (fun (n : ℕ) ↦ (extremalNumber n H - (1 - 1 / r) * n ^ 2 / 2 : ℝ))
    =o[atTop] (fun (n : ℕ) ↦ (n ^ 2 : ℝ))

The Erdős-Stone-Simonovits theorem (Turán density version)

Suppose is a simple graph. If the chromatic number , then the Turán density

theorem turanDensity_eq_of_chromaticNumber
  {r : ℕ} (hr_pos : 0 < r) (hχ : H.chromaticNumber = r + 1) : turanDensity H = 1 - 1 / r

The Erdős-Stone-Simonovits theorem (equivalence version)

Suppose is a simple graph. If the chromatic number , then the extremal numbers of satisfy

as .

theorem isEquivalent_extremalNumber_of_chromaticNumber
  {r : ℕ} (hr : 1 < r) (hχ : H.chromaticNumber = r + 1) :
  (fun (n : ℕ) ↦ (extremalNumber n H : ℝ))
    ~[atTop] (fun (n : ℕ) ↦ ((1 - 1 / r) * n.choose 2 : ℝ))

The Erdős-Stone(-Simonovits) theorem (chromatic number subgraph version)

Suppose is a positive real number and is a simple graph. If the number of vertices is sufficiently large and the number of edges , then contains a copy of any simple graph such that the chromatic number .

theorem isContained_of_card_edgeFinset_of_chromaticNumber
  {r : ℕ} (hr_pos : 0 < r) (hχ : H.chromaticNumber = r + 1) {ε : ℝ} (hε_pos : 0 < ε) :
  ∃ N, ∀ n ≥ N, ∀ {G : SimpleGraph (Fin n)} [DecidableRel G.Adj],
    #G.edgeFinset ≥ (1 - 1 / r + ε) * n.choose 2 → H ⊑ G

The Kővári-Sós-Turán theorem

Suppose , , and are natural numbers such that . The Zarankiewicz function satisfies

theorem zarankiewicz_le (m n : ℕ) {s t : ℕ} (hs : 1 ≤ s) (ht : s ≤ t) :
  (zarankiewicz m n s t : ℝ)
    ≤ ((t - 1) ^ (s⁻¹ : ℝ) * m * n ^ (1 - (s⁻¹ : ℝ)) + (s - 1) * n : ℝ)

The Kővári-Sós-Turán theorem (extremal number version)

Suppose , and are natural numbers such that . The extremal numbers of complete bipartite graphs satisfy

theorem extremalNumber_completeBipartiteGraph_le
  (n : ℕ) [Nonempty α] (hcard_le : card α ≤ card β) :
  (extremalNumber n (completeBipartiteGraph α β) : ℝ) 
    ≤ (card β - 1) ^ (card α : ℝ)⁻¹ * n ^ (2 - (card α : ℝ)⁻¹) / 2 + (card α - 1) * n / 2

Upstreaming to mathlib

The progress towards upstreaming these results to mathlib is as follows:

  • The Erdős-Stone theorem (minimal degree version)
  • The Erdős-Stone theorem
  • The Erdős-Stone theorem (colorable subgraph version)
  • The Erdős-Stone-Simonovits theorem
  • The Erdős-Stone-Simonovits theorem (little-O version)
  • The Erdős-Stone-Simonovits theorem (Turán density version)
  • The Erdős-Stone-Simonovits theorem (equivalence version)
  • The Erdős-Stone(-Simonovits) theorem (chromatic number subgraph version)
  • The Kővári–Sós–Turán theorem
  • The Kővári–Sós–Turán theorem (extremal number version)

Future work

Future work formalising the forbidden subgraph problem could include: