Documentation

Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Existence of minimizers (Hilbert projection theorem) #

This file shows the existence of minimizers (also known as the Hilbert projection theorem). This is the key tool that is used to define Submodule.orthogonalProjection in Mathlib/Analysis/InnerProductSpace/Projection/Basic.

theorem exists_norm_eq_iInf_of_complete_convex {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace F] {K : Set F} (ne : K.Nonempty) (h₁ : IsComplete K) (h₂ : Convex K) (u : F) :
vK, u - v = ⨅ (w : K), 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.

theorem norm_eq_iInf_iff_real_inner_le_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace F] {K : Set F} (h : Convex K) {u v : F} (hv : v K) :
u - v = ⨅ (w : K), u - w wK, inner (u - v) (w - v) 0

Characterization of minimizers for the projection on a convex set in a real inner product space.

theorem Submodule.exists_norm_eq_iInf_of_complete_subspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) (h : IsComplete K) (u : E) :
vK, u - v = ⨅ (w : K), u - w

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 Submodule.norm_eq_iInf_iff_real_inner_eq_zero {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace F] (K : Submodule F) {u v : F} (hv : v K) :
u - v = ⨅ (w : K), u - w wK, inner (u - v) w = 0

Characterization of minimizers in the projection on a subspace, in the real case. Let u be a point in a real inner product space, and let K be a nonempty subspace. Then point v minimizes the distance ‖u - v‖ over points in K if and only if for all w ∈ K, ⟪u - v, w⟫ = 0 (i.e., u - v is orthogonal to the subspace K). This is superseded by norm_eq_iInf_iff_inner_eq_zero that gives the same conclusion over any RCLike field.

theorem Submodule.norm_eq_iInf_iff_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) {u v : E} (hv : v K) :
u - v = ⨅ (w : K), u - w wK, inner 𝕜 (u - v) w = 0

Characterization of minimizers in the projection on a subspace. Let u be a point in an inner product space, and let K be a nonempty subspace. Then point v minimizes the distance ‖u - v‖ over points in K if and only if for all w ∈ K, ⟪u - v, w⟫ = 0 (i.e., u - v is orthogonal to the subspace K)