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.

What's known in the literature

theorem hasAddVCDimAtMost_three_of_convex_r2 {C : Set (EuclideanSpace ℝ (Fin 2))} (hC : Convex ℝ C) : HasAddVCDimAtMost C 3

Every convex set in $\mathbb R^2$ has VC dimension at most 3.

theorem exists_infinite_convex_r3_shatters : ∃ (A : Set (EuclideanSpace ℝ (Fin 3))) (C : Set (EuclideanSpace ℝ (Fin 3))), A.Infinite ∧ Convex ℝ C ∧ Shatters {x : Set (EuclideanSpace ℝ (Fin 3)) | ∃ (t : EuclideanSpace ℝ (Fin 3)), t +ᵥ C = x} A

There exists a set in $\mathbb R^3$ shattering an infinite set.

What's not in the literature

theorem exists_convex_rn_add_two_vc_n_forall_not_hasAddVCNDimAtMost (n : ℕ) : ∃ (C : Set (Fin (n + 2) → ℝ)), Convex ℝ C ∧ ∀ (d : ℕ), ¬HasAddVCNDimAtMost C n d

There exists a set of infinite $\mathrm{VC}_n$ dimension in $\mathbb R^{n + 2}$.

Conjectures

theorem hasAddVCNDimAtMost_two_one_of_convex_r3 {C : Set (EuclideanSpace ℝ (Fin 3))} (hC : Convex ℝ C) : HasAddVCNDimAtMost C 2 1

Every convex set in $\mathbb R^3$ has $\mathrm{VC}_2$ dimension at most 1.

theorem exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one (n : ℕ) : ∃ (d : ℕ), ∀ (C : Set (Fin (n + 1) → ℝ)), Convex ℝ C → HasAddVCNDimAtMost C n d

For every $n$ there exists some $d$ such that every convex set in $\mathbb R^{n + 1}$ has $\mathrm{VC}_n$ dimension at most $d$.

theorem hasAddVCNDimAtMost_n_one_of_convex_rn_add_one {n : ℕ} (hn : 2 ≤ n) {C : Set (Fin (n + 1) → ℝ)} (hC : Convex ℝ C) : HasAddVCNDimAtMost C n 1

If $n \ge 2$, every convex set in $\mathbb R^{n + 1}$ has $\mathrm{VC}_n$ dimension at most 1.