Erdős Problem 20

References:

• erdosproblems.com/20
• Wikipedia
• [ErRa60] Erdős, Paul and Rado, Richard. Intersection theorems for systems of sets. J. London Math. Soc. 35 (1960), 85--90.

noncomputable def Erdos20.f (n k : ℕ) : ℕ

Let $f(n,k)$ be minimal such that every $F$ family of $n$-uniform sets with $|F| \ge f(n,k)$ contains a $k$-sunflower.

Equations

• Erdos20.f n k = sInf {m : ℕ | ∀ {α : Type} (F : Set (Set α)), (∀ f ∈ F, f.ncard = n) ∧ m ≤ F.ncard → ∃ S ⊆ F, S.ncard = k ∧ IsSunflower S}

theorem Erdos20.f_0_1 : f 0 1 = 1

theorem Erdos20.erdos_20 : sorry ↔ ∃ (c : ℕ → ℕ), ∀ (n k : ℕ), n > 0 → f n k < c k ^ n

Is it true that $f(n,k) < c_k^n$ for some constant $c_k>0$ and for all $n > 0$?

theorem Erdos20.erdos_20.variants.erdos_rado_bound (n k : ℕ) : n > 0 → 2 ≤ k → f n k ≤ (k - 1) ^ n * n.factorial + 1

Erdős and Rado [ErRa60] proved the factorial upper bound for the $k$-sunflower threshold: any family of $n$-uniform sets with more than $(k-1)^n \, n!$ members contains a $k$-sunflower, hence $f(n,k) \le (k-1)^n \, n! + 1$.