Lemma 14.9 (projection lemma): for the projection v of w onto a convex H and every u ∈ H, ‖w − u‖² − ‖v − u‖² ≥ 0
ProvedUnderstandingML.projection_lemmaconvexityprojection
Lemma 14.9 (Projection Lemma). Let be a closed convex set and let be the projection of onto , . Then for every , .
Formally: for a convex and a point minimizing over (closedness only guarantees existence).
Preamble
import Definitions.Def_UnderstandingML_SGD open MeasureTheory open scoped InnerProductSpace
Formal statement
namespace UnderstandingML
/-- **Lemma 14.9 (Projection Lemma)** (p. 193). Let `H` be a closed convex set and let `v` be the
projection of `w` onto `H`, `v = argmin_{x ∈ H} ‖x − w‖²`. Then for every `u ∈ H`,
`‖w − u‖² − ‖v − u‖² ≥ 0`. (Closedness is only needed for the projection to exist.) -/
theorem projection_lemma {d : ℕ} (H : Set (Vec d)) (hH : Convex ℝ H) (w v : Vec d)
(hv : IsProjection H w v) (u : Vec d) (hu : u ∈ H) :
0 ≤ ‖w - u‖ ^ 2 - ‖v - u‖ ^ 2 := 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, §14.4.1 pp. 193-194, Lemma 14.9 with its proof
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.