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} [DecidableEq α] (𝒜 : Finset (Finset α)) (s : Finset α) : Prop

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

• Finset.Shatters 𝒜 s = ∀ ⦃t : Finset α⦄, t ⊆ s → ∃ u ∈ 𝒜, s ∩ u = t

instance Finset.instDecidablePredFinsetShatters {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} : DecidablePred (Finset.Shatters 𝒜)

Equations

• Finset.instDecidablePredFinsetShatters _s = Finset.decidableForallOfDecidableSubsets

theorem Finset.Shatters.exists_inter_eq_singleton {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : Finset.Shatters 𝒜 s) (ha : a ∈ s) : ∃ t ∈ 𝒜, s ∩ t = {a}

theorem Finset.Shatters.mono_left {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} (h : 𝒜 ⊆ ℬ) (h𝒜 : Finset.Shatters 𝒜 s) : Finset.Shatters ℬ s

theorem Finset.Shatters.mono_right {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {t : Finset α} (h : t ⊆ s) (hs : Finset.Shatters 𝒜 s) : Finset.Shatters 𝒜 t

theorem Finset.Shatters.exists_superset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : Finset.Shatters 𝒜 s) : ∃ t ∈ 𝒜, s ⊆ t

theorem Finset.shatters_of_forall_subset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : ∀ t ⊆ s, t ∈ 𝒜) : Finset.Shatters 𝒜 s

theorem Finset.Shatters.nonempty {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : Finset.Shatters 𝒜 s) : 𝒜.Nonempty

@[simp]

theorem Finset.shatters_empty {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} : Finset.Shatters 𝒜 ∅ ↔ 𝒜.Nonempty

theorem Finset.Shatters.subset_iff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {t : Finset α} (h : Finset.Shatters 𝒜 s) : t ⊆ s ↔ ∃ u ∈ 𝒜, s ∩ u = t

theorem Finset.shatters_iff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} : Finset.Shatters 𝒜 s ↔ Finset.image (fun (t : Finset α) => s ∩ t) 𝒜 = Finset.powerset s

theorem Finset.univ_shatters {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] : Finset.Shatters Finset.univ s

@[simp]

theorem Finset.shatters_univ {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} [Fintype α] : Finset.Shatters 𝒜 Finset.univ ↔ 𝒜 = Finset.univ

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

The set family of sets that are shattered by 𝒜.

Equations

• Finset.shatterer 𝒜 = Finset.filter (Finset.Shatters 𝒜) (Finset.biUnion 𝒜 Finset.powerset)

@[simp]

theorem Finset.mem_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} : s ∈ Finset.shatterer 𝒜 ↔ Finset.Shatters 𝒜 s

theorem Finset.shatterer_mono {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} (h : 𝒜 ⊆ ℬ) : Finset.shatterer 𝒜 ⊆ Finset.shatterer ℬ

theorem Finset.subset_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (h : IsLowerSet ↑𝒜) : 𝒜 ⊆ Finset.shatterer 𝒜

@[simp]

theorem Finset.isLowerSet_shatterer {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) : IsLowerSet ↑(Finset.shatterer 𝒜)

@[simp]

theorem Finset.shatterer_eq {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} : Finset.shatterer 𝒜 = 𝒜 ↔ IsLowerSet ↑𝒜

@[simp]

theorem Finset.shatterer_idem {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} : Finset.shatterer (Finset.shatterer 𝒜) = Finset.shatterer 𝒜

@[simp]

theorem Finset.shatters_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} : Finset.Shatters (Finset.shatterer 𝒜) s ↔ Finset.Shatters 𝒜 s

theorem Finset.Shatters.shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} : Finset.Shatters 𝒜 s → Finset.Shatters (Finset.shatterer 𝒜) s

Alias of the reverse direction of Finset.shatters_shatterer.

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

Pajor's variant of the Sauer-Shelah lemma.

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

theorem Finset.shatterer_compress_subset_shatterer {α : Type u_1} [DecidableEq α] (a : α) (𝒜 : Finset (Finset α)) : Finset.shatterer (Down.compression a 𝒜) ⊆ Finset.shatterer 𝒜

Vapnik-Chervonenkis dimension

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

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

Equations

• Finset.vcDim 𝒜 = Finset.sup (Finset.shatterer 𝒜) Finset.card

theorem Finset.Shatters.card_le_vcDim {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (hs : Finset.Shatters 𝒜 s) : s.card ≤ Finset.vcDim 𝒜

theorem Finset.vcDim_compress_le {α : Type u_1} [DecidableEq α] (a : α) (𝒜 : Finset (Finset α)) : Finset.vcDim (Down.compression a 𝒜) ≤ Finset.vcDim 𝒜

Down-compressing decreases the VC-dimension.

theorem Finset.card_shatterer_le_sum_vcDim {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} [Fintype α] : (Finset.shatterer 𝒜).card ≤ Finset.sum (Finset.Iic (Finset.vcDim 𝒜)) fun (k : ℕ) => Nat.choose (Fintype.card α) k

The Sauer-Shelah lemma.