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.lean.

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) : ∃ v ∈ K, ‖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‖ ↔ ∀ w ∈ K, 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) : ∃ v ∈ K, ‖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‖ ↔ ∀ w ∈ K, 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‖ ↔ ∀ w ∈ K, 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)