Ruzsa–Szemerédi (6,3) theorem

DefinitionThe (6, 3) extremal number#✓fully proved

For \(n \in \mathbb{N}\), \(\mathrm{ex}_3(n)\) is the largest number of \(3\)-element subsets of \(\{1, \dots, n\}\) such that every set of at most \(6\) of these points contains at most \(2\) of the chosen subsets.

For \(n \ge 6\) this is the extremal number \(\mathrm{ex}_3(n, \mathcal{F})\) of the family \(\mathcal{F}\) of \(3\)-uniform hypergraphs with \(6\) vertices and \(3\) edges, since a set of triples contains a member of \(\mathcal{F}\) exactly when some \(6\) points carry \(3\) of the triples.

noncomputable def sixThreeExtremalNumber (n : ℕ) : ℕ :=
  sSup {e | ∃ E : Finset (Finset (Fin n)), (∀ t ∈ E, t.card = 3) ∧
    (∀ S : Finset (Fin n), S.card ≤ 6 → (E.filter (· ⊆ S)).card ≤ 2) ∧ E.card = e}

Used by 1

Used byThe Brown–Erdős–Sós (6, 3) conjecture

DefinitionThe Brown–Erdős–Sós (6, 3) conjecture#✓fully proved

For \(n \in \mathbb{N}\) let \(\mathrm{ex}_3(n)\) be the largest number of \(3\)-element subsets of \(\{1, \dots, n\}\) such that every set of at most \(6\) of these points contains at most \(2\) of the chosen subsets. The conjecture (Erdős Problem 716) is the proposition that \(\mathrm{ex}_3(n) / n^2 \to 0\) as \(n \to \infty\), that is, \(\mathrm{ex}_3(n) = o(n^2)\).

def sixThreeExtremalNumberLittleO : Prop :=
  Tendsto (fun n : ℕ => (sixThreeExtremalNumber n : ℝ) / (n : ℝ) ^ 2) atTop (𝓝 0)

Uses 1 · Used by 1

Statement usesThe (6, 3) extremal number

Used byThe Ruzsa–Szemerédi (6, 3) theorem

TheoremThe Ruzsa–Szemerédi (6, 3) theorem#●ready to prove

For \(n \in \mathbb{N}\) let \(\mathrm{ex}_3(n)\) be the largest number of \(3\)-element subsets of \(\{1, \dots, n\}\) such that every set of at most \(6\) of these points contains at most \(2\) of the chosen subsets. Then \(\mathrm{ex}_3(n) / n^2 \to 0\) as \(n \to \infty\), that is, \(\mathrm{ex}_3(n) = o(n^2)\).

public theorem_wanted sixThreeExtremalNumberLittleO_holds : sixThreeExtremalNumberLittleO

Sources

• T. F. Bloom, Erdős Problems, Problem #716, https://www.erdosproblems.com/716 (status PROVED (LEAN)); resolution: I. Z. Ruzsa and E. Szemerédi, Triple systems with no six points carrying three triangles, Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976), Vol. II (1978), 939-945, erdosproblems.com/716: 'The answer is yes, proved by Ruzsa and Szemerédi' (the Ruzsa-Szemerédi problem), https://www.erdosproblems.com/716.

Uses 1

Statement usesThe Brown–Erdős–Sós (6, 3) conjecture

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.