The orthogonal projection #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 projection into U from an orthogonal submodule V is the zero map.
The projection into U from V is the zero map if and only if U and V are orthogonal.
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.
If x lies within an orthogonal family v, it can be expressed as a sum of projections.
If a family of submodules is orthogonal, then the orthogonal_projection on a direct sum
is just the coefficient of that direct sum.
If a family of submodules is orthogonal and they span the whole space, then the orthogonal projection provides a means to decompose the space into its submodules.
The projection function is decompose V x i = orthogonal_projection (V i) x.
See note [reducible non-instances].
Equations
- hV.decomposition h = {decompose' := λ (x : E), ⇑(dfinsupp.equiv_fun_on_fintype.symm) (λ (i : ι), ⇑(orthogonal_projection (V i)) x), left_inv := _, right_inv := _}
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.