1. FormalConjecturesForMathlib
  2. Combinatorics
  3. Additive
  4. VCDim
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim public import Mathlib.Algebra.Group.Action.Pointwise.Set.Basic@[expose] public section

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.

open scoped Pointwisevariable {G : Type*} [CommGroup G] {A B : Set G} {n d d' : ℕ}variable (A d) in

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].

@[to_additive

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].

] def HasMulVCDimAtMost : Prop := ∀ (x : Fin (d + 1) → G) (y : Set (Fin (d + 1)) → G), ¬ ∀ i s, y s * x i ∈ A ↔ i ∈ sG:Type u_1inst✝:CommGroup GA:Set Gd:ℕd':ℕhd:HasMulVCDimAtMost A dx:Fin (d' + 1) → Gy:Set (Fin (d' + 1)) → Ghxy:∀ (i : Fin (d' + 1)) (s : Set (Fin (d' + 1))), y s * x i ∈ A ↔ i ∈ sh:d + 1 ≤ d' + 1⊢ False exact hd (x ∘ Fin.castLE h) (y ∘ Set.image (Fin.castLE h)) fun i s ↦ (hxy ..).trans <| G:Type u_1inst✝:CommGroup GA:Set Gd:ℕd':ℕhd:HasMulVCDimAtMost A dx:Fin (d' + 1) → Gy:Set (Fin (d' + 1)) → Ghxy:∀ (i : Fin (d' + 1)) (s : Set (Fin (d' + 1))), y s * x i ∈ A ↔ i ∈ sh:d + 1 ≤ d' + 1i:Fin (d + 1)s:Set (Fin (d + 1))⊢ Fin.castLE h i ∈ Fin.castLE h '' s ↔ i ∈ s All goals completed! 🐙@[to_additive (attr := simp)] lemma hasMulVCDimAtMost_compl : HasMulVCDimAtMost Aᶜ d ↔ HasMulVCDimAtMost A d := forall_congr' fun x ↦ (compl_involutive.toPerm.arrowCongr <| .refl _).forall_congr fun y ↦ not_congr <| forall_congr' fun i ↦ compl_involutive.toPerm.forall_congr <| G:Type u_1inst✝:CommGroup GA:Set Gd:ℕx:Fin (d + 1) → Gy:Set (Fin (d + 1)) → Gi:Fin (d + 1)⊢ ∀ (a : Set (Fin (d + 1))), (y a * x i ∈ Aᶜ ↔ i ∈ a) ↔ ((Equiv.arrowCongr (Function.Involutive.toPerm compl ⋯) (Equiv.refl G)) y ((Function.Involutive.toPerm compl ⋯) a) * x i ∈ A ↔ i ∈ (Function.Involutive.toPerm compl ⋯) a) G:Type u_1inst✝:CommGroup GA:Set Gd:ℕx:Fin (d + 1) → Gy:Set (Fin (d + 1)) → Gi:Fin (d + 1)⊢ ∀ (a : Set (Fin (d + 1))), (y a * x i ∉ A ↔ i ∈ a) ↔ (y a * x i ∈ A ↔ i ∉ a); All goals completed! 🐙@[to_additive] protected alias ⟨HasMulVCDimAtMost.of_compl, HasMulVCDimAtMost.compl⟩ := hasMulVCDimAtMost_compl@[to_additive (attr := simp)] protected lemma HasMulVCDimAtMost.empty : HasMulVCDimAtMost (∅ : Set G) d := G:Type u_1inst✝:CommGroup Gd:ℕ⊢ HasMulVCDimAtMost ∅ d simpa [HasMulVCDimAtMost] using ⟨default, .univ, G:Type u_1inst✝:CommGroup Gd:ℕ⊢ default ∈ Set.univ All goals completed! 🐙⟩@[to_additive (attr := simp)] protected lemma HasMulVCDimAtMost.univ : HasMulVCDimAtMost (.univ : Set G) d := G:Type u_1inst✝:CommGroup Gd:ℕ⊢ HasMulVCDimAtMost Set.univ d simpa [HasMulVCDimAtMost] using ⟨default, ∅, G:Type u_1inst✝:CommGroup Gd:ℕ⊢ default ∉ ∅ All goals completed! 🐙⟩@[to_additive (attr := simp)] lemma hasVCDimAtMost_smul : HasVCDimAtMost {t • A | t : G} d ↔ HasMulVCDimAtMost A d := G:Type u_1inst✝:CommGroup GA:Set Gd:ℕ⊢ HasVCDimAtMost {x | ∃ t, t • A = x} d ↔ HasMulVCDimAtMost A d simpa [HasVCDimAtMost, HasMulVCDimAtMost, Classical.skolem (b := fun _ ↦ G), ← funext_iff, Set.mem_smul_set_iff_inv_smul_mem] using forall_congr' fun x ↦ (Equiv.inv _).forall_congr <| G:Type u_1inst✝:CommGroup GA:Set Gd:ℕx:Fin (d + 1) → G⊢ ∀ (a : Set (Fin (d + 1)) → G), (∃ x_1 x_2, ¬((a x_2)⁻¹ * x x_1 ∈ A ↔ x_1 ∈ x_2)) ↔ ∃ x_1 x_2, ¬((Equiv.inv (Set (Fin (d + 1)) → G)) a x_2 * x x_1 ∈ A ↔ x_1 ∈ x_2) All goals completed! 🐙variable (A d n) in

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]ⁿ.

@[to_additive

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]ⁿ.

] def HasMulVCNDimAtMost : Prop := ∀ (x : Fin n → Fin (d + 1) → G) (y : Set (Fin n → Fin (d + 1)) → G), ¬ ∀ i s, y s * ∏ k, x k (i k) ∈ A ↔ i ∈ sG:Type u_1inst✝:CommGroup GA:Set Gn:ℕd:ℕd':ℕhd:HasMulVCNDimAtMost A n dx:Fin n → Fin (d' + 1) → Gy:Set (Fin n → Fin (d' + 1)) → Ghxy:∀ (i : Fin n → Fin (d' + 1)) (s : Set (Fin n → Fin (d' + 1))), y s * ∏ k, x k (i k) ∈ A ↔ i ∈ sh:d + 1 ≤ d' + 1⊢ False exact hd (x · ∘ Fin.castLE h) (y ∘ Set.image (Fin.castLE h ∘ ·)) fun i s ↦ (hxy ..).trans <| G:Type u_1inst✝:CommGroup GA:Set Gn:ℕd:ℕd':ℕhd:HasMulVCNDimAtMost A n dx:Fin n → Fin (d' + 1) → Gy:Set (Fin n → Fin (d' + 1)) → Ghxy:∀ (i : Fin n → Fin (d' + 1)) (s : Set (Fin n → Fin (d' + 1))), y s * ∏ k, x k (i k) ∈ A ↔ i ∈ sh:d + 1 ≤ d' + 1i:Fin n → Fin (d + 1)s:Set (Fin n → Fin (d + 1))⊢ (fun k ↦ Fin.castLE h (i k)) ∈ (fun x ↦ Fin.castLE h ∘ x) '' s ↔ i ∈ s G:Type u_1inst✝:CommGroup GA:Set Gn:ℕd:ℕd':ℕhd:HasMulVCNDimAtMost A n dx:Fin n → Fin (d' + 1) → Gy:Set (Fin n → Fin (d' + 1)) → Ghxy:∀ (i : Fin n → Fin (d' + 1)) (s : Set (Fin n → Fin (d' + 1))), y s * ∏ k, x k (i k) ∈ A ↔ i ∈ sh:d + 1 ≤ d' + 1i:Fin n → Fin (d + 1)s:Set (Fin n → Fin (d + 1))⊢ (∃ x ∈ s, ∀ (x_1 : Fin n), x x_1 = i x_1) ↔ i ∈ s; All goals completed! 🐙@[to_additive (attr := simp)] lemma hasMulVCNDimAtMost_compl : HasMulVCNDimAtMost Aᶜ n d ↔ HasMulVCNDimAtMost A n d := forall_congr' fun x ↦ (compl_involutive.toPerm.arrowCongr <| .refl _).forall_congr fun y ↦ not_congr <| forall_congr' fun i ↦ compl_involutive.toPerm.forall_congr <| G:Type u_1inst✝:CommGroup GA:Set Gn:ℕd:ℕx:Fin n → Fin (d + 1) → Gy:Set (Fin n → Fin (d + 1)) → Gi:Fin n → Fin (d + 1)⊢ ∀ (a : Set (Fin n → Fin (d + 1))), (y a * ∏ k, x k (i k) ∈ Aᶜ ↔ i ∈ a) ↔ ((Equiv.arrowCongr (Function.Involutive.toPerm compl ⋯) (Equiv.refl G)) y ((Function.Involutive.toPerm compl ⋯) a) * ∏ k, x k (i k) ∈ A ↔ i ∈ (Function.Involutive.toPerm compl ⋯) a) G:Type u_1inst✝:CommGroup GA:Set Gn:ℕd:ℕx:Fin n → Fin (d + 1) → Gy:Set (Fin n → Fin (d + 1)) → Gi:Fin n → Fin (d + 1)⊢ ∀ (a : Set (Fin n → Fin (d + 1))), (y a * ∏ k, x k (i k) ∉ A ↔ i ∈ a) ↔ (y a * ∏ k, x k (i k) ∈ A ↔ i ∉ a); All goals completed! 🐙@[to_additive] protected alias ⟨HasMulVCNDimAtMost.of_compl, HasMulVCNDimAtMost.compl⟩ := hasMulVCNDimAtMost_compl@[to_additive (attr := simp)] protected lemma HasMulVCNDimAtMost.empty : HasMulVCNDimAtMost (∅ : Set G) n d := G:Type u_1inst✝:CommGroup Gn:ℕd:ℕ⊢ HasMulVCNDimAtMost ∅ n d simpa [HasMulVCNDimAtMost] using ⟨default, .univ, G:Type u_1inst✝:CommGroup Gn:ℕd:ℕ⊢ default ∈ Set.univ All goals completed! 🐙⟩@[to_additive (attr := simp)] protected lemma HasMulVCNDimAtMost.univ : HasMulVCNDimAtMost (.univ : Set G) n d := G:Type u_1inst✝:CommGroup Gn:ℕd:ℕ⊢ HasMulVCNDimAtMost Set.univ n d simpa [HasMulVCNDimAtMost] using ⟨default, ∅, G:Type u_1inst✝:CommGroup Gn:ℕd:ℕ⊢ default ∉ ∅ All goals completed! 🐙⟩@[to_additive (attr := simp)] lemma hasMulVCNDimAtMost_one : HasMulVCNDimAtMost A 1 d ↔ HasMulVCDimAtMost A d := G:Type u_1inst✝:CommGroup GA:Set Gd:ℕ⊢ HasMulVCNDimAtMost A 1 d ↔ HasMulVCDimAtMost A d G:Type u_1inst✝:CommGroup GA:Set Gd:ℕ⊢ HasMulVCDimAtMost A d ↔ HasMulVCNDimAtMost A 1 d G:Type u_1inst✝:CommGroup GA:Set Gd:ℕx:Fin (d + 1) → Gy:Set (Fin (d + 1)) → Gi:Fin (d + 1)s:Set (Fin (d + 1))⊢ (y s * x i ∈ A ↔ i ∈ s) ↔ (((Equiv.Set.congr (Equiv.funUnique (Fin 1) (Fin (d + 1)))).arrowCongr (Equiv.refl G)).symm y ((Equiv.Set.congr (Equiv.funUnique (Fin 1) (Fin (d + 1)))).symm s) * ∏ k, (Equiv.funUnique (Fin 1) (Fin (d + 1) → G)).symm x k ((Equiv.funUnique (Fin 1) (Fin (d + 1))).symm i k) ∈ A ↔ (Equiv.funUnique (Fin 1) (Fin (d + 1))).symm i ∈ (Equiv.Set.congr (Equiv.funUnique (Fin 1) (Fin (d + 1)))).symm s) All goals completed! 🐙