Nearest Projection

noncomputable def HumanVerification.CauchyCrofton.nearestPoint (K : Body) (x : Point2) : Point2

A nearest point of x in the compact convex body K.

Equations

• HumanVerification.CauchyCrofton.nearestPoint K x = Classical.choose ⋯

theorem HumanVerification.CauchyCrofton.nearestPoint_spec (K : Body) (x : Point2) : nearestPoint K x ∈ K.carrier ∧ ‖x - nearestPoint K x‖ = ⨅ (y : ↑K.carrier), ‖x - ↑y‖

theorem HumanVerification.CauchyCrofton.nearestPoint_mem (K : Body) (x : Point2) : nearestPoint K x ∈ K.carrier

theorem HumanVerification.CauchyCrofton.nearestPoint_inner_le_zero (K : Body) (x : Point2) {y : Point2} (hy : y ∈ K.carrier) : inner ℝ (x - nearestPoint K x) (y - nearestPoint K x) ≤ 0

Variational characterization of the nearest point.

@[simp]

theorem HumanVerification.CauchyCrofton.nearestPoint_eq_self (K : Body) {x : Point2} (hx : x ∈ K.carrier) : nearestPoint K x = x

Nearest-point projection fixes every point of the body.

theorem HumanVerification.CauchyCrofton.dist_nearestPoint_le (K : Body) (x y : Point2) : dist (nearestPoint K x) (nearestPoint K y) ≤ dist x y

The metric projection onto a closed convex set is nonexpansive.

theorem HumanVerification.CauchyCrofton.lipschitz_nearestPoint (K : Body) : LipschitzWith 1 (nearestPoint K)

The nearest-point projection is globally one-Lipschitz.