Turán numbers of cycles

DefinitionGraphs without cycles of lengths \(2k-1\) and \(2k\)#✓fully proved

For a natural number \(k\), a simple graph \(G\) is free of the cycle lengths \(2k-1\) and \(2k\) when it contains no copy of the cycle graph \(C_{2k-1}\) and no copy of the cycle graph \(C_{2k}\), where a copy is an injective graph homomorphism, that is, a subgraph that need not be induced.

Here \(C_m\) is the cycle graph on \(m\) vertices, which has no edges for \(m \le 1\) and is a single edge for \(m = 2\), and \(2k-1\) is computed in the natural numbers, so it is \(0\) when \(k = 0\).

def IsFreeOf574Cycles {V : Type*} (G : SimpleGraph V) (k : ℕ) : Prop :=
  (SimpleGraph.cycleGraph (2 * k - 1)).Free G ∧
    (SimpleGraph.cycleGraph (2 * k)).Free G
Used by 1

DefinitionExtremal number for cycles of lengths \(2k-1\) and \(2k\)#✓fully proved

For natural numbers \(k\) and \(n\), \(\mathrm{ex}(n; \{C_{2k-1}, C_{2k}\})\) is the supremum of the numbers of edges of the simple graphs on the vertex set \(\{0, \dots, n-1\}\) that contain no copy of the cycle graph \(C_{2k-1}\) and no copy of the cycle graph \(C_{2k}\), where the supremum of the empty set is \(0\). Here \(2k-1\) is computed in the natural numbers, so it is \(0\) when \(k = 0\).

noncomputable def extremalNumber (k n : ℕ) : ℕ :=
  sSup { e : ℕ | ∃ G : SimpleGraph (Fin n), IsFreeOf574Cycles G k ∧ G.edgeSet.ncard = e }
Uses 1 · Used by 1

DefinitionErdős Problem 574#✓fully proved

The statement that for every natural number \(k \ge 2\) the ratio \(\mathrm{ex}(n; \{C_{2k-1}, C_{2k}\}) / (n/2)^{1 + 1/k}\) tends to \(1\) as \(n \to \infty\), that is, \(\mathrm{ex}(n; \{C_{2k-1}, C_{2k}\}) = (1 + o(1)) (n/2)^{1 + 1/k}\). Here \(\mathrm{ex}(n; \{C_{2k-1}, C_{2k}\})\) is the extremal number: the supremum of the numbers of edges of simple graphs on \(n\) vertices that contain no copy of the cycle graph \(C_{2k-1}\) and no copy of the cycle graph \(C_{2k}\).

noncomputable def conjecture : Prop :=
  ∀ k : ℕ, 2 ≤ k →
    Filter.Tendsto
      (fun n : ℕ => (extremalNumber k n : ℝ) / (((n : ℝ) / 2) ^ (1 + 1 / (k : ℝ))))
      Filter.atTop (nhds 1)
Uses 1 · Used by 1

TheoremErdős Problem 574 is false#●ready to prove

It is not the case that for every natural number \(k \ge 2\) the ratio \(\mathrm{ex}(n; \{C_{2k-1}, C_{2k}\}) / (n/2)^{1 + 1/k}\) tends to \(1\) as \(n \to \infty\). Here \(\mathrm{ex}(n; \{C_{2k-1}, C_{2k}\})\) is the extremal number: the supremum of the numbers of edges of simple graphs on \(n\) vertices that contain no copy of the cycle graph \(C_{2k-1}\) and no copy of the cycle graph \(C_{2k}\).

Lazebnik, Ustimenko and Woldar (Discrete Math. 1999), per Füredi–Simonovits (arXiv:1306.5167, Construction 4.28), blow up one side of Benson's girth-12 bipartite graph to get bipartite \(C_{10}\)-free graphs (hence also \(C_9\)-free) with \(4(n/5)^{6/5} > 0.5798\, n^{6/5}\) edges for infinitely many \(n\), refuting the case \(k = 5\).

public theorem_wanted conjecture_refuted : ¬ conjecture
Sources
  • Zoltán Füredi and Miklós Simonovits, The history of degenerate (bipartite) extremal graph problems, in Erdős Centennial, Bolyai Soc. Math. Stud. 25 (2013), arXiv:1306.5167, https://arxiv.org/abs/1306.5167.
Uses 1
Statement usesErdős Problem 574
3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.