Erdős Problem 20

References:

• erdosproblems.com/20
• Wikipedia

def Erdos20.IsSunflowerWithKernel {α : Type} (F : Set (Set α)) (S : Set α) : Prop

A sunflower $F$ with kernel $S$ is a collection of sets in which all possible distinct pairs of sets share the same intersection $S$.

Equations

• Erdos20.IsSunflowerWithKernel F S = F.Pairwise fun (A B : Set α) => A ∩ B = S

theorem Erdos20.isSunflowerWithKernel_empty {α : Type} (S : Set α) : IsSunflowerWithKernel ∅ S

theorem Erdos20.isSunflowerWithKernel_singleton {α : Type} (S A : Set α) : IsSunflowerWithKernel {A} S

def Erdos20.IsSunflower {α : Type} (F : Set (Set α)) : Prop

A sunflower $F$ is a collection of sets in which all possible distinct pairs of sets share the same intersection.

Equations

• Erdos20.IsSunflower F = ∃ (S : Set α), Erdos20.IsSunflowerWithKernel F S

theorem Erdos20.isSunflower_empty {α : Type} : IsSunflower ∅

theorem Erdos20.isSunflower_singleton {α : Type} (A : Set α) : IsSunflower {A}

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 ∧ Erdos20.IsSunflower S}

theorem Erdos20.f_0_1 : f 0 1 = 1

theorem Erdos20.erdos_20 : True ↔ ∃ (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$?