Theorems · Theorem · functional analysis

Submodule.norm_eq_iInf_iff_real_inner_eq_zero

∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (K : Submodule ℝ F) {u v : F},
  v ∈ K → (‖u - v‖ = ⨅ w, ‖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.

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace