Plucking sunflowers

To pluck a sunflower with p ≥ 2 petals from a family of sets is to remove its petals and add its core. The core is contained in every petal, so every set of the family still contains a set of the plucked family (Pluck.exists_subset), and the family gets strictly smaller (Pluck.card_lt). Plucking until no sunflower with p petals is left therefore terminates after at most as many plucks as the family has sets, and, by the sunflower lemma, leaves a family of sets of size at most w with at most sunflowerBound p w sets (card_pluckNormalForm_le). This is the normalisation step of Razborov's method of approximations Jukna, Chapter 9.

Main definitions

• Cslib.Pluck: the relation of plucking one sunflower.
• Cslib.pluckNormalForm: a family reached by plucking that contains no sunflower with p petals.

Main results

• Cslib.relatesInSteps_pluckNormalForm: the normal form is reached in at most as many plucks as the family has sets.
• Cslib.card_pluckNormalForm_le: the size of a normal form of a family of small sets.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Pluck {α : Type u_1} [DecidableEq α] (p : ℕ) (F G : Finset (Finset α)) : Prop

G is obtained from F by plucking a sunflower with p petals: removing the petals and adding their core.

theorem Cslib.Pluck.card_lt {α : Type u_1} [DecidableEq α] {p : ℕ} {F G : Finset (Finset α)} (hp : 2 ≤ p) (h : Pluck p F G) : G.card < F.card

Plucking makes a family strictly smaller.

theorem Cslib.Pluck.exists_superset {α : Type u_1} [DecidableEq α] {p : ℕ} {F G : Finset (Finset α)} (hp : 2 ≤ p) (h : Pluck p F G) {t : Finset α} (ht : t ∈ G) : ∃ s ∈ F, t ⊆ s

Every set of a plucked family is a set of the family or contained in one.

theorem Cslib.Pluck.exists_subset {α : Type u_1} [DecidableEq α] {p : ℕ} {F G : Finset (Finset α)} (hp : 2 ≤ p) (h : Pluck p F G) {s : Finset α} (hs : s ∈ F) : ∃ t ∈ G, t ⊆ s

Every set of a family contains a set of the plucked family.

theorem Cslib.Pluck.forall_card_le {α : Type u_1} [DecidableEq α] {p w : ℕ} {F G : Finset (Finset α)} (hp : 2 ≤ p) (h : Pluck p F G) (hF : ∀ s ∈ F, s.card ≤ w) (t : Finset α) : t ∈ G → t.card ≤ w

Plucking keeps the sets of size at most w.

theorem Cslib.exists_relatesInSteps_not_containsSunflower {α : Type u_1} [DecidableEq α] {p : ℕ} (hp : 2 ≤ p) (F : Finset (Finset α)) : ∃ (G : Finset (Finset α)), ∃ m ≤ F.card, Relation.RelatesInSteps (Pluck p) F G m ∧ ¬ContainsSunflower p G

Plucking a family to the end takes at most as many plucks as it has sets.

noncomputable def Cslib.pluckNormalForm {α : Type u_1} [DecidableEq α] (p : ℕ) (F : Finset (Finset α)) : Finset (Finset α)

A family reached from F by plucking that contains no sunflower with p petals, for 2 ≤ p; for smaller p it is F itself.

theorem Cslib.relatesInSteps_pluckNormalForm {α : Type u_1} [DecidableEq α] {p : ℕ} (hp : 2 ≤ p) (F : Finset (Finset α)) : ∃ m ≤ F.card, Relation.RelatesInSteps (Pluck p) F (pluckNormalForm p F) m

For 2 ≤ p, the normal form of F is reached from F in at most F.card plucks.

theorem Cslib.not_containsSunflower_pluckNormalForm {α : Type u_1} [DecidableEq α] {p : ℕ} (hp : 2 ≤ p) (F : Finset (Finset α)) : ¬ContainsSunflower p (pluckNormalForm p F)

For 2 ≤ p, the normal form contains no sunflower with p petals.

theorem Cslib.forall_card_le_of_relatesInSteps_pluck {α : Type u_1} [DecidableEq α] {p w : ℕ} {F G : Finset (Finset α)} (hp : 2 ≤ p) {m : ℕ} (h : Relation.RelatesInSteps (Pluck p) F G m) (hF : ∀ s ∈ F, s.card ≤ w) (t : Finset α) : t ∈ G → t.card ≤ w

Plucking repeatedly keeps the sets of size at most w.

theorem Cslib.exists_subset_of_relatesInSteps_pluck {α : Type u_1} [DecidableEq α] {p : ℕ} {F G : Finset (Finset α)} (hp : 2 ≤ p) {m : ℕ} (h : Relation.RelatesInSteps (Pluck p) F G m) {s : Finset α} (hs : s ∈ F) : ∃ t ∈ G, t ⊆ s

After plucking repeatedly, every set of the family contains a set of the result.

theorem Cslib.forall_card_le_pluckNormalForm {α : Type u_1} [DecidableEq α] {p w : ℕ} {F : Finset (Finset α)} (hF : ∀ s ∈ F, s.card ≤ w) (t : Finset α) : t ∈ pluckNormalForm p F → t.card ≤ w

If every set of F has size at most w, so does every set of its normal form.

theorem Cslib.exists_subset_of_mem_pluckNormalForm {α : Type u_1} [DecidableEq α] {p : ℕ} {F : Finset (Finset α)} {s : Finset α} (hs : s ∈ F) : ∃ t ∈ pluckNormalForm p F, t ⊆ s

Every set of F contains a set of its normal form.

theorem Cslib.card_pluckNormalForm_le {α : Type u_1} [DecidableEq α] {p w : ℕ} {F : Finset (Finset α)} (hp : 2 ≤ p) (hF : ∀ s ∈ F, s.card ≤ w) : (pluckNormalForm p F).card ≤ sunflowerBound p w

A normal form of a family of sets of size at most w has at most sunflowerBound p w sets.