Theorems · Theorem · functional analysis

exists_norm_eq_iInf_of_complete_convex

• 1000+ list: Hilbert projection theorem

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F},
  K.Nonempty → IsComplete K → Convex ℝ K → ∀ (u : F), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Existence of minimizers, aka the Hilbert projection theorem. Let u be a point in a real inner product space, and let K be a nonempty complete convex subset. Then there exists a (unique) v in K that minimizes the distance ‖u - v‖ to u.

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Cited by

1 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpace