VC dimension of homogeneous linear halfspaces is exactly n (Cover 1965; Vapnik–Chervonenkis). The class signClass (coordSpace n) of homogeneous linear halfspaces of ℝⁿ has VC dimension equal to the ambient dimension n: the Dudley bound gives ≤ n, and the n standard basis points are shattered, giving ≥ n.
∀ (n : ℕ), VCDim (Fin n → ℝ) (signClass (FLT.Halfspace.coordSpace n)) = ↑n
- DeclFLT.Halfspace.vcDim_halfspace_eqDeclaration kindtheorem
∀ (n : ℕ), VCDim (Fin n → ℝ) (signClass (FLT.Halfspace.coordSpace n)) = ↑n
- DeclFLT.Halfspace.vcDim_halfspace_leDeclaration kindtheorem
VC dimension of homogeneous linear halfspaces: the Dudley upper bound.
The class of homogeneous linear halfspaces
x ↦ (0 < ⟨w, x⟩)inℝⁿhas VC dimension at mostn. This is the canonical instance of Dudley's bound (vcDim_signClass_le): the underlying function space iscoordSpace n, of dimensionn. (Cover 1965; Vapnik–Chervonenkis.)∀ (n : ℕ), VCDim (Fin n → ℝ) (signClass (FLT.Halfspace.coordSpace n)) ≤ ↑n
- DeclvcDim_signClass_leDeclaration kindtheorem
Dudley's bound. The VC dimension of the linear sign class of a finite-dimensional subspace
V ≤ (X → ℝ)is at mostdim V.∀ {X : Type u} (V : Submodule ℝ (X → ℝ)) [FiniteDimensional ℝ ↥V], VCDim X (signClass V) ≤ ↑(Module.finrank ℝ ↥V) - DeclFLT.Halfspace.finrank_coordSpaceDeclaration kindtheorem
The dimension of the coordinate space is
n. The coordinate functionals form the dual basis ofℝⁿ, so their span has dimensionn.∀ (n : ℕ), Module.finrank ℝ ↥(FLT.Halfspace.coordSpace n) = n
- DeclFLT.Halfspace.linearIndependent_coordDeclaration kindtheorem
The coordinate functionals are linearly independent. They are the dual basis of the standard basis; concretely, evaluating a vanishing combination at each standard basis point
Pi.single j 1isolates thej-th coefficient.∀ (n : ℕ), LinearIndependent ℝ (FLT.Halfspace.coord n)
- DeclFLT.Halfspace.coord_singleDeclaration kindtheorem
Evaluating the
i-th coordinate functional at thej-th standard basis point gives the identity matrix:coord n i (Pi.single j 1) = if i = j then 1 else 0.∀ (n : ℕ) (i j : Fin n), FLT.Halfspace.coord n i (Pi.single j 1) = if i = j then 1 else 0
- DeclFLT.Halfspace.finiteDimensional_coordSpaceDeclaration kindtheorem
The coordinate space is finite-dimensional (it is the span of a finite family).
∀ (n : ℕ), FiniteDimensional ℝ ↥(FLT.Halfspace.coordSpace n)
- DeclFLT.Halfspace.vcDim_halfspace_geDeclaration kindtheorem
VC dimension of homogeneous linear halfspaces: the lower bound. The
nstandard basis points are shattered, so the VC dimension is at leastn.∀ (n : ℕ), ↑n ≤ VCDim (Fin n → ℝ) (signClass (FLT.Halfspace.coordSpace n))
- DeclFLT.Halfspace.shatters_basisPointsDeclaration kindtheorem
The standard basis points are shattered by homogeneous halfspaces. Given any labelling, the
±1-weighted functionalg x = ∑ i, w i * x iwithw i = ±1selected by the label realises it:g (Pi.single j 1) = w j, and0 < w jiff the label istrue.∀ (n : ℕ), Shatters (Fin n → ℝ) (signClass (FLT.Halfspace.coordSpace n)) (FLT.Halfspace.basisPoints n)
Uses
- DeclFLT.Halfspace.weighted_singleDeclaration kindtheorem
A weighted functional evaluated at a standard basis point returns that point's weight:
(∑ i, w i * (Pi.single j 1) i) = w j.∀ (n : ℕ) (w : Fin n → ℝ) (j : Fin n), ∑ i, w i * Pi.single j 1 i = w j
- DeclFLT.Halfspace.weighted_mem_coordSpaceDeclaration kindtheorem
A
±1-weighted coordinate functional belongs to the coordinate space. Concretely, for any weightsw : Fin n → ℝ, the functionalx ↦ ∑ i, w i * x iis a member ofcoordSpace n.∀ (n : ℕ) (w : Fin n → ℝ), (fun x => ∑ i, w i * x i) ∈ FLT.Halfspace.coordSpace n
- DeclFLT.Halfspace.single_mem_basisPointsDeclaration kindtheorem
Each standard basis point lies in
basisPoints n.∀ (n : ℕ) (i : Fin n), Pi.single i 1 ∈ FLT.Halfspace.basisPoints n
- DeclFLT.Halfspace.card_basisPointsDeclaration kindtheorem
There are exactly
nstandard basis points.∀ (n : ℕ), (FLT.Halfspace.basisPoints n).card = n
- DeclFLT.Halfspace.single_injectiveDeclaration kindtheorem
The map
i ↦ Pi.single i 1is injective (the basis points are distinct).∀ (n : ℕ), Function.Injective fun i => Pi.single i 1
- DefinitionConceptClassdef
A concept class is a set of concepts. Used by every paradigm, complexity measure, and criterion.
Primary definition: Set of functions. Used for PAC/agnostic PAC where concept classes are sets over which VC dimension, Rademacher complexity, covering numbers, etc. are measured. Alternative definitions below for contexts requiring decidability, enumerability, or measurability.
Type u → Type v → Type (max v u)
- DefinitionFLT.Conceptdef
A concept is a function from domain to label. This is the atomic unit that concept classes collect and learners try to approximate.
Type u → Type v → Type (max u v)
- DefinitionFLT.Halfspace.basisPointsdef
The
nstandard basis points{Pi.single i 1 | i : Fin n}ofℝⁿ. These are the witnesses for the VC-dimension lower bound.(n : ℕ) → Finset (Fin n → ℝ)
- DefinitionFLT.Halfspace.coorddef
The
i-th coordinate functionalx ↦ x ionFin n → ℝ, viewed as an element of the function space(Fin n → ℝ) → ℝ.(n : ℕ) → Fin n → (Fin n → ℝ) → ℝ
- DefinitionFLT.Halfspace.coordSpacedef
The coordinate space: the span of the
ncoordinate functionals(fun x => x i)inside(Fin n → ℝ) → ℝ. This is the (dual) space of homogeneous linear functionals onℝⁿ; its sign class is exactly the family of homogeneous linear halfspaces.(n : ℕ) → Submodule ℝ ((Fin n → ℝ) → ℝ)
A set S ⊆ X is shattered by concept class C if every labeling of S is realized by some concept in C.
(X : Type u) → ConceptClass X Bool → Finset X → Prop
- DefinitionVCDimdef
VC dimension of a concept class: the size of the largest shattered set. Returns ℕ∞ = WithTop ℕ.
(X : Type u) → ConceptClass X Bool → WithTop ℕ
- DefinitionevalAtdef
Evaluation at a point
x : Xas a linear functional onV:g ↦ (g : X → ℝ) x.{X : Type u} → (V : Submodule ℝ (X → ℝ)) → X → ↥V →ₗ[ℝ] ℝ - DefinitionsignClassdef
The sign-pattern concept class of a subspace
V ≤ (X → ℝ): all concepts of the formx ↦ decide (0 < g x)for someg ∈ V.{X : Type u} → Submodule ℝ (X → ℝ) → ConceptClass X Bool
Verification
- Replay
- accepted
- Axioms
- Classical.choiceQuot.soundpropext
- Statement identity
- not-applicable
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- design-lab@5802df4 · initial
- Frozen export
- e70dfad48239
- Verified
- 2026-09-24T00:00:00Z