Orthogonal projections in finite-dimensional spaces

This file contains results about orthogonal projections in finite-dimensional spaces.

Main results

• Submodule.det_reflection: The determinant of K.reflection is (-1) ^ finrank 𝕜 Kᗮ.
• LinearIsometryEquiv.reflections_generate: The orthogonal group of F is generated by reflections.

Results that do not use finite dimensionality:

• OrthogonalFamily.isInternal_iff_of_isComplete
• OrthogonalFamily.sum_projection_of_mem_iSup
• OrthogonalFamily.projection_directSum_coeAddHom
• OrthogonalFamily.decomposition
• maximal_orthonormal_iff_orthogonalComplement_eq_bot

@[simp]

theorem Submodule.topologicalClosure_eq_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] : K.topologicalClosure = K

@[simp]

theorem Submodule.det_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] : LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ Module.finrank 𝕜 ↥Kᗮ

@[simp]

theorem Submodule.linearEquiv_det_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥K] : LinearEquiv.det K.reflection.toLinearEquiv = (-1) ^ Module.finrank 𝕜 ↥Kᗮ

theorem Submodule.finrank_add_inf_finrank_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) : Module.finrank 𝕜 ↥K₁ + Module.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = Module.finrank 𝕜 ↥K₂

Given a finite-dimensional subspace K₂, and a subspace K₁ contained 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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : Module.finrank 𝕜 ↥K₁ + n = Module.finrank 𝕜 ↥K₂) : Module.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

Given a finite-dimensional subspace K₂, and a subspace K₁ contained 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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E) : Module.finrank 𝕜 ↥K + Module.finrank 𝕜 ↥Kᗮ = Module.finrank 𝕜 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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {K : Submodule 𝕜 E} {n : ℕ} (h_dim : Module.finrank 𝕜 ↥K + n = Module.finrank 𝕜 E) : Module.finrank 𝕜 ↥Kᗮ = n

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

theorem Submodule.finrank_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [_i : Fact (Module.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) : Module.finrank 𝕜 ↥(span 𝕜 {v})ᗮ = n

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.

theorem LinearIsometryEquiv.reflections_generate_dim_aux {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ} (φ : F ≃ₗᵢ[ℝ] F) (hn : Module.finrank ℝ ↥(LinearMap.ker (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤ n) : ∃ (l : List F), l.length ≤ n ∧ φ = (List.map (fun (v : F) => (Submodule.span ℝ {v})ᗮ.reflection) l).prod

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 φ.

theorem LinearIsometryEquiv.reflections_generate_dim {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (φ : F ≃ₗᵢ[ℝ] F) : ∃ (l : List F), l.length ≤ Module.finrank ℝ F ∧ φ = (List.map (fun (v : F) => (Submodule.span ℝ {v})ᗮ.reflection) l).prod

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.

theorem LinearIsometryEquiv.reflections_generate {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] : Subgroup.closure (Set.range fun (v : F) => (Submodule.span ℝ {v})ᗮ.reflection) = ⊤

The orthogonal group of F is generated by reflections.

theorem OrthogonalFamily.isInternal_iff_of_isComplete {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (hc : IsComplete ↑(iSup V)) : DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

An orthogonal family of subspaces of E satisfies DirectSum.IsInternal (that is, they provide an internal direct sum decomposition of E) if and only if their span has trivial orthogonal complement.

theorem OrthogonalFamily.isInternal_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] [FiniteDimensional 𝕜 E] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) : DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

An orthogonal family of subspaces of E satisfies DirectSum.IsInternal (that is, they provide an internal direct sum decomposition of E) if and only if their span has trivial orthogonal complement.

theorem OrthogonalFamily.sum_projection_of_mem_iSup {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] {V : ι → Submodule 𝕜 E} [∀ (i : ι), CompleteSpace ↥(V i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (x : E) (hx : x ∈ iSup V) : ∑ i : ι, (V i).starProjection x = x

If x lies within an orthogonal family v, it can be expressed as a sum of projections.

theorem OrthogonalFamily.projection_directSum_coeAddHom {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (x : DirectSum ι fun (i : ι) => ↥(V i)) (i : ι) [CompleteSpace ↥(V i)] : (V i).orthogonalProjection ((DirectSum.coeAddMonoidHom V) x) = x i

If a family of submodules is orthogonal, then the orthogonalProjection on a direct sum is just the coefficient of that direct sum.

@[reducible, inline]

noncomputable abbrev OrthogonalFamily.decomposition {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] [Fintype ι] {V : ι → Submodule 𝕜 E} [∀ (i : ι), CompleteSpace ↥(V i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (h : iSup V = ⊤) : DirectSum.Decomposition V

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 = (V i).orthogonalProjection x.

See note [reducible non-instances].

Equations

• hV.decomposition h = { decompose' := fun (x : E) => DFinsupp.equivFunOnFintype.symm fun (i : ι) => (V i).orthogonalProjection x, left_inv := ⋯, right_inv := ⋯ }

theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} (hv : Orthonormal 𝕜 Subtype.val) : (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (Submodule.span 𝕜 v)ᗮ = ⊥

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

theorem maximal_orthonormal_iff_basis_of_finiteDimensional {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E] (hv : Orthonormal 𝕜 Subtype.val) : (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ (b : Module.Basis (↑v) 𝕜 E), ⇑b = Subtype.val

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