VC dimension in a group

This file defines the Vapnik–Chervonenkis (aka VC) dimension of a set in a group, defined as the VC dimension of its family of translates.

It also defines the VCₙ dimension, which has no set family analogue.

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

A set A in an abelian group has VC dimension at most d iff one cannot find two sequences x and y of elements indexed by [d + 1] and 2 ^ [d + 1] respectively such that y s * x i ∈ A ↔ i ∈ s for all i ∈ [d + 1], s ⊆ [d + 1].

Equations

• HasMulVCDimAtMost A d = ∀ (x : Fin (d + 1) → G) (y : Set (Fin (d + 1)) → G), ¬∀ (i : Fin (d + 1)) (s : Set (Fin (d + 1))), y s * x i ∈ A ↔ i ∈ s

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

A set A in an abelian group has VC dimension at most d iff one cannot find two sequences x and y of elements indexed by [d + 1] and 2 ^ [d + 1] respectively such that y s + x i ∈ A ↔ i ∈ s for all i ∈ [d + 1], s ⊆ [d + 1].

Equations

• HasAddVCDimAtMost A d = ∀ (x : Fin (d + 1) → G) (y : Set (Fin (d + 1)) → G), ¬∀ (i : Fin (d + 1)) (s : Set (Fin (d + 1))), y s + x i ∈ A ↔ i ∈ s

theorem HasMulVCDimAtMost.mono {G : Type u_1} [CommGroup G] {A : Set G} {d d' : ℕ} (h : d ≤ d') (hd : HasMulVCDimAtMost A d) : HasMulVCDimAtMost A d'

theorem HasAddVCDimAtMost.mono {G : Type u_1} [AddCommGroup G] {A : Set G} {d d' : ℕ} (h : d ≤ d') (hd : HasAddVCDimAtMost A d) : HasAddVCDimAtMost A d'

@[simp]

theorem hasMulVCDimAtMost_compl {G : Type u_1} [CommGroup G] {A : Set G} {d : ℕ} : HasMulVCDimAtMost Aᶜ d ↔ HasMulVCDimAtMost A d

@[simp]

theorem hasAddVCDimAtMost_compl {G : Type u_1} [AddCommGroup G] {A : Set G} {d : ℕ} : HasAddVCDimAtMost Aᶜ d ↔ HasAddVCDimAtMost A d

theorem HasMulVCDimAtMost.of_compl {G : Type u_1} [CommGroup G] {A : Set G} {d : ℕ} : HasMulVCDimAtMost Aᶜ d → HasMulVCDimAtMost A d

Alias of the forward direction of hasMulVCDimAtMost_compl.

theorem HasMulVCDimAtMost.compl {G : Type u_1} [CommGroup G] {A : Set G} {d : ℕ} : HasMulVCDimAtMost A d → HasMulVCDimAtMost Aᶜ d

Alias of the reverse direction of hasMulVCDimAtMost_compl.

theorem HasAddVCDimAtMost.of_compl {G : Type u_1} [AddCommGroup G] {A : Set G} {d : ℕ} : HasAddVCDimAtMost Aᶜ d → HasAddVCDimAtMost A d

theorem HasAddVCDimAtMost.compl {G : Type u_1} [AddCommGroup G] {A : Set G} {d : ℕ} : HasAddVCDimAtMost A d → HasAddVCDimAtMost Aᶜ d

@[simp]

theorem HasMulVCDimAtMost.empty {G : Type u_1} [CommGroup G] {d : ℕ} : HasMulVCDimAtMost ∅ d

@[simp]

theorem HasAddVCDimAtMost.empty {G : Type u_1} [AddCommGroup G] {d : ℕ} : HasAddVCDimAtMost ∅ d

@[simp]

theorem HasMulVCDimAtMost.univ {G : Type u_1} [CommGroup G] {d : ℕ} : HasMulVCDimAtMost Set.univ d

@[simp]

theorem HasAddVCDimAtMost.univ {G : Type u_1} [AddCommGroup G] {d : ℕ} : HasAddVCDimAtMost Set.univ d

@[simp]

theorem hasVCDimAtMost_smul {G : Type u_1} [CommGroup G] {A : Set G} {d : ℕ} : HasVCDimAtMost {x : Set G | ∃ (t : G), t • A = x} d ↔ HasMulVCDimAtMost A d

@[simp]

theorem hasVCDimAtMost_vadd {G : Type u_1} [AddCommGroup G] {A : Set G} {d : ℕ} : HasVCDimAtMost {x : Set G | ∃ (t : G), t +ᵥ A = x} d ↔ HasAddVCDimAtMost A d

def HasMulVCNDimAtMost {G : Type u_1} [CommGroup G] (A : Set G) (n d : ℕ) : Prop

A set A in an abelian group has VCₙ dimension at most d iff one cannot find two sequences x and y of elements indexed by [n] × [d + 1] and 2 ^ [d + 1]ⁿ respectively such that y s * ∏ k, x (k, i k) ∈ A ↔ i ∈ s for all i ∈ [d + 1]ⁿ, s ⊆ [d + 1]ⁿ.

Equations

• One or more equations did not get rendered due to their size.

def HasAddVCNDimAtMost {G : Type u_1} [AddCommGroup G] (A : Set G) (n d : ℕ) : Prop

A set A in an abelian group has VCₙ dimension at most d iff one cannot find two sequences x and y of elements indexed by [n] × [d + 1] and 2 ^ [d + 1]ⁿ respectively such that y s + ∑ k, x (k, i k) ∈ A ↔ i ∈ s for all i ∈ [d + 1]ⁿ, s ⊆ [d + 1]ⁿ.

Equations

• One or more equations did not get rendered due to their size.

theorem HasMulVCNDimAtMost.mono {G : Type u_1} [CommGroup G] {A : Set G} {n d d' : ℕ} (h : d ≤ d') (hd : HasMulVCNDimAtMost A n d) : HasMulVCNDimAtMost A n d'

theorem HasAddVCNDimAtMost.mono {G : Type u_1} [AddCommGroup G] {A : Set G} {n d d' : ℕ} (h : d ≤ d') (hd : HasAddVCNDimAtMost A n d) : HasAddVCNDimAtMost A n d'

@[simp]

theorem hasMulVCNDimAtMost_compl {G : Type u_1} [CommGroup G] {A : Set G} {n d : ℕ} : HasMulVCNDimAtMost Aᶜ n d ↔ HasMulVCNDimAtMost A n d

@[simp]

theorem hasAddVCNDimAtMost_compl {G : Type u_1} [AddCommGroup G] {A : Set G} {n d : ℕ} : HasAddVCNDimAtMost Aᶜ n d ↔ HasAddVCNDimAtMost A n d

theorem HasMulVCNDimAtMost.of_compl {G : Type u_1} [CommGroup G] {A : Set G} {n d : ℕ} : HasMulVCNDimAtMost Aᶜ n d → HasMulVCNDimAtMost A n d

Alias of the forward direction of hasMulVCNDimAtMost_compl.

theorem HasMulVCNDimAtMost.compl {G : Type u_1} [CommGroup G] {A : Set G} {n d : ℕ} : HasMulVCNDimAtMost A n d → HasMulVCNDimAtMost Aᶜ n d

Alias of the reverse direction of hasMulVCNDimAtMost_compl.

theorem HasAddVCNDimAtMost.compl {G : Type u_1} [AddCommGroup G] {A : Set G} {n d : ℕ} : HasAddVCNDimAtMost A n d → HasAddVCNDimAtMost Aᶜ n d

theorem HasAddVCNDimAtMost.of_compl {G : Type u_1} [AddCommGroup G] {A : Set G} {n d : ℕ} : HasAddVCNDimAtMost Aᶜ n d → HasAddVCNDimAtMost A n d

@[simp]

theorem HasMulVCNDimAtMost.empty {G : Type u_1} [CommGroup G] {n d : ℕ} : HasMulVCNDimAtMost ∅ n d

@[simp]

theorem HasAddVCNDimAtMost.empty {G : Type u_1} [AddCommGroup G] {n d : ℕ} : HasAddVCNDimAtMost ∅ n d

@[simp]

theorem HasMulVCNDimAtMost.univ {G : Type u_1} [CommGroup G] {n d : ℕ} : HasMulVCNDimAtMost Set.univ n d

@[simp]

theorem HasAddVCNDimAtMost.univ {G : Type u_1} [AddCommGroup G] {n d : ℕ} : HasAddVCNDimAtMost Set.univ n d

@[simp]

theorem hasMulVCNDimAtMost_one {G : Type u_1} [CommGroup G] {A : Set G} {d : ℕ} : HasMulVCNDimAtMost A 1 d ↔ HasMulVCDimAtMost A d

@[simp]

theorem hasAddVCNDimAtMost_zero {G : Type u_1} [AddCommGroup G] {A : Set G} {d : ℕ} : HasAddVCNDimAtMost A 1 d ↔ HasAddVCDimAtMost A d