The elementary sunflower bound

The Erdős--Rado induction used by the monotone CLIQUE approximation method is formalized here for finite set families. A p-sunflower is a p-element subfamily whose distinct members have one common pairwise intersection.

The quantitative endpoint is the classical elementary bound

family.card > (p - 1) ^ width * width!.

For families whose members have size at most width, the proof partitions the family by cardinality and applies the uniform bound to a large layer.

def Algebraic.Sunflower.IsSunflowerWithCore {α : Type u_1} [DecidableEq α] (petals : Finset (Finset α)) (core : Finset α) : Prop

A finite family has a common pairwise intersection core.

Equations

• Algebraic.Sunflower.IsSunflowerWithCore petals core = ∀ {left : Finset α}, left ∈ petals → ∀ {right : Finset α}, right ∈ petals → left ≠ right → left ∩ right = core

def Algebraic.Sunflower.ContainsSunflower {α : Type u_1} [DecidableEq α] (p : ℕ) (family : Finset (Finset α)) : Prop

A family contains a sunflower with exactly p petals.

Equations

• Algebraic.Sunflower.ContainsSunflower p family = ∃ petals ⊆ family, petals.card = p ∧ ∃ (core : Finset α), Algebraic.Sunflower.IsSunflowerWithCore petals core

theorem Algebraic.Sunflower.isSunflowerWithCore_empty_of_pairwiseDisjoint {α : Type u_1} [DecidableEq α] {petals : Finset (Finset α)} (disjoint : (↑petals).Pairwise fun (left right : Finset α) => Disjoint left right) : IsSunflowerWithCore petals ∅

Pairwise disjoint sets form a sunflower with empty core.

theorem Algebraic.Sunflower.pairwiseDisjoint_mono {α : Type u_1} {small large : Finset (Finset α)} (subset : small ⊆ large) (disjoint : (↑large).Pairwise fun (left right : Finset α) => Disjoint left right) : (↑small).Pairwise fun (left right : Finset α) => Disjoint left right

A subfamily inherits pairwise disjointness.

theorem Algebraic.Sunflower.containsSunflower_of_uniform {α : Type u_1} [DecidableEq α] (petals : ℕ) (two_le : 2 ≤ petals) (width : ℕ) (family : Finset (Finset α)) (uniform : ∀ set ∈ family, set.card = width) (large : (petals - 1) ^ width * width.factorial < family.card) : ContainsSunflower petals family

The classical uniform Erdős--Rado sunflower bound.

def Algebraic.Sunflower.bound (petals width : ℕ) : ℕ

The size bound used for families of sets of size at most width. The extra width + 1 partitions the family into uniform layers.

Equations

• Algebraic.Sunflower.bound petals width = (width + 1) * ((petals - 1) ^ width * width.factorial)

theorem Algebraic.Sunflower.containsSunflower_of_bounded {α : Type u_1} [DecidableEq α] (petals : ℕ) (two_le : 2 ≤ petals) (width : ℕ) (family : Finset (Finset α)) (bounded : ∀ set ∈ family, set.card ≤ width) (large : bound petals width < family.card) : ContainsSunflower petals family

The elementary sunflower lemma for bounded-size set families.