mathlib documentation

analysis.inner_product_space.projection

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.

The last section covers orthonormal bases, etc. The lemma maximal_orthonormal_iff_orthogonal_complement_eq_bot states that an orthonormal set in an inner product space is maximal, if and only the orthogonal complement of its span is trivial. Various consequences are stated for finite-dimensional E, including that a maximal orthonormal set is a basis (maximal_orthonormal_iff_basis_of_finite_dimensional); these consequences require the theory on the orthogonal complement developed earlier in this file. For consequences in infinite dimension (Hilbert bases, etc.), see the file analysis.inner_product_space.l2_space.

References #

The orthogonal projection construction is adapted from

The Coq code is available at the following address: http://www.lri.fr/~sboldo/elfic/index.html

Orthogonal projection in inner product spaces #

theorem exists_norm_eq_infi_of_complete_convex {F : Type u_3} [inner_product_space โ„ F] {K : set F} (ne : K.nonempty) (hโ‚ : is_complete K) (hโ‚‚ : convex โ„ K) (u : F) :
โˆƒ (v : F) (H : v โˆˆ K), โˆฅu - vโˆฅ = โจ… (w : โ†ฅK), โˆฅu - โ†‘wโˆฅ

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.

theorem norm_eq_infi_iff_real_inner_le_zero {F : Type u_3} [inner_product_space โ„ F] {K : set F} (h : convex โ„ K) {u v : F} (hv : v โˆˆ K) :
(โˆฅu - vโˆฅ = โจ… (w : โ†ฅK), โˆฅu - โ†‘wโˆฅ) โ†” โˆ€ (w : F), w โˆˆ K โ†’ has_inner.inner (u - v) (w - v) โ‰ค 0

Characterization of minimizers for the projection on a convex set in a real inner product space.

theorem exists_norm_eq_infi_of_complete_subspace {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) (h : is_complete โ†‘K) (u : E) :
โˆƒ (v : E) (H : 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 norm_eq_infi_iff_real_inner_eq_zero {F : Type u_3} [inner_product_space โ„ F] (K : submodule โ„ F) {u v : F} (hv : v โˆˆ K) :
(โˆฅu - vโˆฅ = โจ… (w : โ†ฅโ†‘K), โˆฅu - โ†‘wโˆฅ) โ†” โˆ€ (w : F), w โˆˆ K โ†’ has_inner.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 superceded by norm_eq_infi_iff_inner_eq_zero that gives the same conclusion over any is_R_or_C field.

theorem norm_eq_infi_iff_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) {u v : E} (hv : v โˆˆ K) :
(โˆฅu - vโˆฅ = โจ… (w : โ†ฅโ†‘K), โˆฅu - โ†‘wโˆฅ) โ†” โˆ€ (w : E), w โˆˆ K โ†’ has_inner.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)

noncomputable def orthogonal_projection_fn {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] (v : E) :
E

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
theorem orthogonal_projection_fn_mem {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (v : E) :

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.

theorem orthogonal_projection_fn_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (v w : E) (H : w โˆˆ K) :

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.

theorem eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {u v : E} (hvm : v โˆˆ K) (hvo : โˆ€ (w : E), w โˆˆ K โ†’ has_inner.inner (u - v) w = 0) :

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.

noncomputable def orthogonal_projection {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :
E โ†’L[๐•œ] โ†ฅK

The orthogonal projection onto a complete subspace.

Equations
@[simp]
theorem orthogonal_projection_fn_eq {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (v : E) :
@[simp]
theorem orthogonal_projection_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (v w : E) (H : w โˆˆ K) :

The characterization of the orthogonal projection.

@[simp]
theorem sub_orthogonal_projection_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (v : E) :

The difference of v from its orthogonal projection onto K is in Kแ—ฎ.

theorem eq_orthogonal_projection_of_mem_of_inner_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {u v : E} (hvm : v โˆˆ K) (hvo : โˆ€ (w : E), w โˆˆ K โ†’ has_inner.inner (u - v) w = 0) :

The orthogonal projection is the unique point in K with the orthogonality property.

theorem eq_orthogonal_projection_of_eq_submodule {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {K' : submodule ๐•œ E} [complete_space โ†ฅK'] (h : K = K') (u : E) :

The orthogonal projections onto equal subspaces are coerced back to the same point in E.

@[simp]
theorem orthogonal_projection_mem_subspace_eq_self {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (v : โ†ฅK) :

The orthogonal projection sends elements of K to themselves.

theorem orthogonal_projection_eq_self_iff {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {v : E} :

A point equals its orthogonal projection if and only if it lies in the subspace.

theorem linear_isometry.map_orthogonal_projection {๐•œ : Type u_1} [is_R_or_C ๐•œ] {E : Type u_2} {E' : Type u_3} [inner_product_space ๐•œ E] [inner_product_space ๐•œ E'] (f : E โ†’โ‚—แตข[๐•œ] E') (p : submodule ๐•œ E) [complete_space โ†ฅp] (x : E) :
theorem orthogonal_projection_map_apply {๐•œ : Type u_1} [is_R_or_C ๐•œ] {E : Type u_2} {E' : Type u_3} [inner_product_space ๐•œ E] [inner_product_space ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') (p : submodule ๐•œ E) [complete_space โ†ฅp] (x : E') :

Orthogonal projection onto the submodule.map of a subspace.

@[simp]
theorem orthogonal_projection_bot {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] :

The orthogonal projection onto the trivial submodule is the zero map.

theorem orthogonal_projection_norm_le {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :

The orthogonal projection has norm โ‰ค 1.

theorem smul_orthogonal_projection_singleton (๐•œ : Type u_1) {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {v : E} (w : E) :
theorem orthogonal_projection_singleton (๐•œ : Type u_1) {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {v : E} (w : E) :

Formula for orthogonal projection onto a single vector.

theorem orthogonal_projection_unit_singleton (๐•œ : Type u_1) {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {v : E} (hv : โˆฅvโˆฅ = 1) (w : E) :

Formula for orthogonal projection onto a single unit vector.

noncomputable def reflection_linear_equiv {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :
E โ‰ƒโ‚—[๐•œ] E

Auxiliary definition for reflection: the reflection as a linear equivalence.

Equations
noncomputable def reflection {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :

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
theorem reflection_apply {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (p : E) :

The result of reflecting.

@[simp]
theorem reflection_symm {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] :

Reflection is its own inverse.

@[simp]
theorem reflection_inv {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] :

Reflection is its own inverse.

@[simp]
theorem reflection_reflection {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] (p : E) :

Reflecting twice in the same subspace.

theorem reflection_involutive {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :

Reflection is involutive.

@[simp]
theorem reflection_trans_reflection {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :

Reflection is involutive.

@[simp]
theorem reflection_mul_reflection {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :

Reflection is involutive.

theorem reflection_eq_self_iff {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] (x : E) :

A point is its own reflection if and only if it is in the subspace.

theorem reflection_mem_subspace_eq_self {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {x : E} (hx : x โˆˆ K) :
theorem reflection_map_apply {๐•œ : Type u_1} [is_R_or_C ๐•œ] {E : Type u_2} {E' : Type u_3} [inner_product_space ๐•œ E] [inner_product_space ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') (K : submodule ๐•œ E) [complete_space โ†ฅK] (x : E') :

Reflection in the submodule.map of a subspace.

theorem reflection_map {๐•œ : Type u_1} [is_R_or_C ๐•œ] {E : Type u_2} {E' : Type u_3} [inner_product_space ๐•œ E] [inner_product_space ๐•œ E'] (f : E โ‰ƒโ‚—แตข[๐•œ] E') (K : submodule ๐•œ E) [complete_space โ†ฅK] :

Reflection in the submodule.map of a subspace.

@[simp]
theorem reflection_bot {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] :

Reflection through the trivial subspace {0} is just negation.

theorem submodule.sup_orthogonal_inf_of_complete_space {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {Kโ‚ Kโ‚‚ : submodule ๐•œ E} (h : Kโ‚ โ‰ค Kโ‚‚) [complete_space โ†ฅKโ‚] :
Kโ‚ โŠ” Kโ‚แ—ฎ โŠ“ Kโ‚‚ = Kโ‚‚

If Kโ‚ is complete and contained in Kโ‚‚, Kโ‚ and Kโ‚แ—ฎ โŠ“ Kโ‚‚ span Kโ‚‚.

theorem submodule.sup_orthogonal_of_complete_space {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] :

If K is complete, K and Kแ—ฎ span the whole space.

theorem submodule.exists_sum_mem_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] (v : E) :
โˆƒ (y : E) (H : y โˆˆ K) (z : E) (H : z โˆˆ Kแ—ฎ), v = y + z

If K is complete, any v in E can be expressed as a sum of elements of K and Kแ—ฎ.

@[simp]
theorem submodule.orthogonal_orthogonal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space โ†ฅK] :

If K is complete, then the orthogonal complement of its orthogonal complement is itself.

theorem submodule.orthogonal_orthogonal_eq_closure {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] (K : submodule ๐•œ E) [complete_space E] :
theorem submodule.is_compl_orthogonal_of_complete_space {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] :

If K is complete, K and Kแ—ฎ are complements of each other.

@[simp]
theorem submodule.orthogonal_eq_bot_iff {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅโ†‘K] :
theorem eq_orthogonal_projection_of_mem_orthogonal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {u v : E} (hv : v โˆˆ K) (hvo : u - v โˆˆ Kแ—ฎ) :

A point in K with the orthogonality property (here characterized in terms of Kแ—ฎ) must be the orthogonal projection.

theorem eq_orthogonal_projection_of_mem_orthogonal' {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {u v z : E} (hv : v โˆˆ K) (hz : z โˆˆ Kแ—ฎ) (hu : u = v + z) :

A point in K with the orthogonality property (here characterized in terms of Kแ—ฎ) must be the orthogonal projection.

theorem orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {v : E} (hv : v โˆˆ Kแ—ฎ) :

The orthogonal projection onto K of an element of Kแ—ฎ is zero.

theorem reflection_mem_subspace_orthogonal_complement_eq_neg {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space โ†ฅK] {v : E} (hv : v โˆˆ Kแ—ฎ) :

The reflection in K of an element of Kแ—ฎ is its negation.

theorem orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space E] {v : E} (hv : v โˆˆ K) :

The orthogonal projection onto Kแ—ฎ of an element of K is zero.

theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {K : submodule ๐•œ E} [complete_space E] {v : E} (hv : v โˆˆ K) :

The reflection in Kแ—ฎ of an element of K is its negation.

theorem orthogonal_projection_orthogonal_complement_singleton_eq_zero {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [complete_space E] (v : E) :

The orthogonal projection onto (๐•œ โˆ™ v)แ—ฎ of v is zero.

theorem reflection_orthogonal_complement_singleton_eq_neg {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [complete_space E] (v : E) :

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.

theorem submodule.finrank_add_inf_finrank_orthogonal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {Kโ‚ Kโ‚‚ : submodule ๐•œ E} [finite_dimensional ๐•œ โ†ฅKโ‚‚] (h : Kโ‚ โ‰ค 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โ‚‚.

theorem submodule.finrank_add_inf_finrank_orthogonal' {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {Kโ‚ Kโ‚‚ : submodule ๐•œ E} [finite_dimensional ๐•œ โ†ฅKโ‚‚] (h : Kโ‚ โ‰ค Kโ‚‚) {n : โ„•} (h_dim : finite_dimensional.finrank ๐•œ โ†ฅKโ‚ + n = finite_dimensional.finrank ๐•œ โ†ฅKโ‚‚) :
finite_dimensional.finrank ๐•œ โ†ฅ(Kโ‚แ—ฎ โŠ“ Kโ‚‚) = n

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โ‚‚.

theorem submodule.finrank_add_finrank_orthogonal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] (K : submodule ๐•œ E) :

Given a finite-dimensional space E and subspace K, the dimensions of K and Kแ—ฎ add to that of E.

theorem submodule.finrank_add_finrank_orthogonal' {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {K : submodule ๐•œ E} {n : โ„•} (h_dim : finite_dimensional.finrank ๐•œ โ†ฅK + n = finite_dimensional.finrank ๐•œ E) :

Given a finite-dimensional space E and subspace K, the dimensions of K and Kแ—ฎ add to that of E.

theorem finrank_orthogonal_span_singleton {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {n : โ„•} [fact (finite_dimensional.finrank ๐•œ E = n + 1)] {v : E} (hv : v โ‰  0) :

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.

theorem orthogonal_family.is_internal_iff_of_is_complete {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {ฮน : Type u_4} [decidable_eq ฮน] {V : ฮน โ†’ submodule ๐•œ E} (hV : orthogonal_family ๐•œ (ฮป (i : ฮน), (V i).subtypeโ‚—แตข)) (hc : is_complete โ†‘(supr V)) :

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.

theorem orthogonal_family.is_internal_iff {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {ฮน : Type u_4} [decidable_eq ฮน] [finite_dimensional ๐•œ E] {V : ฮน โ†’ submodule ๐•œ E} (hV : orthogonal_family ๐•œ (ฮป (i : ฮน), (V i).subtypeโ‚—แตข)) :

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.

Existence of orthonormal basis, etc. #

theorem maximal_orthonormal_iff_orthogonal_complement_eq_bot {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {v : set E} (hv : orthonormal ๐•œ coe) :
(โˆ€ (u : set E), u โŠ‡ v โ†’ orthonormal ๐•œ coe โ†’ u = v) โ†” (submodule.span ๐•œ v)แ—ฎ = โŠฅ

An orthonormal set in an inner_product_space is maximal, if and only if the orthogonal complement of its span is empty.

theorem maximal_orthonormal_iff_basis_of_finite_dimensional {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {v : set E} [finite_dimensional ๐•œ E] (hv : orthonormal ๐•œ coe) :
(โˆ€ (u : set E), u โŠ‡ v โ†’ orthonormal ๐•œ coe โ†’ u = v) โ†” โˆƒ (b : basis โ†ฅv ๐•œ E), โ‡‘b = coe

An orthonormal set in a finite-dimensional inner_product_space is maximal, if and only if it is a basis.

theorem exists_subset_is_orthonormal_basis {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] {v : set E} [finite_dimensional ๐•œ E] (hv : orthonormal ๐•œ coe) :
โˆƒ (u : set E) (H : u โŠ‡ v) (b : basis โ†ฅu ๐•œ E), orthonormal ๐•œ โ‡‘b โˆง โ‡‘b = coe

In a finite-dimensional inner_product_space, any orthonormal subset can be extended to an orthonormal basis.

def orthonormal_basis_index (๐•œ : Type u_1) (E : Type u_2) [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] :
set E

Index for an arbitrary orthonormal basis on a finite-dimensional inner_product_space.

Equations
Instances for โ†ฅorthonormal_basis_index
noncomputable def std_orthonormal_basis (๐•œ : Type u_1) (E : Type u_2) [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] :
basis โ†ฅ(orthonormal_basis_index ๐•œ E) ๐•œ E

A finite-dimensional inner_product_space has an orthonormal basis.

Equations
theorem std_orthonormal_basis_orthonormal (๐•œ : Type u_1) (E : Type u_2) [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] :
@[simp]
theorem coe_std_orthonormal_basis (๐•œ : Type u_1) (E : Type u_2) [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] :
@[protected, instance]
noncomputable def orthonormal_basis_index.fintype (๐•œ : Type u_1) (E : Type u_2) [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] :
Equations
noncomputable def fin_std_orthonormal_basis {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) :
basis (fin n) ๐•œ E

An n-dimensional inner_product_space has an orthonormal basis indexed by fin n.

Equations
theorem fin_std_orthonormal_basis_orthonormal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) :
noncomputable def direct_sum.is_internal.sigma_orthonormal_basis_index_equiv {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) {ฮน : Type u_4} [fintype ฮน] [decidable_eq ฮน] {V : ฮน โ†’ submodule ๐•œ E} (hV : direct_sum.is_internal V) :
(ฮฃ (i : ฮน), โ†ฅ(orthonormal_basis_index ๐•œ โ†ฅ(V i))) โ‰ƒ fin n

Exhibit a bijection between fin n and the index set of a certain basis of an n-dimensional inner product space E. This should not be accessed directly, but only via the subsequent API.

Equations
noncomputable def direct_sum.is_internal.subordinate_orthonormal_basis {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) {ฮน : Type u_4} [fintype ฮน] [decidable_eq ฮน] {V : ฮน โ†’ submodule ๐•œ E} (hV : direct_sum.is_internal V) :
basis (fin n) ๐•œ E

An n-dimensional inner_product_space equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by fin n and subordinate to that direct sum.

Equations
noncomputable def direct_sum.is_internal.subordinate_orthonormal_basis_index {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) {ฮน : Type u_4} [fintype ฮน] [decidable_eq ฮน] {V : ฮน โ†’ submodule ๐•œ E} (hV : direct_sum.is_internal V) (a : fin n) :
ฮน

An n-dimensional inner_product_space equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by fin n and subordinate to that direct sum. This function provides the mapping by which it is subordinate.

Equations
theorem direct_sum.is_internal.subordinate_orthonormal_basis_orthonormal {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) {ฮน : Type u_4} [fintype ฮน] [decidable_eq ฮน] {V : ฮน โ†’ submodule ๐•œ E} (hV : direct_sum.is_internal V) (hV' : orthogonal_family ๐•œ (ฮป (i : ฮน), (V i).subtypeโ‚—แตข)) :

The basis constructed in orthogonal_family.subordinate_orthonormal_basis is orthonormal.

theorem direct_sum.is_internal.subordinate_orthonormal_basis_subordinate {๐•œ : Type u_1} {E : Type u_2} [is_R_or_C ๐•œ] [inner_product_space ๐•œ E] [finite_dimensional ๐•œ E] {n : โ„•} (hn : finite_dimensional.finrank ๐•œ E = n) {ฮน : Type u_4} [fintype ฮน] [decidable_eq ฮน] {V : ฮน โ†’ submodule ๐•œ E} (hV : direct_sum.is_internal V) (a : fin n) :

The basis constructed in orthogonal_family.subordinate_orthonormal_basis is subordinate to the orthogonal_family in question.