VCₙ dimension of convex sets in ℝⁿ, ℝⁿ⁺¹, ℝⁿ⁺²

/-
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 FormalConjecturesUtil

/-!
# 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

namespace VCDimConvex

/-  ### What's known in the literature -/

/-- Every convex set in $\mathbb R^2$ 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 $\mathbb R^3$ 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 $\mathrm{VC}_n$ dimension in $\mathbb R^{n + 2}$. -/
@[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 -/

/-- Not every convex set in $\mathbb R^3$ has
$\mathrm{VC}_2$ dimension at most 1. -/
@[category research solved, AMS 5 52,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/vcdim-convex-counterexample/blob/ad7ffff1514843c886633f5408c6456dfb2e2a49/formal-conjectures-v4.27.0/VCDimConvexCounterexample.lean"]
lemma hasAddVCNDimAtMost_two_one_of_convex_r3 :
    ¬ ∀ {C : Set ℝ³} (hC : Convex ℝ C),
      HasAddVCNDimAtMost C 2 1 := sorry

/-- Every convex set in $\mathbb R^3$ has
$\mathrm{VC}_2$ dimension at most 2. -/
@[category research open, AMS 5 52]
lemma hasAddVCNDimAtMost_two_two_of_convex_r3 {C : Set ℝ³} (hC : Convex ℝ C) :
    HasAddVCNDimAtMost C 2 2 := sorry

/-- For every $n \ge 1$ there exists some $d$ such that every convex set in $\mathbb R^{n + 1}$ has
$\mathrm{VC}_n$ dimension at most $d$. -/
@[category research open, AMS 5 52]
lemma exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one (n : ℕ) (hn : 1 ≤ n) :
    ∃ d : ℕ, ∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n d := sorry

/-- If $n \ge 2$, every convex set in $\mathbb R^{n + 1}$ has $\mathrm{VC}_n$ 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

end VCDimConvex

• Formalization source ↗

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.