feat: state results and conjectures on VCₘ dim of convex sets in ℝⁿ #553
Conversation
…n ℝⁿ VC dimension of a set family is an old notion in learning theory. VC dimension of a *set* in a group (defined as the VC dimension of its family of translates) is a more recent notion motivated by additive combinatorics. VCₙ dimension of a set family is a very recent notion that appeared in the context of model theory. Therefore very few questions have been asked and answered at the intersection of both, i.e. about the VCₙ dimension of a family of translates 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.
| @[category research solved, AMS 5 52] | ||
| lemma vc_lt_four_of_convex_r2 {C : Set (Fin 2 → ℝ)} (hC : Convex ℝ C) | ||
| {x : Fin 4 → Fin 2 → ℝ} {y : Set (Fin 4) → Fin 2 → ℝ} | ||
| (hxy : ∀ i s, x i + y s ∈ C ↔ i ∈ s) : False := sorry |
There was a problem hiding this comment.
nit: the convention we follow is by sorry rather than sorry.
| 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 |
There was a problem hiding this comment.
Which of the formal statements below corresponds to "every convex set in ℝⁿ has finite VCₙ dimension"?
There was a problem hiding this comment.
Whoops, that got lost in translation
| @[category research solved, AMS 5 52] | ||
| lemma vc_lt_four_of_convex_r2 {C : Set (Fin 2 → ℝ)} (hC : Convex ℝ C) | ||
| {x : Fin 4 → Fin 2 → ℝ} {y : Set (Fin 4) → Fin 2 → ℝ} | ||
| (hxy : ∀ i s, x i + y s ∈ C ↔ i ∈ s) : False := sorry |
There was a problem hiding this comment.
How annoying would it be to add a local definition of the VC dimension and use it in these formalisations? This wouldn't have to be at Mathlib level generality (but could definitely be added to ForMathlib and eventually upstreamed;))
There was a problem hiding this comment.
It's definitely possible, but it would make the statement less concrete for no theoretical benefit (the first thing you do when dealing with VC dimension is unfolding the definition, quite often). What do you think?
There was a problem hiding this comment.
I see! In my eyes, the main benefit of using the general definition is maintainability e.g. if we later decide we need to make some changes related to that definition, we would only need to modify one def rather than all the theorems (which might end up introducing error/inconsistencies). A good middle ground could involve:
- Stating a general definition
- Adding a tiny bit of API (which you can leave sorried out if it's not in the
ForMathlibdirectory) to help unfolding the definition.
What do you think?
| import FormalConjectures.Util.ProblemImports | ||
| import Mathlib.Analysis.Convex.Basic | ||
| import Mathlib.Data.Real.Basic |
There was a problem hiding this comment.
this should suffice
| import FormalConjectures.Util.ProblemImports | |
| import Mathlib.Analysis.Convex.Basic | |
| import Mathlib.Data.Real.Basic | |
| import FormalConjectures.Util.ProblemImports |
Paul-Lez
added
the
Awaiting author
3 participants
VC dimension of a set family is an old notion in learning theory. VC dimension of a set in a group (defined as the VC dimension of its family of translates) is a more recent notion motivated by additive combinatorics. VCₙ dimension of a set family is a very recent notion that appeared in the context of model theory. Therefore very few questions have been asked and answered at the intersection of both, i.e. about the VCₙ dimension of a family of translates
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.