turan_petersen_free
Provedcombinatoricsconjectureextremal-combinatoricsgraph-theory
Turán-type problem for Petersen-free graphs: Max edges in n-vertex graph with no Petersen subgraph. Turán density π(Petersen) is unknown; conjectured 3/4 by Bondy–Simonovits.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem turan_petersen_free :
∀ eps : ℝ, 0 < eps →
∃ N : ℕ, ∀ (n : ℕ) (_ : N ≤ n) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
let petersen_edges : Finset (ℕ × ℕ) :=
{(0,1),(1,2),(2,3),(3,4),(4,0),(0,5),(1,6),(2,7),(3,8),(4,9),
(5,7),(7,9),(9,6),(6,8),(8,5)}
(¬∃ (phi : Fin 10 → Fin n), Function.Injective phi ∧
∀ i j : Fin 10, (i.val, j.val) ∈ petersen_edges → G.Adj (phi i) (phi j)) →
(G.edgeFinset.card : ℝ) ≤ (3/4 + eps) * n * (n - 1) / 2 := by
sorrySource