VC dimension of a set in a group

This file defines the VC dimension of a set in a group as the VC dimension of its set of translates. We prove that sets of small VC dimension are closed under lattice operations.

def HasMulVCDimLE {G : Type u_1} [Group G] (d : ℕ) (A : Set G) : Prop

A set A in a group G has VC dimension at most d if all the sets that {t • A | t : G} shatters have size at most d.

Equations

• HasMulVCDimLE d A = HasVCDimLE d {x : Set G | ∃ (t : G), t • A = x}

def HasAddVCDimLE {G : Type u_1} [AddGroup G] (d : ℕ) (A : Set G) : Prop

A set A in a group G has VC dimension at most d if all the sets that {t +ᵥ A | t : G} shatters have size at most d.

Equations

• HasAddVCDimLE d A = HasVCDimLE d {x : Set G | ∃ (t : G), t +ᵥ A = x}

theorem HasMulVCDimLE.mono {G : Type u_1} [Group G] {A : Set G} {d₁ d₂ : ℕ} (hd : d₁ ≤ d₂) (hA : HasMulVCDimLE d₁ A) : HasMulVCDimLE d₂ A

theorem HasAddVCDimLE.mono {G : Type u_1} [AddGroup G] {A : Set G} {d₁ d₂ : ℕ} (hd : d₁ ≤ d₂) (hA : HasAddVCDimLE d₁ A) : HasAddVCDimLE d₂ A

theorem HasMulVCDimLE.inter {G : Type u_1} [Group G] {A B : Set G} {d₁ d₂ : ℕ} (hA : HasMulVCDimLE d₁ A) (hB : HasMulVCDimLE d₂ B) : HasMulVCDimLE (10 * (d₁ + d₂)) (A ∩ B)

theorem HasAddVCDimLE.inter {G : Type u_1} [AddGroup G] {A B : Set G} {d₁ d₂ : ℕ} (hA : HasAddVCDimLE d₁ A) (hB : HasAddVCDimLE d₂ B) : HasAddVCDimLE (10 * (d₁ + d₂)) (A ∩ B)