Claim 15.6: for y ∈ {±1}, w ↦ max{0, 1 − y⟨w,x⟩} is ‖x‖-Lipschitz
ProvedUnderstandingML.hinge_lipschitzhinge-losslipschitz
Claim 15.6. Let . Then is -Lipschitz.
Preamble
import Definitions.Def_UnderstandingML_SVM open MeasureTheory open scoped InnerProductSpace
Formal statement
namespace UnderstandingML
/-- **Claim 15.6** (p. 208). Let `f(w) = max{0, 1 − y⟨w, x⟩}` with `y ∈ {±1}`. Then `f` is
`‖x‖`-Lipschitz. -/
theorem hinge_lipschitz {d : ℕ} (x : Vec d) (y : ℝ) (hy : y = 1 ∨ y = -1) :
∀ w₁ w₂ : Vec d, |hingeLoss w₁ (x, y) - hingeLoss w₂ (x, y)| ≤ ‖x‖ * ‖w₁ - w₂‖ := 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, §15.2.1 p. 208, Claim 15.6
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.