From 181190038e560da89dd3cb0d621656d44267ed77 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 23 Dec 2025 15:44:23 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20state=20results=20and=20conjectures=20o?= =?UTF-8?q?n=20VC=E2=82=98=20dim=20of=20convex=20sets=20in=20=E2=84=9D?= =?UTF-8?q?=E2=81=BF=20VC=20dimension=20of=20a=20set=20family=20is=20an=20?= =?UTF-8?q?old=20notion=20in=20learning=20theory.=20VC=20dimension=20of=20?= =?UTF-8?q?a=20*set*=20in=20a=20group=20(defined=20as=20the=20VC=20dimensi?= =?UTF-8?q?on=20of=20its=20family=20of=20translates)=20is=20a=20more=20rec?= =?UTF-8?q?ent=20notion=20motivated=20by=20additive=20combinatorics.=20VC?= =?UTF-8?q?=E2=82=99=20dimension=20of=20a=20set=20family=20is=20a=20very?= =?UTF-8?q?=20recent=20notion=20that=20appeared=20in=20the=20context=20of?= =?UTF-8?q?=20model=20theory.=20Therefore=20very=20few=20questions=20have?= =?UTF-8?q?=20been=20asked=20and=20answered=20at=20the=20intersection=20of?= =?UTF-8?q?=20both,=20i.e.=20about=20the=20VC=E2=82=99=20dimension=20of=20?= =?UTF-8?q?a=20family=20of=20translates?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR offers some conjectures in this direction. The conjectures are all mine and do not appear in the literature. They are very easily stated due to the elementary nature of VCₙ dimension. --- .../Combinatorics/Additive/VCDim.lean | 106 ++++++++++++++++++ .../Combinatorics/SetFamily/VCDim.lean | 82 ++++++++++++++ FormalConjectures/Other/VCDimConvex.lean | 67 +++++++++++ FormalConjectures/Util/ForMathlib.lean | 2 + 4 files changed, 257 insertions(+) create mode 100644 FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean create mode 100644 FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean create mode 100644 FormalConjectures/Other/VCDimConvex.lean diff --git a/FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean b/FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean new file mode 100644 index 000000000..ef01e12d4 --- /dev/null +++ b/FormalConjectures/ForMathlib/Combinatorics/Additive/VCDim.lean @@ -0,0 +1,106 @@ +/- +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. +-/ +import FormalConjectures.ForMathlib.Combinatorics.SetFamily.VCDim +import Mathlib + +open scoped Pointwise + +variable {G : Type*} [CommGroup G] {A B : Set G} {n d d' : ℕ} + +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 `[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 `[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 HasMulVCDimAtMost : Prop := + ∀ (x : Fin (d + 1) → G) (y : Set (Fin (d + 1)) → G), ¬ ∀ i s, y s * x i ∈ A ↔ i ∈ s + +@[to_additive] +lemma HasMulVCDimAtMost.mono (h : d ≤ d') (hd : HasMulVCDimAtMost A d) : + HasMulVCDimAtMost A d' := by + rintro x y hxy + replace h : d + 1 ≤ d' + 1 := by omega + exact hd (x ∘ Fin.castLE h) (y ∘ Set.image (Fin.castLE h)) fun i s ↦ (hxy ..).trans <| by simp + +@[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 <| by simp; tauto + +@[to_additive] +protected alias ⟨HasMulVCDimAtMost.of_compl, HasMulVCDimAtMost.compl⟩ := hasMulVCDimAtMost_compl + +@[to_additive (attr := simp)] +protected lemma HasMulVCDimAtMost.empty : HasMulVCDimAtMost (∅ : Set G) d := by + simpa [HasMulVCDimAtMost] using ⟨default, .univ, by simp⟩ + +@[to_additive (attr := simp)] +protected lemma HasMulVCDimAtMost.univ : HasMulVCDimAtMost (.univ : Set G) d := by + simpa [HasMulVCDimAtMost] using ⟨default, ∅, by simp⟩ + +@[to_additive (attr := simp)] +lemma hasVCDimAtMost_smul : HasVCDimAtMost {t • A | t : G} d ↔ HasMulVCDimAtMost A d := by + 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 <| by simp + +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 ∈ s + +@[to_additive] +lemma HasMulVCNDimAtMost.mono (h : d ≤ d') (hd : HasMulVCNDimAtMost A n d) : + HasMulVCNDimAtMost A n d' := by + rintro x y hxy + replace h : d + 1 ≤ d' + 1 := by omega + exact hd (x · ∘ Fin.castLE h) (y ∘ Set.image (Fin.castLE h ∘ ·)) fun i s ↦ + (hxy ..).trans <| by simp [funext_iff]; simp [← funext_iff] + +@[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 <| by simp; tauto + +@[to_additive] +protected alias ⟨HasMulVCNDimAtMost.of_compl, HasMulVCNDimAtMost.compl⟩ := hasMulVCNDimAtMost_compl + +@[to_additive (attr := simp)] +protected lemma HasMulVCNDimAtMost.empty : HasMulVCNDimAtMost (∅ : Set G) n d := by + simpa [HasMulVCNDimAtMost] using ⟨default, .univ, by simp⟩ + +@[to_additive (attr := simp)] +protected lemma HasMulVCNDimAtMost.univ : HasMulVCNDimAtMost (.univ : Set G) n d := by + simpa [HasMulVCNDimAtMost] using ⟨default, ∅, by simp⟩ + +@[to_additive (attr := simp)] +lemma hasMulVCNDimAtMost_one : HasMulVCNDimAtMost A 1 d ↔ HasMulVCDimAtMost A d := by + symm + refine (Equiv.funUnique ..).symm.forall_congr fun x ↦ + ((Equiv.Set.congr <| Equiv.funUnique ..).arrowCongr <| .refl _).symm.forall_congr fun y ↦ + not_congr <| (Equiv.funUnique ..).symm.forall_congr fun i ↦ + (Equiv.Set.congr <| Equiv.funUnique ..).symm.forall_congr fun s ↦ ?_ + simp [Set.image_image, funext_iff] diff --git a/FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean b/FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean new file mode 100644 index 000000000..911c3cbb4 --- /dev/null +++ b/FormalConjectures/ForMathlib/Combinatorics/SetFamily/VCDim.lean @@ -0,0 +1,82 @@ +/- +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. +-/ +import Mathlib.Data.Set.Card + +/-! +# 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. +-/ + +variable {α : Type*} {𝒜 ℬ : Set (Set α)} {A B : Set α} {a : α} {d d' : ℕ} + +variable (𝒜 A) in +/-- A set family `𝒜` shatters a set `A` if restricting `𝒜` to `A` gives rise to all subsets of `A`. +-/ +def Shatters : Prop := ∀ ⦃B⦄, B ⊆ A → ∃ C ∈ 𝒜, A ∩ C = B + +lemma Shatters.exists_inter_eq_singleton (hs : Shatters 𝒜 A) (ha : a ∈ A) : ∃ B ∈ 𝒜, A ∩ B = {a} := + hs <| Set.singleton_subset_iff.2 ha + +lemma Shatters.mono_left (h : 𝒜 ⊆ ℬ) (h𝒜 : Shatters 𝒜 A) : Shatters ℬ A := + fun _B hB ↦ let ⟨u, hu, hut⟩ := h𝒜 hB; ⟨u, h hu, hut⟩ + +lemma Shatters.mono_right (h : B ⊆ A) (hs : Shatters 𝒜 A) : Shatters 𝒜 B := fun u hu ↦ by + obtain ⟨v, hv, rfl⟩ := hs (hu.trans h); exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩ + +lemma Shatters.exists_superset (h : Shatters 𝒜 A) : ∃ B ∈ 𝒜, A ⊆ B := + let ⟨B, hB, hst⟩ := h .rfl; ⟨B, hB, Set.inter_eq_left.1 hst⟩ + +lemma Shatters.of_forall_subset (h : ∀ B, B ⊆ A → B ∈ 𝒜) : Shatters 𝒜 A := + fun B hB ↦ ⟨B, h _ hB, Set.inter_eq_right.2 hB⟩ + +protected lemma Shatters.nonempty (h : Shatters 𝒜 A) : 𝒜.Nonempty := + let ⟨B, hB, _⟩ := h .rfl; ⟨B, hB⟩ + +@[simp] lemma shatters_empty : Shatters 𝒜 ∅ ↔ 𝒜.Nonempty := + ⟨Shatters.nonempty, fun ⟨A, hs⟩ B hB ↦ ⟨A, hs, by simpa [eq_comm] using hB⟩⟩ + +protected lemma Shatters.subset_iff (h : Shatters 𝒜 A) : B ⊆ A ↔ ∃ u ∈ 𝒜, A ∩ u = B := + ⟨fun hB ↦ h hB, by rintro ⟨u, _, rfl⟩; exact Set.inter_subset_left⟩ + +lemma shatters_iff : Shatters 𝒜 A ↔ (A ∩ ·) '' 𝒜 = A.powerset := + ⟨fun h ↦ by ext B; simp [h.subset_iff], fun h B hB ↦ h.superset hB⟩ + +lemma univ_shatters : Shatters .univ A := .of_forall_subset <| by simp + +@[simp] lemma shatters_univ : Shatters 𝒜 .univ ↔ 𝒜 = .univ := by + simp [Shatters, Set.eq_univ_iff_forall] + +variable (𝒜 d) in +/-- 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], s ⊆ [d]`. -/ +def HasVCDimAtMost : Prop := + ∀ (x : Fin (d + 1) → α) (A : Set (Fin (d + 1)) → Set α), + (∀ s, A s ∈ 𝒜) → ¬ ∀ i s, x i ∈ A s ↔ i ∈ s + +lemma HasVCDimAtMost.anti (h𝒜ℬ : 𝒜 ≤ ℬ) (hℬ : HasVCDimAtMost ℬ d) : HasVCDimAtMost 𝒜 d := + fun _x _A hA ↦ hℬ _ _ fun _s ↦ h𝒜ℬ <| hA _ + +lemma HasVCDimAtMost.mono (h : d ≤ d') (hd : HasVCDimAtMost 𝒜 d) : HasVCDimAtMost 𝒜 d' := by + rintro x A hA hxA + replace h : d + 1 ≤ d' + 1 := by omega + exact hd (x ∘ Fin.castLE h) (A ∘ Set.image (Fin.castLE h)) (by simp [hA]) fun i s ↦ + (hxA ..).trans <| by simp + +@[simp] lemma HasVCDimAtMost.empty : HasVCDimAtMost (∅ : Set (Set α)) d := by simp [HasVCDimAtMost] + +proof_wanted hasVCDimAtMost_iff_shatters : HasVCDimAtMost 𝒜 d ↔ ∀ A, Shatters 𝒜 A → A.encard ≤ d diff --git a/FormalConjectures/Other/VCDimConvex.lean b/FormalConjectures/Other/VCDimConvex.lean new file mode 100644 index 000000000..3bf86b74f --- /dev/null +++ b/FormalConjectures/Other/VCDimConvex.lean @@ -0,0 +1,67 @@ +/- +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. +-/ +import FormalConjectures.Util.ProblemImports + +/-! +# VCₙ dimension of convex sets in ℝⁿ, ℝⁿ⁺¹, ℝⁿ⁺² + +In the literature it is known that every convex set in ℝ² has VC dimension at most 3, +and there exists a convex set in ℝ³ with infinite VC dimension (even more strongly, +which shatters an infinite set). + +This file states that every convex set in ℝⁿ has finite VCₙ dimension, constructs a convex set in +ℝⁿ⁺² with infinite VCₙ dimension (even more strongly, which n-shatters an infinite set), +and conjectures that every convex set in ℝⁿ⁺¹ has finite VCₙ dimension. +-/ + +open scoped EuclideanGeometry Pointwise + +/-! ### What's known in the literature -/ + +/-- Every convex set in ℝ² has VC dimension at most 3. -/ +@[category research solved, AMS 5 52] +lemma hasAddVCDimAtMost_three_of_convex_r2 {C : Set ℝ²} (hC : Convex ℝ C) : HasAddVCDimAtMost C 3 := + sorry + +/-- There exists a set in ℝ³ shattering an infinite set. -/ +@[category research solved, AMS 5 52] +lemma exists_infinite_convex_r3_shatters : + ∃ A C : Set ℝ³, A.Infinite ∧ Convex ℝ C ∧ Shatters {t +ᵥ C | t : ℝ³} A := sorry + +/-! ### What's not in the literature -/ + +/-- There exists a set of infinite VCₙ dimension in ℝⁿ⁺². -/ +@[category research solved, AMS 5 52] +lemma exists_convex_rn_add_two_vc_n_forall_not_hasAddVCNDimAtMost (n : ℕ) : + ∃ C : Set (Fin (n + 2) → ℝ), Convex ℝ C ∧ ∀ d, ¬ HasAddVCNDimAtMost C n d := sorry + +/-! ### Conjectures -/ + +/-- Every convex set in ℝ³ has VC₂ dimension at most 1. -/ +@[category research open, AMS 5 52] +lemma hasAddVCNDimAtMost_two_one_of_convex_r3 {C : Set ℝ³} (hC : Convex ℝ C) : + HasAddVCNDimAtMost C 2 1 := sorry + +/-- For every `n` there exists some `d` such that every convex set in ℝⁿ⁺¹ has VCₙ dimension at +most `d`. -/ +@[category research open, AMS 5 52] +lemma exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one (n : ℕ) : + ∃ d : ℕ, ∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n d := sorry + +/-- If `n ≥ 2`, every convex set in ℝⁿ⁺¹ has VCₙ dimension at most 1. -/ +@[category research open, AMS 5 52] +lemma hasAddVCNDimAtMost_n_one_of_convex_rn_add_one {n : ℕ} (hn : 2 ≤ n) {C : Set (Fin (n + 1) → ℝ)} + (hC : Convex ℝ C) : HasAddVCNDimAtMost C n 1 := sorry diff --git a/FormalConjectures/Util/ForMathlib.lean b/FormalConjectures/Util/ForMathlib.lean index b1ed7e74f..2e4e114f8 100644 --- a/FormalConjectures/Util/ForMathlib.lean +++ b/FormalConjectures/Util/ForMathlib.lean @@ -30,8 +30,10 @@ import FormalConjectures.ForMathlib.Analysis.SpecialFunctions.NthRoot import FormalConjectures.ForMathlib.Combinatorics.AP.Basic import FormalConjectures.ForMathlib.Combinatorics.Additive.Basis import FormalConjectures.ForMathlib.Combinatorics.Additive.Convolution +import FormalConjectures.ForMathlib.Combinatorics.Additive.VCDim import FormalConjectures.ForMathlib.Combinatorics.Basic import FormalConjectures.ForMathlib.Combinatorics.Ramsey +import FormalConjectures.ForMathlib.Combinatorics.SetFamily.VCDim import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Balanced import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Coloring import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.DiamExtra