hypergraph_turan_fano
Provedcombinatoricsconjectureextremal-combinatoricsgraph-theoryhypergraph-theory
Fano plane Turán problem: Maximum 3-uniform hyperedges on n vertices with no Fano plane subhypergraph. Conjectured to be 3/4·C(n,3) achieved by a blow-up of K₄. De Caen–Füredi proved 3/4+o(1) is an upper bound; whether 3/4 is the exact limit is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem hypergraph_turan_fano :
∀ eps : ℝ, 0 < eps →
∃ N : ℕ, ∀ (n : ℕ) (_ : N ≤ n)
(H : Finset (Finset (Fin n))),
(∀ e ∈ H, e.card = 3) →
(¬∃ (lines : Fin 7 → Finset (Fin n)),
(∀ i, (lines i).card = 3) ∧
(∀ i j : Fin 7, i ≠ j → (lines i ∩ lines j).card = 1) ∧
∀ i, lines i ∈ H) →
(H.card : ℝ) ≤ (3/4 + eps) * Nat.choose n 3 := by
sorrySource