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
.
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
.
Characterization of minimizers for the projection on a convex set in a real inner product space.
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
.
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.
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
)