Theory Sunflowers.Erdos_Rado_Sunflower
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