The sample complexity of learning halfspaces in grows with , which is bad news when features are many or infinite. Chapter 15 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) introduces the support vector machine, the learning rule that replaces dimension by geometry. Among the halfspaces separating a sample, Hard-SVM picks the one of largest margin, the distance from the hyperplane to the nearest example (Claim 15.1, Lemma 15.2); if the data are separable with margin and lie in a ball of radius , the resulting classifier has error whatever the dimension (Theorem 15.4), and the Perceptron of Chapter 9 makes at most updates (Remark 15.1). Soft-SVM drops separability by allowing slack variables, and Claim 15.5 identifies it with regularized hinge-loss minimization, so that the stability theory of Chapter 13 applies: the hinge loss is -Lipschitz (Claim 15.6), and Corollary 15.7 gives an expected-risk bound depending only on the norms of the data and of the comparison halfspace. The chapter closes with the optimality conditions that explain the name: the Hard-SVM solution is a combination of the examples on the margin (Theorem 15.8, via the Fritz John conditions, Lemma 15.9).
Vectors live in as in Mission VI; labels are real numbers, with as a hypothesis wherever the book needs it. A sample is linearly separable if some halfspace has for all , and the margin of on the sample is . Hard-SVM solutions are minimizers of subject to , formalized as a relation; the minimizer is unique whenever the constraints are feasible, and the homogenous version sets . A distribution over is separable with a -margin if some unit (and ) has and almost surely. Soft-SVM is the problem under , ; its homogenous form is the regularized loss minimization rule of Mission IX for the hinge loss , and the 0–1 loss is . Expectations over samples are integrals against , with the measurability conventions of Mission IX.
For on almost surely, , and the Soft-SVM learner with : , and for every with , .
Claim 15.1. The distance from to with is .
Lemma 15.2. For a sample with both labels present, the normalized Hard-SVM output has unit norm and margin at least that of every unit-norm halfspace.
Theorem 15.4. Under homogenous -separability, with probability at least the 0–1 risk of the Hard-SVM output is at most .
Claim 15.5. Every feasible slack vector has average at least the hinge loss, and the hinge losses are feasible slacks.
Claim 15.6. For , is -Lipschitz.
Corollary 15.7, first parts. For every , and are at most .
Theorem 15.8. The homogenous Hard-SVM solution is with .
Lemma 15.9. Fritz John conditions, in the correct form with a multiplier on .
Further items: Exercise 15.1 (the two Hard-SVM formulations agree) and Exercise 15.2 (the Perceptron makes at most updates).
SVM is the bridge between the statistical theory of Part I and the kernel methods of Chapter 16: because the bounds of Theorem 15.4 and Corollary 15.7 involve only , and , the same algorithm can be run after an embedding into a huge or infinite-dimensional feature space, and Theorem 15.8, that the solution lies in the span of the examples, is what makes the embedding computable. Corollary 15.7 is also the first place where the abstract machinery of Chapter 13 is applied to a specific learning rule.
Nothing here is machine-checked. One correction is built in: the Fritz John lemma is stated with the multiplier on and nonnegative multipliers not all zero, since the printed form, with unweighted and unrestricted, fails already for and on the line. Theorem 15.8 is unaffected: its constraints are affine, so the multiplier on can be taken to be .
Claim 15.6 and Claim 15.5 are short inequalities and the intended entry points, and Exercise 15.2 is Theorem 9.1 of Mission VI with and . Claim 15.1 is the book's computation with the foot of the perpendicular and a Pythagorean inequality for every other point of the hyperplane, packaged as an infimum distance. Lemma 15.2 is the rescaling argument of the book, together with the observation that both labels force ; Exercise 15.1 needs the positivity of the optimal margin on a separable sample. Corollary 15.7 is Corollaries 13.8 and 13.9 of Mission IX for the hinge loss, whose Lipschitz constant is only on the support of , so the stability argument must be run with the almost-sure bound; the 0–1 clause is the pointwise inequality . Theorem 15.4 is the content of §26.3: Rademacher complexity of the class of norm-bounded halfspaces, the contraction lemma for the ramp loss, the observation that the Hard-SVM output has zero ramp loss on the sample and norm at most , and a concentration step, all of which will be items of the Rademacher mission. Theorem 15.8 is the KKT theorem for a strictly convex quadratic with affine constraints (Slater's condition holds), and Lemma 15.9 is the general Fritz John theorem for differentiable data, whose proof goes through a separation or penalty argument; neither is in Mathlib.
Hard-SVM and Soft-SVM are relations and learners, not programs; the margin is a real infimum over the sample; the ramp loss is defined but its bounds belong to Chapter 26. Theorem 15.4 is stated for any learner that returns the Hard-SVM solution whenever the sample is feasible, which is almost surely the case under the margin assumption, and bounds the failure event in outer measure. Corollary 15.7 carries the measurability conventions of Mission IX. The Fritz John lemma is stated correctly rather than as printed. The duality of §15.4, the SGD implementation of §15.5 (whose guarantee needs the trajectory bound of §14.5.3 rather than Theorem 14.11 as stated in Mission X), Exercises 15.3 and 15.4, and Remark 15.2 are not stated.
Trivializing readings are excluded: both labels must be present for the normalized Hard-SVM output, the margin assumption and the support condition are almost sure with respect to , and the risks are genuine integrals. Welcome contributions: the uniqueness of the Hard-SVM minimizer, the KKT conditions for affine constraints, and the pointwise comparison of the 0–1, ramp and hinge losses.
namespace UnderstandingML
/-- **Corollary 15.7** (p. 208), last part. For every `B > 0`, if Soft-SVM (15.6) is run with
`λ = √(2ρ²/(B²m))` then
`E_S[L^{0−1}_D(A(S))] ≤ E_S[L^hinge_D(A(S))] ≤ min_{w : ‖w‖ ≤ B} L^hinge_D(w) + √(8ρ²B²/m)`.
The parameter depends on `m`; "`min`" is "for every `w` with `‖w‖ ≤ B`". -/
theorem soft_svm_norm_bound {d : ℕ} (D : Measure (Vec d × ℝ)) [IsProbabilityMeasure D]
{ρ B : ℝ} (hρ : 0 < ρ) (hB : 0 < B) (hD : ∀ᵐ z ∂D, ‖z.1‖ ≤ ρ ∧ (z.2 = 1 ∨ z.2 = -1))
(A : Learner (Vec d × ℝ) (Vec d))
(hA : ∀ (m : ℕ) (S : Fin m → Vec d × ℝ),
IsRLM hingeLoss (Real.sqrt (2 * ρ ^ 2 / (B ^ 2 * m))) S (A m S))
(hAmeas : ∀ m, Measurable (A m)) (m : ℕ) (hm : 0 < m) :
∫ S, risk zeroOneLoss D (A m S) ∂(iidLaw D m) ≤
∫ S, risk hingeLoss D (A m S) ∂(iidLaw D m) ∧
∀ w : Vec d, ‖w‖ ≤ B →
∫ S, risk hingeLoss D (A m S) ∂(iidLaw D m) ≤
risk hingeLoss D w + Real.sqrt (8 * ρ ^ 2 * B ^ 2 / m) := by sorry
end UnderstandingML
Corollary 15.7 (last part). For every , if we set then
Formally: the Soft-SVM parameter depends on ; "" is "for every with ".
No open leaves. Every sub-goal is proved or awaiting decomposition.