The orthogonal projection onto the range of an operator

If B : F →L[𝕜] V is an operator between inner product spaces whose Gram operator B† B is invertible, the orthogonal projection of V onto the range of B is B (B† B)⁻¹ B†. When F is finite-dimensional, B† B is invertible exactly when B is injective.

Over ℝ this explicit formula shows that the projection depends smoothly on the operator: for a C^n family of injective operators A u : E →L[ℝ] V out of a finite-dimensional real normed space E, the orthogonal projections of V onto the ranges of A u form a C^n family. Applied to the derivative of an immersion into a Euclidean space, this says that the tangent spaces, and hence the normal spaces, of an immersed submanifold vary smoothly.

Main results

• ContinuousLinearMap.isUnit_adjoint_comp_self: the Gram operator of an injective operator out of a finite-dimensional space is invertible.
• ContinuousLinearMap.starProjection_range_eq: the formula B (B† B)⁻¹ B† for the orthogonal projection onto the range of B.
• ContinuousLinearMap.finrank_orthogonal_range_of_injective: the dimension of the orthogonal complement of the range of an injective operator.
• Submodule.starProjection_inverse_apply: if the compression to W of the orthogonal projection onto K is invertible, it inverts the projection from W onto K.
• ContDiffAt.starProjection_range, ContDiffAt.starProjection_orthogonal_range: the orthogonal projections onto the range of a C^n family of injective operators, and onto its orthogonal complement, are C^n.

theorem ContinuousLinearMap.isUnit_adjoint_comp_self {𝕜 : Type u_1} {F : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] [FiniteDimensional 𝕜 F] {B : F →L[𝕜] V} (hB : Function.Injective ⇑B) : IsUnit (adjoint B ∘SL B)

The Gram operator B† B of an injective operator out of a finite-dimensional space is invertible.

theorem ContinuousLinearMap.starProjection_range_eq {𝕜 : Type u_1} {F : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {B : F →L[𝕜] V} [(↑B).range.HasOrthogonalProjection] (hB : IsUnit (adjoint B ∘SL B)) : (↑B).range.starProjection = B ∘SL Ring.inverse (adjoint B ∘SL B) ∘SL adjoint B

The orthogonal projection onto the range of B is B (B† B)⁻¹ B†, when the Gram operator B† B is invertible.

theorem ContinuousLinearMap.finrank_orthogonal_range_of_injective {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {A : E →L[𝕜] V} (hA : Function.Injective ⇑A) : Module.finrank 𝕜 ↥(↑A).rangeᗮ = Module.finrank 𝕜 V - Module.finrank 𝕜 E

The orthogonal complement of the range of an injective operator into a finite-dimensional inner product space has the expected dimension.

theorem Submodule.starProjection_inverse_apply {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {K W : Submodule 𝕜 V} (hrank : Module.finrank 𝕜 ↥W = Module.finrank 𝕜 ↥K) (hR : IsUnit (W.orthogonalProjectionOnto ∘SL K.starProjection ∘SL W.subtypeL)) {v : V} (hv : v ∈ K) : K.starProjection ↑((Ring.inverse (W.orthogonalProjectionOnto ∘SL K.starProjection ∘SL W.subtypeL)) (W.orthogonalProjectionOnto v)) = v

Let K and W be subspaces of the same dimension. If the compression R = π_W ∘ P_K ∘ ι_W of the orthogonal projection onto K is invertible, then P_K maps W onto K, and the preimage of v ∈ K is R⁻¹ (π_W v).

theorem ContDiffAt.starProjection_range {X : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {A : X → E →L[ℝ] V} {u₀ : X} {n : WithTop ℕ∞} (hA : ContDiffAt ℝ n A u₀) (hinj : Function.Injective ⇑(A u₀)) : ContDiffAt ℝ n (fun (u : X) => (↑(A u)).range.starProjection) u₀

The orthogonal projection onto the range of a C^n family of operators out of a finite-dimensional space is C^n at every point where the operator is injective.

theorem ContDiffAt.starProjection_orthogonal_range {X : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {A : X → E →L[ℝ] V} {u₀ : X} {n : WithTop ℕ∞} (hA : ContDiffAt ℝ n A u₀) (hinj : Function.Injective ⇑(A u₀)) : ContDiffAt ℝ n (fun (u : X) => (↑(A u)).rangeᗮ.starProjection) u₀

The orthogonal projection onto the orthogonal complement of the range of a C^n family of operators out of a finite-dimensional space is C^n at every point where the operator is injective.