The orthogonal projection #
Given a nonempty complete subspace K
of an inner product space E
, this file constructs
orthogonal_projection K : E โL[๐] K
, the orthogonal projection of E
onto K
. This map
satisfies: for any point u
in E
, the point v = orthogonal_projection K u
in K
minimizes the
distance โu - vโ
to u
.
Also a linear isometry equivalence reflection K : E โโแตข[๐] E
is constructed, by choosing, for
each u : E
, the point reflection K u
to satisfy
u + (reflection K u) = 2 โข orthogonal_projection K u
.
Basic API for orthogonal_projection
and reflection
is developed.
Next, the orthogonal projection is used to prove a series of more subtle lemmas about the
the orthogonal complement of complete subspaces of E
(the orthogonal complement itself was
defined in analysis.inner_product_space.basic
); the lemma
submodule.sup_orthogonal_of_is_complete
, stating that for a complete subspace K
of E
we have
K โ Kแฎ = โค
, is a typical example.
References #
The orthogonal projection construction is adapted from
- [Clรฉment & Martin, The Lax-Milgram Theorem. A detailed proof to be formalized in Coq]
- [Clรฉment & Martin, A Coq formal proof of the LaxโMilgram theorem]
The Coq code is available at the following address: http://www.lri.fr/~sboldo/elfic/index.html
Orthogonal projection in inner product spaces #
Existence of minimizers
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 superceded by norm_eq_infi_iff_inner_eq_zero
that gives the same conclusion over
any is_R_or_C
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
)
The orthogonal projection onto a complete subspace, as an
unbundled function. This definition is only intended for use in
setting up the bundled version orthogonal_projection
and should not
be used once that is defined.
Equations
- orthogonal_projection_fn K v = _.some
The unbundled orthogonal projection is in the given subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.
The characterization of the unbundled orthogonal projection. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.
The unbundled orthogonal projection is the unique point in K
with the orthogonality property. This lemma is only intended for use
in setting up the bundled version and should not be used once that is
defined.
The orthogonal projection onto a complete subspace.
Equations
- orthogonal_projection K = {to_fun := ฮป (v : E), โจorthogonal_projection_fn K v, _โฉ, map_add' := _, map_smul' := _}.mk_continuous 1 _
The characterization of the orthogonal projection.
The difference of v
from its orthogonal projection onto K
is in Kแฎ
.
The orthogonal projection is the unique point in K
with the
orthogonality property.
The orthogonal projection of y
on U
minimizes the distance โy - xโ
for x โ U
.
The orthogonal projections onto equal subspaces are coerced back to the same point in E
.
The orthogonal projection sends elements of K
to themselves.
A point equals its orthogonal projection if and only if it lies in the subspace.
Orthogonal projection onto the submodule.map
of a subspace.
The orthogonal projection onto the trivial submodule is the zero map.
The orthogonal projection has norm โค 1
.
Formula for orthogonal projection onto a single vector.
Formula for orthogonal projection onto a single unit vector.
Auxiliary definition for reflection
: the reflection as a linear equivalence.
Equations
Reflection in a complete subspace of an inner product space. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in a subspace, is a more general sense of the word that includes both those common cases.
Equations
- reflection K = {to_linear_equiv := {to_fun := (reflection_linear_equiv K).to_fun, map_add' := _, map_smul' := _, inv_fun := (reflection_linear_equiv K).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
The result of reflecting.
Reflection is its own inverse.
Reflection is its own inverse.
Reflecting twice in the same subspace.
Reflection is involutive.
Reflection is involutive.
Reflection is involutive.
A point is its own reflection if and only if it is in the subspace.
Reflection in the submodule.map
of a subspace.
Reflection in the submodule.map
of a subspace.
Reflection through the trivial subspace {0} is just negation.
If Kโ
is complete and contained in Kโ
, Kโ
and Kโแฎ โ Kโ
span Kโ
.
If K
is complete, K
and Kแฎ
span the whole space.
If K
is complete, any v
in E
can be expressed as a sum of elements of K
and Kแฎ
.
If K
is complete, then the orthogonal complement of its orthogonal complement is itself.
If K
is complete, K
and Kแฎ
are complements of each other.
A point in K
with the orthogonality property (here characterized in terms of Kแฎ
) must be the
orthogonal projection.
A point in K
with the orthogonality property (here characterized in terms of Kแฎ
) must be the
orthogonal projection.
The orthogonal projection onto K
of an element of Kแฎ
is zero.
The reflection in K
of an element of Kแฎ
is its negation.
The orthogonal projection onto Kแฎ
of an element of K
is zero.
If U โค V
, then projecting on V
and then on U
is the same as projecting on U
.
Given a monotone family U
of complete submodules of E
and a fixed x : E
,
the orthogonal projection of x
on U i
tends to the orthogonal projection of x
on
(โจ i, U i).topological_closure
along at_top
.
Given a monotone family U
of complete submodules of E
with dense span supremum,
and a fixed x : E
, the orthogonal projection of x
on U i
tends to x
along at_top
.
The orthogonal complement satisfies Kแฎแฎแฎ = Kแฎ
.
The closure of K
is the full space iff Kแฎ
is trivial.
If S
is dense and x - y โ Kแฎ
, then x = y
.
The reflection in Kแฎ
of an element of K
is its negation.
The orthogonal projection onto (๐ โ v)แฎ
of v
is zero.
The reflection in (๐ โ v)แฎ
of v
is -v
.
In a complete space E
, a vector splits as the sum of its orthogonal projections onto a
complete submodule K
and onto the orthogonal complement of K
.
The Pythagorean theorem, for an orthogonal projection.
In a complete space E
, the projection maps onto a complete subspace K
and its orthogonal
complement sum to the identity.
The orthogonal projection is self-adjoint.
The orthogonal projection is symmetric.
Given a finite-dimensional subspace Kโ
, and a subspace Kโ
containined in it, the dimensions of Kโ
and the intersection of its
orthogonal subspace with Kโ
add to that of Kโ
.
Given a finite-dimensional subspace Kโ
, and a subspace Kโ
containined in it, the dimensions of Kโ
and the intersection of its
orthogonal subspace with Kโ
add to that of Kโ
.
Given a finite-dimensional space E
and subspace K
, the dimensions of K
and Kแฎ
add to
that of E
.
Given a finite-dimensional space E
and subspace K
, the dimensions of K
and Kแฎ
add to
that of E
.
In a finite-dimensional inner product space, the dimension of the orthogonal complement of the span of a nonzero vector is one less than the dimension of the space.
An element ฯ
of the orthogonal group of F
can be factored as a product of reflections, and
specifically at most as many reflections as the dimension of the complement of the fixed subspace
of ฯ
.
The orthogonal group of F
is generated by reflections; specifically each element ฯ
of the
orthogonal group is a product of at most as many reflections as the dimension of F
.
Special case of the CartanโDieudonnรฉ theorem.
The orthogonal group of F
is generated by reflections.
An orthogonal family of subspaces of E
satisfies direct_sum.is_internal
(that is,
they provide an internal direct sum decomposition of E
) if and only if their span has trivial
orthogonal complement.
An orthogonal family of subspaces of E
satisfies direct_sum.is_internal
(that is,
they provide an internal direct sum decomposition of E
) if and only if their span has trivial
orthogonal complement.
An orthonormal set in an inner_product_space
is maximal, if and only if the orthogonal
complement of its span is empty.
An orthonormal set in a finite-dimensional inner_product_space
is maximal, if and only if it
is a basis.