theorem metricProjection_eq_along_projection_ray {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_complete : IsComplete C) (hC_convex : Convex ℝ C) (x : E) (t : ℝ) (ht : 0 ≤ t) : metricProjectionOfComplete C hC_nonempty hC_complete hC_convex (↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x) + t • (x - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x))) = metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x

Helper for Lemma 6.43: points on the ray leaving P x in the direction of x - P x keep the same metric projection onto C.

theorem infDist_prox_objective_lower_bound_by_projection_residual {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_complete : IsComplete C) (hC_convex : Convex ℝ C) (lam : ℝ) (x y : E) : lam * ‖y - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex y)‖ + 1 / 2 * ‖y - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex y) - (x - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x))‖ ^ 2 + 1 / 2 * ‖↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex y) - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)‖ ^ 2 ≤ lam * Metric.infDist y C + 1 / 2 * ‖y - x‖ ^ 2

Helper for Lemma 6.43: the distance-penalty proximal objective is bounded below by the radial residual objective centered at P x, together with the nonnegative defect term measuring the displacement of the projection point.

theorem distance_prox_candidate_eq_piecewise_target {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_complete : IsComplete C) (hC_convex : Convex ℝ C) (lam : ℝ) (x : E) : ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x) + (1 - lam / max ‖x - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)‖ lam) • (x - ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)) = if lam < Metric.infDist x C then (AffineMap.lineMap x ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)) (lam / Metric.infDist x C) else ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)

Helper for Lemma 6.43: the projection-centered shrinkage candidate is exactly the textbook piecewise point on the segment from x to P x.

theorem prox_infDist_eq_singleton_piecewise_metricProjection {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_complete : IsComplete C) (hC_convex : Convex ℝ C) (lam : ℝ) (hlam : 0 ≤ lam) (x : E) : prox[fun (y : E) => ↑(lam * Metric.infDist y C)] x = {if lam < Metric.infDist x C then (AffineMap.lineMap x ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)) (lam / Metric.infDist x C) else ↑(metricProjectionOfComplete C hC_nonempty hC_complete hC_convex x)}

Lemma 6.43: if C is a nonempty complete convex subset of a real inner product space and 0 ≤ λ, then the proximal mapping of the distance penalty y ↦ λ d_C(y) at x is the singleton given by the textbook piecewise formula, written in canonical projection-ray form: when λ < d_C(x) it is lineMap x (P_C x) (λ / d_C(x)), equivalently P_C(x) + (1 - λ / d_C(x)) (x - P_C(x)), and when d_C(x) ≤ λ it is P_C(x). Here d_C(x) is written as Metric.infDist x C, and P_C denotes the canonical metric projection onto a nonempty complete convex set. The textbook closed-subset-of-a-complete-space formulation is the downstream specialization obtained from IsClosed.isComplete. The endpoint λ = 0 is included canonically: if x ∉ C, then the first branch becomes lineMap x (P_C x) 0 = x, while if x ∈ C, then both branches reduce to x.