Theorem 9.2: the VC-dimension of the class of homogenous halfspaces in ℝ^d is d

Proved

UnderstandingML.vcDim_homHalfspaces

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

halfspacesvc-dimension

Theorem 9.2. The VC dimension of the class of homogenous halfspaces in $\mathbb{R}^d$ is $d$ .

Preamble

import Definitions.Def_UnderstandingML_Linear

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Theorem 9.2** (p. 122). The VC dimension of the class of homogenous halfspaces in `ℝ^d`
is `d`. -/
theorem vcDim_homHalfspaces (d : ℕ) : vcDim (homHalfspaces d) = d := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §9.1.3 p. 122, Theorem 9.2 with its proof

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph