Extremal graph theory

How many edges or copies of a subgraph a graph can have while avoiding a forbidden structure: Turán and Zarankiewicz problems, saturation, and extremal graphs of given girth.

• Balanced subgraphs
• Books in graphs
• Erdős–Faudree triangle conjecture
• Extremal graphs of girth five
• Four-cycle-free graphs
• Generalized Turán numbers
• Graph saturation
• Pentagons in triangle-free graphs
• Turán numbers of bipartite graphs
• Turán numbers of cycles
• Turán problems in the hypercube
• Unique subgraphs

TheoremKővári–Sós–Turán bound#✓fully proved

Let \(m, n, s, t\) be natural numbers with \(s \ge 1\) and \(1 \le t \le n\). Let \(z(m, n; s, t)\) be the Zarankiewicz number, the largest number of edges in a bipartite graph with parts of sizes \(m\) and \(n\) that contains no copy of the complete bipartite graph \(K_{s,t}\). Then

\[z(m, n; s, t) \le (s - 1)^{1/t} (n - t + 1) m^{1 - 1/t} + (t - 1) m.\]

Proof: Double-count common right neighborhoods, apply the power-mean inequality, and take a real \(t\)-th root, following Kővári–Sós–Turán (1954) and Jukna, Theorem 2.10.

public theorem kovari_sos_turan (m n s t : ℕ) (ht : 0 < t) (hs : 1 ≤ s)
    (htn : t ≤ n) :
    (SimpleGraph.zarankiewicz m n s t : ℝ) ≤
      Real.rpow ((s : ℝ) - 1) (1 / (t : ℝ)) * ((n : ℝ) - (t : ℝ) + 1) *
        Real.rpow (m : ℝ) (1 - 1 / (t : ℝ)) + ((t : ℝ) - 1) * (m : ℝ)

Sources

• https://en.wikipedia.org/wiki/Zarankiewicz_problem.

TheoremMonomial graphs of girth eight#●ready to prove

Let \(p\) be an odd prime, \(e\) a natural number, \(q = p^e\), and \(\mathbb{F}\) a field with \(q\) elements, and suppose that either \(p \ge 5\) and \(e = 2^a 3^b\) for some natural numbers \(a, b\), or \(3 \le q \le 10^{10}\). For natural numbers \(m_2, n_2, m_3, n_3\), let \(G\) be the bipartite graph with two copies of \(\mathbb{F}^3\) as its parts, in which \((x_1, x_2, x_3)\) in the first part is adjacent to \((y_1, y_2, y_3)\) in the second part exactly when \(x_2 + y_2 = x_1^{m_2} y_1^{n_2}\) and \(x_3 + y_3 = x_1^{m_3} y_1^{n_3}\), and let \(\Gamma_3\) be the graph defined in the same way by \(x_2 + y_2 = x_1 y_1\) and \(x_3 + y_3 = x_1 y_1^2\). If the girth of \(G\) is at least \(8\), then \(G\) is isomorphic to \(\Gamma_3\) and the girth of \(G\) is exactly \(8\).

MetaMathlibExt.monomialGraph_girth_eight_classification · 20 lines

public theorem_wanted monomialGraph_girth_eight_classification
    (p e q : ℕ) (𝔽 : Type*) [Field 𝔽] [Fintype 𝔽] [CharP 𝔽 p]
    (hp : p.Prime) (hp_odd : Odd p) (hq : q = p ^ e)
    (hcard : Fintype.card 𝔽 = q)
    (hcase : (5 ≤ p ∧ ∃ a b : ℕ, e = 2 ^ a * 3 ^ b) ∨ (3 ≤ q ∧ q ≤ 10 ^ 10)) :
    ∀ m₂ n₂ m₃ n₃ : ℕ,
      let G : SimpleGraph (Sum (𝔽 × 𝔽 × 𝔽) (𝔽 × 𝔽 × 𝔽)) :=
        SimpleGraph.fromRel fun u v ↦
          match u, v with
          | Sum.inl (x₁, x₂, x₃), Sum.inr (y₁, y₂, y₃) =>
              x₂ + y₂ = x₁ ^ m₂ * y₁ ^ n₂ ∧
                x₃ + y₃ = x₁ ^ m₃ * y₁ ^ n₃
          | _, _ => False
      let Γ₃ : SimpleGraph (Sum (𝔽 × 𝔽 × 𝔽) (𝔽 × 𝔽 × 𝔽)) :=
        SimpleGraph.fromRel fun u v ↦
          match u, v with
          | Sum.inl (x₁, x₂, x₃), Sum.inr (y₁, y₂, y₃) =>
              x₂ + y₂ = x₁ * y₁ ∧ x₃ + y₃ = x₁ * y₁ ^ 2
          | _, _ => False
      8 ≤ G.girth → Nonempty (G ≃g Γ₃) ∧ G.girth = 8

Sources

• V. Dmytrenko, F. Lazebnik, and J. Williford, "On monomial graphs of girth eight", Finite Fields Appl. 13 (2007), 828–842, Theorem 3.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.