§30.2.2: the point of the convex hull of separable signed examples closest to the origin separates them, ⟨w, vᵢ⟩ > 0 for all i

Proved

UnderstandingML.min_norm_separates

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

compression-schemesconvex-hullhalfspaces

§30.2.2 (p. 413). Since the data is linearly separable, the convex hull of $\{x_1, \dots, x_m\}$ (all labels positive w.l.o.g.) does not contain the origin. Consider the point $w$ in this convex hull closest to the origin. We claim that $w$ separates the data: if $\langle w, x_i\rangle \le 0$ for some $i$ , then $w' = (1-\alpha)w + \alpha x_i$ with $\alpha = \|w\|^2/(\|x_i\|^2 + \|w\|^2)$ is in the hull and has $\|w'\| < \|w\|$ , a contradiction.

Formally: for $w$ of minimal norm in the convex hull of $v_1, \dots, v_m$ with $0$ not in the hull, $\langle w, v_i\rangle > 0$ for all $i$ .

Preamble

import Definitions.Def_UnderstandingML_Compression

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **§30.2.2** (p. 413). For linearly separable data (`0` is not in the convex hull of the
signed examples `v₁, …, v_m`), the point `w` of the convex hull closest to the origin separates
the data: `⟨w, vᵢ⟩ > 0` for all `i`. -/
theorem min_norm_separates {d m : ℕ} (v : Fin m → Vec d) (w : Vec d)
    (hw : w ∈ convexHull ℝ (Set.range v)) (hmin : ∀ u ∈ convexHull ℝ (Set.range v), ‖w‖ ≤ ‖u‖)
    (h0 : (0 : Vec d) ∉ convexHull ℝ (Set.range v)) (i : Fin m) :
    0 < ⟪w, v i⟫_ℝ := 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, §30.2.2 p. 413, the claim that the minimal-norm point of the convex hull separates the data, 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