Shattering families #

This file defines the shattering property and VC-dimension of set families.

Main declarations #

• Finset.Shatters: The shattering property.
• Finset.shatterer: The set family of sets shattered by a set family.
• Finset.vcDim: The Vapnik-Chervonenkis dimension.

TODO #

• Order-shattering
• Strong shattering
def Finset.Shatters {α : Type u_1} [] (𝒜 : Finset (Finset α)) (s : ) :

A set family 𝒜 shatters a set s if all subsets of s can be obtained as the intersection of s and some element of the set family, and we denote this 𝒜.Shatters s. We also say that s is traced by 𝒜.

Equations
• 𝒜.Shatters s = ∀ ⦃t : ⦄, t su𝒜, s u = t
Instances For
instance Finset.instDecidablePredShatters {α : Type u_1} [] {𝒜 : Finset (Finset α)} :
DecidablePred 𝒜.Shatters
Equations
• = Finset.decidableForallOfDecidableSubsets
theorem Finset.Shatters.exists_inter_eq_singleton {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } {a : α} (hs : 𝒜.Shatters s) (ha : a s) :
t𝒜, s t = {a}
theorem Finset.Shatters.mono_left {α : Type u_1} [] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : } (h : 𝒜 ) (h𝒜 : 𝒜.Shatters s) :
.Shatters s
theorem Finset.Shatters.mono_right {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } {t : } (h : t s) (hs : 𝒜.Shatters s) :
𝒜.Shatters t
theorem Finset.Shatters.exists_superset {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } (h : 𝒜.Shatters s) :
t𝒜, s t
theorem Finset.shatters_of_forall_subset {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } (h : ts, t 𝒜) :
𝒜.Shatters s
theorem Finset.Shatters.nonempty {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } (h : 𝒜.Shatters s) :
𝒜.Nonempty
@[simp]
theorem Finset.shatters_empty {α : Type u_1} [] {𝒜 : Finset (Finset α)} :
𝒜.Shatters 𝒜.Nonempty
theorem Finset.Shatters.subset_iff {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } {t : } (h : 𝒜.Shatters s) :
t s u𝒜, s u = t
theorem Finset.shatters_iff {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } :
𝒜.Shatters s Finset.image (fun (t : ) => s t) 𝒜 = s.powerset
theorem Finset.univ_shatters {α : Type u_1} [] {s : } [] :
Finset.univ.Shatters s
@[simp]
theorem Finset.shatters_univ {α : Type u_1} [] {𝒜 : Finset (Finset α)} [] :
𝒜.Shatters Finset.univ 𝒜 = Finset.univ
def Finset.shatterer {α : Type u_1} [] (𝒜 : Finset (Finset α)) :

The set family of sets that are shattered by 𝒜.

Equations
• 𝒜.shatterer = Finset.filter 𝒜.Shatters (𝒜.biUnion Finset.powerset)
Instances For
@[simp]
theorem Finset.mem_shatterer {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } :
s 𝒜.shatterer 𝒜.Shatters s
theorem Finset.shatterer_mono {α : Type u_1} [] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} (h : 𝒜 ) :
𝒜.shatterer .shatterer
theorem Finset.subset_shatterer {α : Type u_1} [] {𝒜 : Finset (Finset α)} (h : ) :
𝒜 𝒜.shatterer
@[simp]
theorem Finset.isLowerSet_shatterer {α : Type u_1} [] (𝒜 : Finset (Finset α)) :
IsLowerSet 𝒜.shatterer
@[simp]
theorem Finset.shatterer_eq {α : Type u_1} [] {𝒜 : Finset (Finset α)} :
𝒜.shatterer = 𝒜
@[simp]
theorem Finset.shatterer_idem {α : Type u_1} [] {𝒜 : Finset (Finset α)} :
𝒜.shatterer.shatterer = 𝒜.shatterer
@[simp]
theorem Finset.shatters_shatterer {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } :
𝒜.shatterer.Shatters s 𝒜.Shatters s
theorem Finset.Shatters.shatterer {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } :
𝒜.Shatters s𝒜.shatterer.Shatters s

Alias of the reverse direction of Finset.shatters_shatterer.

theorem Finset.card_le_card_shatterer {α : Type u_1} [] (𝒜 : Finset (Finset α)) :
𝒜.card 𝒜.shatterer.card

Pajor's variant of the Sauer-Shelah lemma.

theorem Finset.Shatters.of_compression {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } {a : α} (hs : (Down.compression a 𝒜).Shatters s) :
𝒜.Shatters s
theorem Finset.shatterer_compress_subset_shatterer {α : Type u_1} [] (a : α) (𝒜 : Finset (Finset α)) :
(Down.compression a 𝒜).shatterer 𝒜.shatterer

Vapnik-Chervonenkis dimension #

def Finset.vcDim {α : Type u_1} [] (𝒜 : Finset (Finset α)) :

The Vapnik-Chervonenkis dimension of a set family is the maximal size of a set it shatters.

Equations
• 𝒜.vcDim = 𝒜.shatterer.sup Finset.card
Instances For
theorem Finset.Shatters.card_le_vcDim {α : Type u_1} [] {𝒜 : Finset (Finset α)} {s : } (hs : 𝒜.Shatters s) :
s.card 𝒜.vcDim
theorem Finset.vcDim_compress_le {α : Type u_1} [] (a : α) (𝒜 : Finset (Finset α)) :
(Down.compression a 𝒜).vcDim 𝒜.vcDim

Down-compressing decreases the VC-dimension.

theorem Finset.card_shatterer_le_sum_vcDim {α : Type u_1} [] {𝒜 : Finset (Finset α)} [] :
𝒜.shatterer.card kFinset.Iic 𝒜.vcDim, (Fintype.card α).choose k

The Sauer-Shelah lemma.