English
Equivalences between the norm-based minimization and inner-product zero condition: (u − v) is orthogonal to every w ∈ K iff the norms match the infimum.
Русский
Эквивалентности между минимизацией по норме и условием нуля скалярного произведения: если u−v ортогонален любому w∈K тогда нормовые минимумы совпадают и наоборот.
LaTeX
$$$\\forall w \\in K, \\langle u-v, w \\rangle = 0$ ↔ $\\|u-v\\| = \\inf_{w\\in K}\\|u-w\\|$$$
Lean4
/-- Existence of projections on complete subspaces.
Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`.
This point `v` is usually called the orthogonal projection of `u` onto `K`.
-/
theorem exists_norm_eq_iInf_of_complete_subspace (h : IsComplete (↑K : Set E)) :
∀ u : E, ∃ v ∈ K, ‖u - v‖ = ⨅ w : (K : Set E), ‖u - w‖ :=
by
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
let K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
exact exists_norm_eq_iInf_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex
