Theorem 9.3: the VC-dimension of the class of nonhomogenous halfspaces in ℝ^d is d + 1

Proved

UnderstandingML.vcDim_halfspaces

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

halfspacesvc-dimension

Theorem 9.3. The VC dimension of the class of nonhomogenous halfspaces in $\mathbb{R}^d$ is $d + 1$ .

Preamble

import Definitions.Def_UnderstandingML_Linear

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Theorem 9.3** (p. 122). The VC dimension of the class of nonhomogenous halfspaces in `ℝ^d`
is `d + 1`. -/
theorem vcDim_halfspaces (d : ℕ) : vcDim (halfspaces d) = d + 1 := 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.3 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