Claim 15.1: the distance from x to the hyperplane {v : ⟨w,v⟩ + b = 0} with ‖w‖ = 1 is |⟨w,x⟩ + b|
ProvedUnderstandingML.dist_to_hyperplanegeometrymargin
Claim 15.1. The distance between a point and the hyperplane defined by where is .
Preamble
import Definitions.Def_UnderstandingML_SVM open MeasureTheory open scoped InnerProductSpace
Formal statement
namespace UnderstandingML
/-- **Claim 15.1** (p. 203). The distance between a point `x` and the hyperplane defined by
`(w, b)` where `‖w‖ = 1` is `|⟨w, x⟩ + b|`. -/
theorem dist_to_hyperplane {d : ℕ} (w : Vec d) (hw : ‖w‖ = 1) (b : ℝ) (x : Vec d) :
Metric.infDist x {v : Vec d | ⟪w, v⟫_ℝ + b = 0} = |⟪w, x⟫_ℝ + b| := 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.1 p. 203, Claim 15.1 with its proof
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.