§9.1.1, Equation (9.1): a sample is separable iff some w has yᵢ⟨w, xᵢ⟩ ≥ 1 for all i

Proved

UnderstandingML.separable_iff_margin_one

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

halfspaceslinear-programmingseparability

§9.1.1, Equation (9.1). In the realizable case we look for $w$ with $y_i\langle w, x_i\rangle > 0$ for all $i$ . If $w^*$ satisfies this, $\gamma = \min_i y_i\langle w^*, x_i\rangle$ and $\bar w = w^*/\gamma$ , then $y_i\langle \bar w, x_i\rangle \ge 1$ for all $i$ (9.1); and clearly such a vector is an ERM predictor.

Formally: the sample $(x_i, y_i)$ is separable if and only if there is $w$ with $y_i\langle w, x_i\rangle \ge 1$ for all $i$ .

Preamble

import Definitions.Def_UnderstandingML_Linear

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **§9.1.1, Equation (9.1)** (p. 119). In the realizable (separable) case there is a vector
with `yᵢ⟨w, xᵢ⟩ ≥ 1` for all `i` (scale a separating vector by `1/γ`, `γ = minᵢ yᵢ⟨w*, xᵢ⟩`),
and clearly such a vector separates the sample: separability is equivalent to the feasibility
of the linear constraints (9.1). -/
theorem separable_iff_margin_one {d m : ℕ} (x : Fin m → Vec d) (y : Fin m → ℝ) :
    Separable x y ↔ ∃ w : Vec d, ∀ i, 1 ≤ y i * ⟪w, x 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, §9.1.1 p. 119, the derivation of Equation (9.1)

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