Theory Sauer_Shelah_Lemma
section "Sauer-Shelah Lemma"
theory Sauer_Shelah_Lemma
imports Shattering Card_Lemmas Binomial_Lemmas
begin
subsection ‹Generalized Sauer-Shelah Lemma›
text ‹To prove the Sauer-Shelah Lemma, we will first prove a slightly stronger fact that every family
@{term "F"} shatters at least as many sets as @{term "card F"}. We first fix an element @{term "x ∈ (⋃ F)"}
and consider the subfamily @{term F0} of sets in the family not containing it. By induction, @{term F0}
shatters at least as many elements of @{term F} as @{term "card F0"}.
Next, we consider the subfamily @{term F1} of sets in the family that contain @{term x}.
Again, by induction, @{term F1} shatters as many elements of @{term F} as its cardinality.
The number of elements of @{term F} shattered by @{term F0} and @{term F1} sum up to at least
@{term "card F0 + card F1 = card F"}. When a set @{term "S ∈ F"} is shattered by only one of the two subfamilies, say @{term F0},
it contributes one unit to the set @{term "shattered_by F0"} and to @{term "shattered_by F"}. However, when the set is shattered by
both subfamilies, both @{term S} and @{term "S ∪ {x}"} are in @{term "shattered_by F"}, so @{term S} contributes two units
to @{term "shattered_by F0 ∪ shattered_by F1"}. Therefore, the cardinality of @{term "shattered_by F"}
is at least equal to the cardinality of @{term "shattered_by F0 ∪ shattered_by F1"}, which is at least @{term "card F"}.›
lemma sauer_shelah_0:
fixes F :: "'a set set"
shows "finite (⋃ F) ⟹ card F ≤ card (shattered_by F)"
proof (induction F rule: measure_induct_rule[of "card"])
case (less F)
note finite_F = finite_UnionD[OF less(2)]
note finite_shF = finite_shattered_by[OF less(2)]
show ?case
proof (cases "2 ≤ card F")
case True
from obtain_difference_element[OF True]
obtain x :: 'a where x_in_Union_F: "x ∈ ⋃F"
and x_not_in_Int_F: "x ∉ ⋂F" by blast
text ‹Define F0 as the subfamily of F containing sets that don't contain @{term x}.›
let ?F0 = "{S ∈ F. x ∉ S}"
from x_in_Union_F have F0_psubset_F: "?F0 ⊂ F" by blast
from F0_psubset_F have F0_in_F: "?F0 ⊆ F" by blast
from subset_shattered_by[OF F0_in_F] have shF0_subset_shF: "shattered_by ?F0 ⊆ shattered_by F" .
from F0_in_F have Un_F0_in_Un_F:"⋃ ?F0 ⊆ ⋃ F" by blast
text ‹F0 shatters at least as many sets as @{term "card F0"} by the induction hypothesis.›
note IH_F0 = less(1)[OF psubset_card_mono[OF finite_F F0_psubset_F] rev_finite_subset[OF less(2) Un_F0_in_Un_F]]
text ‹Define F1 as the subfamily of F containing sets that contain @{term x}.›
let ?F1 = "{S ∈ F. x ∈ S}"
from x_not_in_Int_F have F1_psubset_F: "?F1 ⊂ F" by blast
from F1_psubset_F have F1_in_F: "?F1 ⊆ F" by blast
from subset_shattered_by[OF F1_in_F] have shF1_subset_shF: "shattered_by ?F1 ⊆ shattered_by F" .
from F1_in_F have Un_F1_in_Un_F:"⋃ ?F1 ⊆ ⋃ F" by blast
text ‹F1 shatters at least as many sets as @{term "card F1"} by the induction hypothesis.›
note IH_F1 = less(1)[OF psubset_card_mono[OF finite_F F1_psubset_F] rev_finite_subset[OF less(2) Un_F1_in_Un_F]]
from shF0_subset_shF shF1_subset_shF
have shattered_subset: "(shattered_by ?F0) ∪ (shattered_by ?F1) ⊆ shattered_by F" by simp
text ‹There is a set with the same cardinality as the intersection of
@{term "shattered_by F0"} and @{term "shattered_by F1"} which is disjoint from their union and is also contained in @{term "shattered_by F"}.›
have f_copies_the_intersection:
"∃f. inj_on f (shattered_by ?F0 ∩ shattered_by ?F1) ∧
(shattered_by ?F0 ∪ shattered_by ?F1) ∩ (f ` (shattered_by ?F0 ∩ shattered_by ?F1)) = {} ∧
f ` (shattered_by ?F0 ∩ shattered_by ?F1) ⊆ shattered_by F"
proof
have x_not_in_shattered: "∀S∈(shattered_by ?F0) ∪ (shattered_by ?F1). x ∉ S" unfolding shattered_by_def by blast
text ‹This set is precisely the image of the intersection under @{term "insert x"}.›
let ?f = "insert x"
have 0: "inj_on ?f (shattered_by ?F0 ∩ shattered_by ?F1)"
proof
fix X Y
assume x0: "X ∈ (shattered_by ?F0 ∩ shattered_by ?F1)" and y0: "Y ∈ (shattered_by ?F0 ∩ shattered_by ?F1)"
and 0: "?f X = ?f Y"
from x_not_in_shattered x0 have "X = ?f X - {x}" by blast
also from 0 have "... = ?f Y - {x}" by argo
also from x_not_in_shattered y0 have "... = Y" by blast
finally show "X = Y" .
qed
text ‹The set is disjoint from the union.›
have 1: "(shattered_by ?F0 ∪ shattered_by ?F1) ∩ ?f ` (shattered_by ?F0 ∩ shattered_by ?F1) = {}"
proof (rule ccontr)
assume "(shattered_by ?F0 ∪ shattered_by ?F1) ∩ ?f ` (shattered_by ?F0 ∩ shattered_by ?F1) ≠ {}"
then obtain S where 10: "S ∈ (shattered_by ?F0 ∪ shattered_by ?F1)"
and 11: "S ∈ ?f ` (shattered_by ?F0 ∩ shattered_by ?F1)" by auto
from 10 x_not_in_shattered have "x ∉ S" by blast
with 11 show "False" by blast
qed
text ‹This set is also in @{term "shattered_by F"}.›
have 2: "?f ` (shattered_by ?F0 ∩ shattered_by ?F1) ⊆ shattered_by F"
proof
fix S_x
assume "S_x ∈ ?f ` (shattered_by ?F0 ∩ shattered_by ?F1)"
then obtain S where 20: "S ∈ shattered_by ?F0"
and 21: "S ∈ shattered_by ?F1"
and 22: "S_x = ?f S" by blast
from x_not_in_shattered 20 have x_not_in_S: "x ∉ S" by blast
from 22 Pow_insert[of x S] have "Pow S_x = Pow S ∪ ?f ` Pow S" by fast
also from 20 have "... = (?F0 ∩* S) ∪ (?f ` Pow S)" unfolding shattered_by_def by blast
also from 21 have "... = (?F0 ∩* S) ∪ (?f ` (?F1 ∩* S))" unfolding shattered_by_def by force
also from insert_IntF[of x S ?F1] have "... = (?F0 ∩* S) ∪ (?f ` ?F1 ∩* (?f S))" by argo
also from 22 have "... = (?F0 ∩* S) ∪ (?F1 ∩* S_x)" by blast
also from 22 have "... = (?F0 ∩* S_x) ∪ (?F1 ∩* S_x)" by blast
also from subset_IntF[OF F0_in_F, of S_x] subset_IntF[OF F1_in_F, of S_x] have "... ⊆ (F ∩* S_x)" by blast
finally have "Pow S_x ⊆ (F ∩* S_x)" .
thus "S_x ∈ shattered_by F" unfolding shattered_by_def by blast
qed
from 0 1 2 show "inj_on ?f (shattered_by ?F0 ∩ shattered_by ?F1) ∧
(shattered_by ?F0 ∪ shattered_by ?F1) ∩ (?f ` (shattered_by ?F0 ∩ shattered_by ?F1)) = {} ∧
?f ` (shattered_by ?F0 ∩ shattered_by ?F1) ⊆ shattered_by F" by blast
qed
have F0_union_F1_is_F: "?F0 ∪ ?F1 = F" by fastforce
from finite_F have finite_F0: "finite ?F0" and finite_F1: "finite ?F1" by fastforce+
have disjoint_F0_F1: "?F0 ∩ ?F1 = {}" by fastforce
text ‹We have the following lower bound on the cardinality of @{term "shattered_by F"}:›
from F0_union_F1_is_F card_Un_disjoint[OF finite_F0 finite_F1 disjoint_F0_F1]
have "card F = card ?F0 + card ?F1" by argo
also from IH_F0
have "... ≤ card (shattered_by ?F0) + card ?F1" by linarith
also from IH_F1
have "... ≤ card (shattered_by ?F0) + card (shattered_by ?F1)" by linarith
also from card_Int_copy[OF finite_shF shattered_subset f_copies_the_intersection]
have "... ≤ card (shattered_by F)" by argo
finally show ?thesis .
next
text ‹If @{term F} contains less than 2 sets, the statement follows trivially.›
case False
hence "card F = 0 ∨ card F = 1" by force
thus ?thesis
proof
assume "card F = 0"
thus ?thesis by auto
next
assume asm: "card F = 1"
hence F_not_empty: "F ≠ {}" by fastforce
from shatters_empty[OF F_not_empty] have "{{}} ⊆ shattered_by F" unfolding shattered_by_def by fastforce
from card_mono[OF finite_shF this] asm show ?thesis by fastforce
qed
qed
qed
subsection ‹Sauer-Shelah Lemma›
text ‹The generalized version immediately implies the Sauer-Shelah Lemma,
because only @{text "(∑i≤k. n choose i)"} of the subsets of an @{term n}-item universe have cardinality less than @{term "k + (1::nat)"}.
Thus, when @{text "(∑i≤k. n choose i) < card F"}, there are not enough sets to be shattered,
so one of the shattered sets must have cardinality at least @{term "k + (1::nat)"}.›
corollary sauer_shelah:
fixes F :: "'a set set"
assumes "finite (⋃F)" and "(∑i≤k. card (⋃F) choose i) < card F"
shows "∃S. (F shatters S ∧ card S = k + 1)"
proof -
let ?K = "{S. S ⊆ ⋃F ∧ card S ≤ k}"
from finite_Pow_iff[of F] assms(1) have finite_Pow_Un: "finite (Pow (⋃F))" by fast
from sauer_shelah_0[OF assms(1)] assms(2) have "(∑i≤k. card (⋃F) choose i) < card (shattered_by F)" by linarith
with choose_row_sum_set[OF assms(1), of k] have "card ?K < card (shattered_by F)" by presburger
from finite_diff_not_empty[OF finite_subset[OF _ finite_Pow_Un] this]
obtain S where "S ∈ shattered_by F - ?K" by blast
then have F_shatters_S: "F shatters S" and "S ⊆ ⋃F" and "¬(S ⊆ ⋃F ∧ card S ≤ k)" unfolding shattered_by_def by blast+
then have card_S_ge_Suc_k: "k + 1 ≤ card S" by simp
from obtain_subset_with_card_n[OF card_S_ge_Suc_k] obtain S' where "card S' = k + 1" and "S' ⊆ S" by blast
from this(1) supset_shatters[OF this(2) F_shatters_S] show ?thesis by blast
qed
subsection ‹Sauer-Shelah Lemma for hypergraphs›
text ‹If we designate X to be the set of hyperedges and S the set of vertices, we can also formulate the Sauer-Shelah Lemma in terms of hypergraphs.
In this form, the statement provides a sufficient condition for the existence of an hyperedge of a given cardinality which is shattered by the set of edges.›
corollary sauer_shelah_2:
fixes X :: "'a set set" and S :: "'a set"
assumes "finite S" and "X ⊆ Pow S" and "(∑i≤k. card S choose i) < card X"
shows "∃Y. (X shatters Y ∧ card Y = k + 1)"
proof -
from assms(2) have 0: "⋃X ⊆ S" by blast
then have "(∑i≤k. card (⋃X) choose i) ≤ (∑i≤k. card S choose i)"
by (simp add: assms(1) card_mono choose_mono sum_mono)
then show ?thesis
using "0" assms finite_subset sauer_shelah by fastforce
qed
subsection ‹Alternative statement of the Sauer-Shelah Lemma›
text ‹We can also state the Sauer-Shelah Lemma in terms of the @{term VC_dim}. If the VC-dimension of @{term F} is @{term k} then @{term F}
can consist at most of @{text "(∑i≤k. card (⋃F) choose i)"} sets which is in @{text "𝒪(card (⋃F)^k)"}.›
corollary sauer_shelah_alt:
assumes "finite (⋃F)" and "VC_dim F = k"
shows "card F ≤ (∑i≤k. card (⋃F) choose i)"
proof (rule ccontr)
assume "¬ card F ≤ (∑i≤k. card (⋃F) choose i)" hence "(∑i≤k. card (⋃F) choose i) < card F" by linarith
then obtain S where "F shatters S" and "card S = k + 1"
by (meson assms(1) sauer_shelah)
then have §: "k + 1 ∈ {card S | S. F shatters S}"
by simp metis
have "finite {A. F shatters A}"
by (metis ‹finite (⋃ F)› finite_shattered_by shattered_by_def)
then have "bdd_above {card A |A. F shatters A}"
by simp
then have "k + 1 ≤ Sup {card A |A. F shatters A}"
by (smt (verit, best) "§" cSup_upper)
then have "k + 1 ≤ VC_dim F"
by (simp add: VC_dim_def)
then show False
using assms(2) by auto
qed
end