Erdős Problem 857

Reference: erdosproblems.com/857

For fixed n, k, let m(n, k) be minimal such that every family of subsets of [n] of size at least m(n, k) contains a k-sunflower. The problem asks to estimate m(n, k), ideally asymptotically.

noncomputable def Erdos857.m (n k : ℕ) : ℕ

m(n, k): minimal sunflower-forcing family size in the non-uniform [n] model.

Equations

• Erdos857.m n k = sInf {t : ℕ | ∀ (F : Set (Set (Fin n))), t ≤ F.ncard → ∃ S ⊆ F, S.ncard = k ∧ IsSunflower S}

theorem Erdos857.erdos_857 : have f := sorry; ∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun (n : ℕ) => ↑(m n k) / f k n) Filter.atTop (nhds 1)

Estimate m(n,k), or better give an asymptotic formula.