(* author: R. Thiemann *) section ‹The Sunflower Lemma› text ‹We formalize the proof of the sunflower lemma of Erd\H{o}s and Rado~\<^cite>‹"erdos_rado"›, as it is presented in the textbook~\<^cite>‹‹Chapter~6› in "book"›. We further integrate Exercise 6.2 from the textbook, which provides a lower bound on the existence of sunflowers.› theory Erdos_Rado_Sunflower imports Sunflower begin text ‹When removing an element from all subsets, then one can afterwards add these elements to a sunflower and get a new sunflower.› lemma sunflower_remove_element_lift: assumes S: "S ⊆ { A - {a} | A . A ∈ F ∧ a ∈ A}" and sf: "sunflower S" shows "∃ Sa. sunflower Sa ∧ Sa ⊆ F ∧ card Sa = card S ∧ Sa = insert a ` S" proof (intro exI[of _ "insert a ` S"] conjI refl) let ?Sa = "insert a ` S" { fix B assume "B ∈ ?Sa" then obtain C where C: "C ∈ S" and B: "B = insert a C" by auto from C S obtain T where "T ∈ F" "a ∈ T" "C = T - {a}" by auto with B have "B = T" by auto with ‹T ∈ F› have "B ∈ F" by auto } thus SaF: "?Sa ⊆ F" by auto have inj: "inj_on (insert a) S" using S by (intro inj_on_inverseI[of _ "λ B. B - {a}"], auto) thus "card ?Sa = card S" by (rule card_image) show "sunflower ?Sa" unfolding sunflower_def proof (intro allI, intro impI) fix x assume "∃C D. C ∈ ?Sa ∧ D ∈ ?Sa ∧ C ≠ D ∧ x ∈ C ∧ x ∈ D" then obtain C D where *: "C ∈ ?Sa" "D ∈ ?Sa" "C ≠ D" "x ∈ C" "x ∈ D" by auto from *(1-2) obtain C' D' where **: "C' ∈ S" "D' ∈ S" "C = insert a C'" "D = insert a D'" by auto with ‹C ≠ D› inj have CD': "C' ≠ D'" by auto show "∀E. E ∈ ?Sa ⟶ x ∈ E" proof (cases "x = a") case False with * ** have "x ∈ C'" "x ∈ D'" by auto with ** CD' have "∃C D. C ∈ S ∧ D ∈ S ∧ C ≠ D ∧ x ∈ C ∧ x ∈ D" by auto from sf[unfolded sunflower_def, rule_format, OF this] show ?thesis by auto qed auto qed qed text ‹The sunflower-lemma of Erd\H{o}s and Rado: if a set has a certain size and all elements have the same cardinality, then a sunflower exists.› lemma Erdos_Rado_sunflower_same_card: assumes "∀ A ∈ F. finite A ∧ card A = k" and "card F > (r - 1)^k * fact k" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ {} ∉ S" using assms proof (induct k arbitrary: F) case 0 hence "F = {{}} ∨ F = {}" "card F ≥ 2" by auto hence False by auto thus ?case by simp next case (Suc k F) define pd_sub :: "'a set set ⇒ nat ⇒ bool" where "pd_sub = (λ G t. G ⊆ F ∧ card G = t ∧ pairwise disjnt G ∧ {} ∉ G)" show ?case proof (cases "∃ t G. pd_sub G t ∧ t ≥ r") case True then obtain t G where pd_sub: "pd_sub G t" and t: "t ≥ r" by auto from pd_sub[unfolded pd_sub_def] pairwise_disjnt_imp_sunflower have *: "G ⊆ F" "card G = t" "sunflower G" "{} ∉ G" by auto from t ‹card G = t› obtain H where "H ⊆ G" "card H = r" by (metis obtain_subset_with_card_n) with sunflower_subset[OF ‹H ⊆ G›] * show ?thesis by blast next case False define P where "P = (λ t. ∃ G. pd_sub G t)" have ex: "∃ t. P t" unfolding P_def by (intro exI[of _ 0] exI[of _ "{}"], auto simp: pd_sub_def) have large': "⋀ t. P t ⟹ t < r" using False unfolding P_def by auto hence large: "⋀ t. P t ⟹ t ≤ r" by fastforce define t where "t = (GREATEST t. P t)" from GreatestI_ex_nat[OF ex large, folded t_def] have Pt: "P t" . from Greatest_le_nat[of P, OF _ large] have greatest: "⋀ s. P s ⟹ s ≤ t" unfolding t_def by auto from large'[OF Pt] have tr: "t ≤ r - 1" by simp from Pt[unfolded P_def pd_sub_def] obtain G where cardG: "card G = t" and disj: "pairwise disjnt G" and GF: "G ⊆ F" by blast define A where "A = (⋃ G)" from Suc(3) have "card F > 0" by simp hence "finite F" by (rule card_ge_0_finite) from GF ‹finite F› have finG: "finite G" by (rule finite_subset) have "card (⋃ G) ≤ sum card G" using card_Union_le_sum_card by blast also have "… ≤ of_nat (card G) * Suc k" by (metis GF Suc.prems(1) le_Suc_eq subsetD sum_bounded_above) also have "… ≤ (r - 1) * Suc k" using tr[folded cardG] by (metis id_apply mult_le_mono1 of_nat_eq_id) finally have cardA: "card A ≤ (r - 1) * Suc k" unfolding A_def . { fix B assume *: "B ∈ F" with Suc(2) have nE: "B ≠ {}" by auto from Suc(2) have eF: "{} ∉ F" by auto have "B ∩ A ≠ {}" proof assume dis: "B ∩ A = {}" hence disj: "pairwise disjnt ({B} ∪ G)" using disj unfolding A_def by (smt (verit, ccfv_SIG) Int_commute Un_iff Union_disjoint disjnt_def pairwise_def singleton_iff) from nE dis have "B ∉ G" unfolding A_def by auto with finG have c: "card ({B} ∪ G) = Suc t" by (simp add: cardG) have "P (Suc t)" unfolding P_def pd_sub_def by (intro exI[of _ "{B} ∪ G"], insert eF disj c * GF, auto) with greatest show False by force qed } note overlap = this have "F ≠ {}" using Suc(2-) by auto with overlap have Ane: "A ≠ {}" unfolding A_def by auto have "finite A" unfolding A_def using finG Suc(2-) GF by auto let ?g = "λ B x. x ∈ B ∩ A" define f where "f = (λ B. SOME x. ?g B x)" have "f ∈ F → A" proof fix B assume "B ∈ F" from overlap[OF this] have "∃ x. ?g B x" unfolding A_def by auto from someI_ex[OF this] show "f B ∈ A" unfolding f_def by auto qed from pigeonhole_card[OF this ‹finite F› ‹finite A› Ane] obtain a where a: "a ∈ A" and le: "card F ≤ card (f -` {a} ∩ F) * card A" by auto { fix S assume "S ∈ F" "f S ∈ {a}" with someI_ex[of "?g S"] a overlap[OF this(1)] have "a ∈ S" unfolding f_def by auto } note FaS = this let ?F = "{S - {a} | S . S ∈ F ∧ f S ∈ {a}}" from cardA have "((r - 1) ^ k * fact k) * card A ≤ ((r - 1) ^ k * fact k) * ((r - 1) * Suc k)" by simp also have "… = (r - 1) ^ (Suc k) * fact (Suc k)" by (metis (no_types, lifting) fact_Suc mult.assoc mult.commute of_nat_id power_Suc2) also have "… < card (f -` {a} ∩ F) * card A" using Suc(3) le by auto also have "f -` {a} ∩ F = {S ∈ F. f S ∈ {a}}" by auto also have "card … = card ((λ S. S - {a}) ` {S ∈ F. f S ∈ {a}})" by (subst card_image; intro inj_onI refl, insert FaS) auto also have "(λ S. S - {a}) ` {S ∈ F. f S ∈ {a}} = ?F" by auto finally have lt: "(r - 1) ^ k * fact k < card ?F" by simp have "∀ A ∈ ?F. finite A ∧ card A = k" using Suc(2) FaS by auto from Suc(1)[OF this lt] obtain S where "sunflower S" "card S = r" "S ⊆ ?F" by auto from ‹S ⊆ ?F› FaS have "S ⊆ {A - {a} |A. A ∈ F ∧ a ∈ A}" by auto from sunflower_remove_element_lift[OF this ‹sunflower S›] ‹card S = r› show ?thesis by auto qed qed text ‹Using @{thm [source] sunflower_card_subset_lift} we can easily replace the condition that the cardinality is exactly @{term k} by the requirement that the cardinality is at most @{term k}. However, then @{term "{} ∉ S"} cannot be ensured. Consider @{term "(r :: nat) = 1 ∧ (k :: nat) > 0 ∧ F = {{}}"}.› lemma Erdos_Rado_sunflower: assumes "∀ A ∈ F. finite A ∧ card A ≤ k" and "card F > (r - 1)^k * fact k" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r" by (rule sunflower_card_subset_lift[OF _ assms], metis Erdos_Rado_sunflower_same_card) text ‹We further provide a lower bound on the existence of sunflowers, i.e., Exercise 6.2 of the textbook~\<^cite>‹"book"›. To be more precise, we prove that there is a set of sets of cardinality @{term ‹(r - 1 :: nat)^k›}, where each element is a set of cardinality @{term k}, such that there is no subset which is a sunflower with cardinality of at least @{term r}.› lemma sunflower_lower_bound: assumes inf: "infinite (UNIV :: 'a set)" and r: "r ≠ 0" and rk: "r = 1 ⟹ k ≠ 0" shows "∃ F. card F = (r - 1)^k ∧ finite F ∧ (∀ A ∈ F. finite (A :: 'a set) ∧ card A = k) ∧ (∄ S. S ⊆ F ∧ sunflower S ∧ card S ≥ r)" proof (cases "r = 1") case False with r have r: "r > 1" by auto show ?thesis proof (induct k) case 0 have id: "S ⊆ {{}} ⟷ (S = {} ∨ S = {{}})" for S :: "'a set set" by auto show ?case using r by (intro exI[of _ "{{}}"], auto simp: id) next case (Suc k) then obtain F where cardF: "card F = (r - 1) ^ k" and fin: "finite F" and AF: "⋀ A. (A :: 'a set) ∈ F ⟹ finite A ∧ card A = k" and sf: "¬ (∃S⊆F. sunflower S ∧ r ≤ card S)" by metis text ‹main idea: get @{term "k-1 :: nat"} fresh elements and add one of these to all elements of F› have "finite (⋃ F)" using fin AF by simp hence "infinite (UNIV - ⋃ F)" using inf by simp from infinite_arbitrarily_large[OF this, of "r - 1"] obtain New where New: "finite New" "card New = r - 1" "New ∩ ⋃ F = {}" by auto define G where "G = (λ (A, a). insert a A) ` (F × New)" show ?case proof (intro exI[of _ G] conjI) show "finite G" using New fin unfolding G_def by simp have "card G = card (F × New)" unfolding G_def proof ((subst card_image; (intro refl)?), intro inj_onI, clarsimp, goal_cases) case (1 A a B b) hence ab: "a = b" using New by auto from 1(1) have "insert a A - {a} = insert b B - {a}" by simp also have "insert a A - {a} = A" using New 1 by auto also have "insert b B - {a} = B" using New 1 ab[symmetric] by auto finally show ?case using ab by auto qed also have "… = card F * card New" using New fin by auto finally show "card G = (r - 1) ^ Suc k" unfolding cardF New by simp { fix B assume "B ∈ G" then obtain a A where G: "a ∈ New" "A ∈ F" "B = insert a A" unfolding G_def by auto with AF[of A] New have "finite B" "card B = Suc k" by (auto simp: card_insert_if) } thus "∀A∈G. finite A ∧ card A = Suc k" by auto show "¬ (∃S⊆G. sunflower S ∧ r ≤ card S)" proof (intro notI, elim exE conjE) fix S assume *: "S ⊆ G" "sunflower S" "r ≤ card S" define g where "g B = (SOME a. a ∈ New ∧ a ∈ B)" for B { fix B assume "B ∈ S" with ‹S ⊆ G› have "B ∈ G" by auto hence "∃ a. a ∈ New ∧ a ∈ B" unfolding G_def by auto from someI_ex[OF this, folded g_def] have "g B ∈ New" "g B ∈ B" by auto } note gB = this have "card (g ` S) ≤ card New" by (rule card_mono, insert New gB, auto) also have "… < r" unfolding New using r by simp also have "… ≤ card S" by fact finally have "card (g ` S) < card S" . from pigeonhole[OF this] have "¬ inj_on g S" . then obtain B1 B2 where B12: "B1 ∈ S" "B2 ∈ S" "B1 ≠ B2" "g B1 = g B2" unfolding inj_on_def by auto define a where "a = g B2" from B12 gB[of B1] gB[of B2] have a: "a ∈ New" "a ∈ B1" "a ∈ B2" unfolding a_def by auto with B12 have "∃B1 B2. B1 ∈ S ∧ B2 ∈ S ∧ B1 ≠ B2 ∧ a ∈ B1 ∧ a ∈ B2" unfolding a_def by blast from ‹sunflower S›[unfolded sunflower_def, rule_format, OF this] have aS: "B ∈ S ⟹ a ∈ B" for B by auto define h where "h B = B - {a}" for B define T where "T = h ` S" have "∃S⊆F. sunflower S ∧ r ≤ card S" proof (intro exI[of _ T] conjI) { fix B assume "B ∈ S" have hB: "h B = B - {a}" unfolding h_def T_def by auto from aS ‹B ∈ S› have aB: "a ∈ B" by auto from ‹B ∈ S› ‹S ⊆ G› obtain a' A where AF: "A ∈ F" and B: "B = insert a' A" and a': "a' ∈ New" unfolding G_def by force from aB B a' New AF a(1) hB AF have "insert a (h B) = B" "h B = A" by auto hence "insert a (h B) = B" "h B ∈ F" "insert a (h B) ∈ S" using AF ‹B ∈ S› by auto } note main = this have CTS: "C ∈ T ⟹ insert a C ∈ S" for C using main unfolding T_def by force show "T ⊆ F" unfolding T_def using main by auto have "r ≤ card S" by fact also have "… = card T" unfolding T_def by (subst card_image, intro inj_on_inverseI[of _ "insert a"], insert main, auto) finally show "r ≤ card T" . show "sunflower T" unfolding sunflower_def proof (intro allI impI, elim exE conjE, goal_cases) case (1 x C C1 C2) from CTS[OF ‹C1 ∈ T›] CTS[OF ‹C2 ∈ T›] CTS[OF ‹C ∈ T›] have *: "insert a C1 ∈ S" "insert a C2 ∈ S" "insert a C ∈ S" by auto from 1 have "insert a C1 ≠ insert a C2" using main unfolding T_def by auto hence "∃A B. A ∈ S ∧ B ∈ S ∧ A ≠ B ∧ x ∈ A ∧ x ∈ B" using * 1 by auto from ‹sunflower S›[unfolded sunflower_def, rule_format, OF this *(3)] have "x ∈ insert a C" . with 1 show "x ∈ C" unfolding T_def h_def by auto qed qed with sf show False .. qed qed qed next case r: True with rk have "k ≠ 0" by auto then obtain l where k: "k = Suc l" by (cases k, auto) show ?thesis unfolding r k by (intro exI[of _ "{}"], auto) qed text ‹The difference between the lower and the upper bound on the existence of sunflowers as they have been formalized is @{term ‹fact k›}. There is more recent work with tighter bounds \<^cite>‹"sunflower_new"›, but we only integrate the initial result of Erd\H{o}s and Rado in this theory.› text ‹We further provide the Erd\H{o}s Rado lemma lifted to obtain non-empty cores or cores of arbitrary cardinality.› lemma Erdos_Rado_sunflower_card_core: assumes "finite E" and "∀ A ∈ F. A ⊆ E ∧ s ≤ card A ∧ card A ≤ k" and "card F > (card E choose s) * (r - 1)^k * fact k" and "s ≠ 0" and "r ≠ 0" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ card (⋂ S) ≥ s" by (rule sunflower_card_core_lift[OF assms(1) _ assms(2) _ assms(4-5), of "(r - 1)^k * fact k"], rule Erdos_Rado_sunflower, insert assms(3), auto simp: ac_simps) lemma Erdos_Rado_sunflower_nonempty_core: assumes "finite E" and "∀ A ∈ F. A ⊆ E ∧ card A ≤ k" and "{} ∉ F" and "card F > card E * (r - 1)^k * fact k" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ ⋂ S ≠ {}" by (rule sunflower_nonempty_core_lift[OF assms(1) _ assms(2-3), of "(r - 1)^k * fact k"], rule Erdos_Rado_sunflower, insert assms(4), auto simp: ac_simps) end