VC dimension of a set family

This file defines the VC dimension of a set family as the maximum size of a set it shatters.

def Shatters {α : Type u_1} (𝒜 : Set (Set α)) (A : Set α) : Prop

A set family 𝒜 shatters a set A if restricting 𝒜 to A gives rise to all subsets of A.

Equations

• Shatters 𝒜 A = ∀ ⦃B : Set α⦄, B ⊆ A → ∃ C ∈ 𝒜, A ∩ C = B

theorem Shatters.exists_inter_eq_singleton {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} {a : α} (hs : Shatters 𝒜 A) (ha : a ∈ A) : ∃ B ∈ 𝒜, A ∩ B = {a}

theorem Shatters.mono_left {α : Type u_1} {𝒜 ℬ : Set (Set α)} {A : Set α} (h : 𝒜 ⊆ ℬ) (h𝒜 : Shatters 𝒜 A) : Shatters ℬ A

theorem Shatters.mono_right {α : Type u_1} {𝒜 : Set (Set α)} {A B : Set α} (h : B ⊆ A) (hs : Shatters 𝒜 A) : Shatters 𝒜 B

theorem Shatters.exists_superset {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} (h : Shatters 𝒜 A) : ∃ B ∈ 𝒜, A ⊆ B

theorem Shatters.of_forall_subset {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} (h : ∀ B ⊆ A, B ∈ 𝒜) : Shatters 𝒜 A

theorem Shatters.nonempty {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} (h : Shatters 𝒜 A) : 𝒜.Nonempty

@[simp]

theorem shatters_empty {α : Type u_1} {𝒜 : Set (Set α)} : Shatters 𝒜 ∅ ↔ 𝒜.Nonempty

theorem Shatters.subset_iff {α : Type u_1} {𝒜 : Set (Set α)} {A B : Set α} (h : Shatters 𝒜 A) : B ⊆ A ↔ ∃ u ∈ 𝒜, A ∩ u = B

theorem shatters_iff {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} : Shatters 𝒜 A ↔ (fun (x : Set α) => A ∩ x) '' 𝒜 = 𝒫 A

theorem univ_shatters {α : Type u_1} {A : Set α} : Shatters Set.univ A

@[simp]

theorem shatters_univ {α : Type u_1} {𝒜 : Set (Set α)} : Shatters 𝒜 Set.univ ↔ 𝒜 = Set.univ

def HasVCDimAtMost {α : Type u_1} (𝒜 : Set (Set α)) (d : ℕ) : Prop

A set family 𝒜 has VC dimension at most d if there are no families x of elements indexed by [d + 1] and A of sets of 𝒜 indexed by 2^[d + 1] such that x i ∈ A s ↔ i ∈ s for all i ∈ [d + 1], s ⊆ [d + 1].

Equations

• HasVCDimAtMost 𝒜 d = ∀ (x : Fin (d + 1) → α) (A : Set (Fin (d + 1)) → Set α), (∀ (s : Set (Fin (d + 1))), A s ∈ 𝒜) → ¬∀ (i : Fin (d + 1)) (s : Set (Fin (d + 1))), x i ∈ A s ↔ i ∈ s

theorem HasVCDimAtMost.anti {α : Type u_1} {𝒜 ℬ : Set (Set α)} {d : ℕ} (h𝒜ℬ : 𝒜 ≤ ℬ) (hℬ : HasVCDimAtMost ℬ d) : HasVCDimAtMost 𝒜 d

theorem HasVCDimAtMost.mono {α : Type u_1} {𝒜 : Set (Set α)} {d d' : ℕ} (h : d ≤ d') (hd : HasVCDimAtMost 𝒜 d) : HasVCDimAtMost 𝒜 d'

@[simp]

theorem HasVCDimAtMost.empty {α : Type u_1} {d : ℕ} : HasVCDimAtMost ∅ d