VC dimension

This file defines the VC dimension of set families.

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

A set family 𝒜 shatters a set A if all subsets of A can be obtained as the intersection of A with some element of the set family. We also say that A is traced by 𝒜.

Equations

• Shatters 𝒜 A = ∀ ⦃B : α⦄, B ≤ A → ∃ C ∈ 𝒜, A ⊓ C = B

theorem Shatters.mono {α : Type u_1} [SemilatticeInf α] {𝒜 ℬ : Set α} {A : α} (h : 𝒜 ⊆ ℬ) (h𝒜 : Shatters 𝒜 A) : Shatters ℬ A

theorem Shatters.anti {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} {A B : α} (h : A ≤ B) (hB : Shatters 𝒜 B) : Shatters 𝒜 A

theorem Shatters.exists_ge {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} {A : α} (h : Shatters 𝒜 A) : ∃ B ∈ 𝒜, A ≤ B

theorem Shatters.of_forall_le {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} {A : α} (h : ∀ B ≤ A, B ∈ 𝒜) : Shatters 𝒜 A

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

theorem Shatters.le_iff {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} {A B : α} (h : Shatters 𝒜 A) : B ≤ A ↔ ∃ C ∈ 𝒜, A ⊓ C = B

theorem shatters_iff_image_inf_eq_Iic {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} {A : α} : Shatters 𝒜 A ↔ (fun (x : α) => A ⊓ x) '' 𝒜 = Set.Iic A

theorem Shatters.univ {α : Type u_1} [SemilatticeInf α] {A : α} : Shatters Set.univ A

@[simp]

theorem shatters_bot {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} [OrderBot α] : Shatters 𝒜 ⊥ ↔ 𝒜.Nonempty

@[simp]

theorem shatters_top {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} [OrderTop α] : Shatters 𝒜 ⊤ ↔ 𝒜 = Set.univ

theorem Shatters.preimage_compl {α : Type u_1} [BooleanAlgebra α] {𝒜 : Set α} {A : α} (hA : Shatters 𝒜 A) : Shatters ((fun (x : α) => xᶜ) ⁻¹' 𝒜) A

@[simp]

theorem shatters_preimage_compl {α : Type u_1} [BooleanAlgebra α] {𝒜 : Set α} {A : α} : Shatters ((fun (x : α) => xᶜ) ⁻¹' 𝒜) A ↔ Shatters 𝒜 A

@[simp]

theorem shatters_image_compl {α : Type u_1} [BooleanAlgebra α] {𝒜 : Set α} {A : α} : Shatters ((fun (x : α) => xᶜ) '' 𝒜) A ↔ Shatters 𝒜 A

theorem Shatters.image_compl {α : Type u_1} [BooleanAlgebra α] {𝒜 : Set α} {A : α} : Shatters 𝒜 A → Shatters ((fun (x : α) => xᶜ) '' 𝒜) A

Alias of the reverse direction of shatters_image_compl.

@[instance_reducible]

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

Equations

• instDecidablePredFinsetShattersCoe _s = Finset.decidableForallOfDecidableSubsets

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

theorem shatters_iff_le_ncard_image_inter {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α} : Shatters 𝒜 A ↔ 2 ^ A.ncard ≤ ((fun (x : Set α) => A ∩ x) '' 𝒜).ncard

noncomputable def vcGrowth {α : Type u_1} (n : ℕ) (𝒜 : Set (Set α)) : ℕ

The growth of a set family is the maximum number of sets it cuts out from any set of size at most n.

Equations

• vcGrowth n 𝒜 = ⨆ (A : { A : Set α // A.Finite ∧ A.ncard ≤ n }), ((fun (x : Set α) => ↑A ∩ x) '' 𝒜).ncard

theorem vcGrowth_le_iff {α : Type u_1} {n : ℕ} {𝒜 : Set (Set α)} {d : ℕ} : vcGrowth n 𝒜 ≤ d ↔ ∀ ⦃A : Set α⦄, A.Finite → A.ncard ≤ n → ((fun (x : Set α) => A ∩ x) '' 𝒜).ncard ≤ d

theorem vcGrowth_lt_iff {α : Type u_1} {n : ℕ} {𝒜 : Set (Set α)} {d : ℕ} : vcGrowth n 𝒜 < d ↔ ∀ ⦃A : Set α⦄, A.Finite → A.ncard ≤ n → ((fun (x : Set α) => A ∩ x) '' 𝒜).ncard < d

theorem ncard_image_inter_le_vcGrowth {α : Type u_1} {n : ℕ} {𝒜 : Set (Set α)} {A : Set α} (hA : A.Finite) (hAn : A.ncard ≤ n) : ((fun (x : Set α) => A ∩ x) '' 𝒜).ncard ≤ vcGrowth n 𝒜

theorem vcGrowth_mono {α : Type u_1} {m n : ℕ} {𝒜 ℬ : Set (Set α)} (h𝒜ℬ : 𝒜 ⊆ ℬ) (hmn : m ≤ n) : vcGrowth m 𝒜 ≤ vcGrowth n ℬ

theorem vcGrowth_union_le {α : Type u_1} {n : ℕ} {𝒜 ℬ : Set (Set α)} : vcGrowth n (𝒜 ∪ ℬ) ≤ vcGrowth n 𝒜 + vcGrowth n ℬ

theorem vcGrowth_image2_inter_le {α : Type u_1} {n : ℕ} {𝒜 ℬ : Set (Set α)} : vcGrowth n (Set.image2 (fun (x1 x2 : Set α) => x1 ∩ x2) 𝒜 ℬ) ≤ vcGrowth n 𝒜 * vcGrowth n ℬ

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

A set family 𝒜 has VC dimension at most d if all the sets it shatters have size at most d.

Equations

• HasVCDimLE d 𝒜 = ∀ ⦃A : Set α⦄, A.Finite → Shatters 𝒜 A → A.ncard ≤ d

theorem HasVCDimLE.anti {α : Type u_1} {d : ℕ} {𝒜 ℬ : Set (Set α)} (hℬ𝒜 : ℬ ⊆ 𝒜) (hd : HasVCDimLE d 𝒜) : HasVCDimLE d ℬ

theorem HasVCDimLE.mono {α : Type u_1} {d₁ d₂ : ℕ} {𝒜 : Set (Set α)} (hd : d₁ ≤ d₂) : HasVCDimLE d₁ 𝒜 → HasVCDimLE d₂ 𝒜

theorem vcGrowth_le_iff' {α : Type u_1} {n : ℕ} {𝒜 : Set (Set α)} [Infinite α] {d : ℕ} : vcGrowth n 𝒜 ≤ d ↔ ∀ ⦃A : Set α⦄, A.Finite → A.ncard = n → ((fun (x : Set α) => A ∩ x) '' 𝒜).ncard ≤ d

theorem vcGrowth_lt_iff' {α : Type u_1} {n : ℕ} {𝒜 : Set (Set α)} [Infinite α] {d : ℕ} : vcGrowth n 𝒜 < d ↔ ∀ ⦃A : Set α⦄, A.Finite → A.ncard = n → ((fun (x : Set α) => A ∩ x) '' 𝒜).ncard < d

theorem hasVCDimLE_iff_vcGrowth {α : Type u_1} {d : ℕ} {𝒜 : Set (Set α)} [Infinite α] : HasVCDimLE d 𝒜 ↔ vcGrowth (d + 1) 𝒜 < 2 ^ (d + 1)