Generalized Turán numbers

DefinitionGeneralized Turán number#✓fully proved

Let \(n\) be a natural number and let \(T\) and \(H\) be simple graphs, where \(T\) has finitely many vertices. A copy of a graph in a graph \(G\) is a subgraph of \(G\) isomorphic to it, and \(G\) is \(H\)-free if it contains no copy of \(H\). The generalized Turán number \(\mathrm{ex}(n, T, H)\) is the largest number of copies of \(T\) in an \(H\)-free simple graph on the vertex set \(\{0, 1, \dots, n-1\}\), and is \(0\) if there is no such graph.

The source considers graphs \(T\) and \(H\) without isolated vertices; the definition does not require this.

public noncomputable def generalizedExtremalNumber (n : ℕ)
    {α β : Type*} [Fintype α]
    (T : SimpleGraph α) (H : SimpleGraph β) : ℕ := by
  classical
  exact Finset.sup (Finset.univ.filter (fun G : SimpleGraph (Fin n) => H.Free G))
    (fun G => G.copyCount T)

Used by 4

Used byThe generalized Turán number is an upper bound · The generalized Turán number is attained · The generalized Turán number as a supremum · Upper bounds for the generalized Turán number

TheoremThe generalized Turán number as a supremum#✓fully proved

Let \(n\) be a natural number and let \(T\) and \(H\) be simple graphs, where \(T\) has finitely many vertices. Then the generalized Turán number \(\mathrm{ex}(n, T, H)\) is the supremum in \(\mathbb{N}\), with the supremum of the empty family taken to be \(0\), of the number of copies of \(T\) in \(G\) over all simple graphs \(G\) on the vertex set \(\{0, 1, \dots, n-1\}\) that contain no copy of \(H\) (a subgraph isomorphic to \(H\)).

public theorem generalizedExtremalNumber_eq_sup (n : ℕ)
    {α β : Type*} [Fintype α]
    (T : SimpleGraph α) (H : SimpleGraph β) :
    generalizedExtremalNumber n T H =
      Finset.sup (Finset.univ.filter (fun G : SimpleGraph (Fin n) => H.Free G))
        (fun G => G.copyCount T)

Uses 1 · Used by 1

Statement usesGeneralized Turán number

Used byThe generalized Turán number is attained

TheoremThe generalized Turán number is an upper bound#✓fully proved

Let \(n\) be a natural number and let \(T\) and \(H\) be simple graphs, where \(T\) has finitely many vertices. If \(G\) is a simple graph on the vertex set \(\{0, 1, \dots, n-1\}\) that contains no copy of \(H\) (a subgraph isomorphic to \(H\)), then the number of copies of \(T\) in \(G\) is at most the generalized Turán number \(\mathrm{ex}(n, T, H)\).

public theorem copyCount_le_generalizedExtremalNumber (n : ℕ)
    {α β : Type*} [Fintype α]
    (T : SimpleGraph α) (H : SimpleGraph β)
    (G : SimpleGraph (Fin n)) (hG : H.Free G) :
    G.copyCount T ≤ generalizedExtremalNumber n T H

Uses 1

Statement usesGeneralized Turán number

TheoremUpper bounds for the generalized Turán number#✓fully proved

Let \(n\) and \(m\) be natural numbers and let \(T\) and \(H\) be simple graphs, where \(T\) has finitely many vertices. Then the generalized Turán number \(\mathrm{ex}(n, T, H)\) is at most \(m\) if and only if every simple graph on the vertex set \(\{0, 1, \dots, n-1\}\) that contains no copy of \(H\) (a subgraph isomorphic to \(H\)) has at most \(m\) copies of \(T\).

public theorem generalizedExtremalNumber_le_iff (n : ℕ)
    {α β : Type*} [Fintype α]
    (T : SimpleGraph α) (H : SimpleGraph β)
    (m : ℕ) :
    generalizedExtremalNumber n T H ≤ m ↔
      ∀ G : SimpleGraph (Fin n), H.Free G → G.copyCount T ≤ m

Uses 1

Statement usesGeneralized Turán number

TheoremThe generalized Turán number is attained#✓fully proved

Let \(n\) be a natural number and let \(T\) and \(H\) be simple graphs, where \(T\) has finitely many vertices. If some simple graph on the vertex set \(\{0, 1, \dots, n-1\}\) contains no copy of \(H\) (a subgraph isomorphic to \(H\)), then some such graph \(G\) has exactly \(\mathrm{ex}(n, T, H)\) copies of \(T\), where \(\mathrm{ex}(n, T, H)\) is the generalized Turán number.

public theorem exists_free_copyCount_eq_generalizedExtremalNumber (n : ℕ)
    {α β : Type*} [Fintype α]
    (T : SimpleGraph α) (H : SimpleGraph β)
    (hne : ∃ G : SimpleGraph (Fin n), H.Free G) :
    ∃ G : SimpleGraph (Fin n), H.Free G ∧ G.copyCount T = generalizedExtremalNumber n T H

Uses 2

Statement usesGeneralized Turán number

Proof usesThe generalized Turán number as a supremum

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.