Lower bounds for the sunflower lemma

The sunflower lemma (containsSunflower_of_forall_card_le) finds a sunflower with p petals in every family of more than (p - 1) ^ w * w! sets of size at most w. Erdős and Rado also showed that the factor (p - 1) ^ w cannot be dropped Erdős and Rado: the graphs {(i, f i) | i : ι} of all functions f : ι → β form a family of |β| ^ |ι| sets of size |ι| without a sunflower with |β| + 1 petals (not_containsSunflower_graphFamily). Indeed, among |β| + 1 graphs, at each coordinate i some pair agrees. Thus every petal is contained in the core, which is impossible for two distinct petals. Taking ι = Fin w and β = Fin (p - 1) gives (p - 1) ^ w sets of size w without a sunflower with p petals (exists_card_eq_pow_not_containsSunflower).

For w = 1 the two bounds meet: distinct sets of size at most one are pairwise disjoint, so a family of such sets contains a sunflower with p petals exactly when it has at least p members (containsSunflower_iff_le_card). For w = 2 and p = 3 the product construction is not optimal: two disjoint triangles are six edges without a sunflower with three petals (not_containsSunflower_twoTriangles), more than the (3 - 1) ^ 2 = 4 edges of the construction.

Main definitions

• Cslib.Sunflower.functionGraph: the graph of a function on a finite type, as a finite set.
• Cslib.Sunflower.graphFamily: the graphs of all functions ι → β.
• Cslib.Sunflower.twoTriangles: the edges of two disjoint triangles.

Main results

• Cslib.Sunflower.not_containsSunflower_graphFamily: the graph family has no sunflower with |β| + 1 petals.
• Cslib.exists_card_eq_pow_not_containsSunflower: (p - 1) ^ w sets of size w without a sunflower with p petals.
• Cslib.containsSunflower_iff_le_card: for sets of size at most one, a sunflower with p petals exists exactly when there are at least p sets.
• Cslib.Sunflower.not_containsSunflower_twoTriangles: six sets of size two without a sunflower with three petals.

References

• P. Erdős, R. Rado, Intersection theorems for systems of sets

Graphs of functions

def Cslib.Sunflower.functionGraph {ι : Type u_1} {β : Type u_2} [Fintype ι] (f : ι → β) : Finset (ι × β)

The graph {(i, f i) | i : ι} of a function on a finite type, as a finite set.

@[simp]

theorem Cslib.Sunflower.mem_functionGraph {ι : Type u_1} {β : Type u_2} [Fintype ι] {f : ι → β} {x : ι × β} : x ∈ functionGraph f ↔ f x.1 = x.2

A pair lies in the graph of f exactly when its second component is the value of f at its first.

@[simp]

theorem Cslib.Sunflower.card_functionGraph {ι : Type u_1} {β : Type u_2} [Fintype ι] (f : ι → β) : (functionGraph f).card = Fintype.card ι

The graph of a function on ι has |ι| elements.

theorem Cslib.Sunflower.functionGraph_injective {ι : Type u_1} {β : Type u_2} [Fintype ι] : Function.Injective functionGraph

A function is determined by its graph.

def Cslib.Sunflower.graphFamily (ι : Type u_3) (β : Type u_4) [Fintype ι] [DecidableEq ι] [Fintype β] : Finset (Finset (ι × β))

The graphs of all functions ι → β.

theorem Cslib.Sunflower.mem_graphFamily {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] {s : Finset (ι × β)} : s ∈ graphFamily ι β ↔ ∃ (f : ι → β), functionGraph f = s

The members of the graph family are the graphs of functions.

theorem Cslib.Sunflower.card_graphFamily {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] : (graphFamily ι β).card = Fintype.card β ^ Fintype.card ι

There are |β| ^ |ι| graphs of functions ι → β.

theorem Cslib.Sunflower.card_of_mem_graphFamily {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] {s : Finset (ι × β)} (hs : s ∈ graphFamily ι β) : s.card = Fintype.card ι

Every graph of a function on ι has |ι| elements.

theorem Cslib.Sunflower.not_containsSunflower_graphFamily {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] [Nonempty β] : ¬ContainsSunflower (Fintype.card β + 1) (graphFamily ι β)

Erdős–Rado lower bound. The graphs of all functions ι → β, for nonempty β, contain no sunflower with |β| + 1 petals: at each coordinate some pair of petals agrees, so every petal is contained in the core.

theorem Cslib.exists_card_eq_pow_not_containsSunflower (p w : ℕ) (hp : 2 ≤ p) : ∃ (F : Finset (Finset (Fin w × Fin (p - 1)))), F.card = (p - 1) ^ w ∧ (∀ s ∈ F, s.card = w) ∧ ¬ContainsSunflower p F

Erdős–Rado lower bound. For p ≥ 2 there are (p - 1) ^ w sets of size w without a sunflower with p petals: the graphs of all functions Fin w → Fin (p - 1).

Sets of size at most one

theorem Cslib.containsSunflower_iff_le_card {α : Type u_1} [DecidableEq α] {F : Finset (Finset α)} (hF : ∀ s ∈ F, s.card ≤ 1) (p : ℕ) : ContainsSunflower p F ↔ p ≤ F.card

For a family of sets of size at most one, which are pairwise disjoint when distinct, a sunflower with p petals exists exactly when the family has at least p sets. With the sunflower lemma for w = 1 this shows that its bound p - 1 is exact.

Two disjoint triangles

def Cslib.Sunflower.twoTriangles : Finset (Finset (Fin 6))

The six edges of two disjoint triangles on Fin 6.

theorem Cslib.Sunflower.card_twoTriangles : twoTriangles.card = 6

The two triangles have six edges.

theorem Cslib.Sunflower.card_of_mem_twoTriangles (s : Finset (Fin 6)) : s ∈ twoTriangles → s.card = 2

Every edge of the two triangles has two vertices.

theorem Cslib.Sunflower.not_containsSunflower_twoTriangles : ¬ContainsSunflower 3 twoTriangles

Two disjoint triangles contain no sunflower with three petals: such a sunflower of edges consists of three edges through a common vertex or of three pairwise disjoint edges, but every vertex has degree two and every three edges include two of the same triangle. So the product construction, with (3 - 1) ^ 2 = 4 sets, is not optimal for w = 2 and p = 3. The proof checks all triples of edges by decide.