Products and norms of orthogonal projections

For submodules U and V of an inner product space admitting orthogonal projections P_U and P_V, the two products P_U P_V and P_V P_U have the same operator norm. Since P_V P_U = (P_U P_V)†, this is the identity ‖T‖ = ‖T†‖, stated here without any completeness hypothesis on the ambient space, where the adjoint of a bounded operator need not exist.

A map T P_U that factors through the projection onto a finite-dimensional U has rank at most dim U. For subspaces U and V of the same finite dimension, U ⊓ Vᗮ and V ⊓ Uᗮ have the same dimension. The orthogonal complement of a nonzero vector has codimension one, and fewer than dim E vectors have a common nonzero orthogonal vector, which may be taken of norm one. A nonzero vector followed by a linearly independent family in its orthogonal complement is linearly independent.

For a family of subspaces K x of a finite-dimensional real inner product space whose orthogonal projections are continuous at x₀, projecting linearly independent vectors of K x₀ onto K x keeps them linearly independent near x₀. If moreover a second such family L x has dim K x + dim L x = dim E near x₀, the projections of a basis of K x₀ form a basis of K x near x₀.

For finite-dimensional U and V with dim V ≤ dim U, a lower bound k ‖u‖² ≤ ‖P_V u‖² for u ∈ U transfers to the same lower bound k ‖v‖² ≤ ‖P_U v‖² for v ∈ V.

The projection P_U v is the point of v + Uᗮ of least norm, and it is the only one: a vector w with ‖w‖ ≤ ‖P_U w‖ equals P_U w. Equivalently, v ∈ U exactly when adding a vector of Uᗮ never decreases the norm of v. Over ℝ, Pythagoras splits the squared distance from a point b + c, with b ∈ U and c ∈ Uᗮ, into its components along U and Uᗮ.

Since the kernel of P_V is Vᗮ, the projection P_V is injective on U exactly when no nonzero vector of U is orthogonal to V.

Compressing the square of the difference P_U - P_V to U, from either side, gives P_U - P_U P_V P_U.

A linear map agrees with its composition with the orthogonal projection onto the orthogonal complement of its kernel whenever the kernel admits an orthogonal projection.

Provenance

The submodule inclusion-adjoint identity is adapted from ForTauCeti/Analysis/InnerProductSpace/SinTheta/Perturbation.lean in the AIQ-Kitware DKPS formalization (Apache-2.0; Jon Crall and GPT-6).

Main results

• Submodule.adjoint_subtype: the adjoint of subspace inclusion is orthogonal projection onto that subspace.
• Submodule.adjoint_orthogonalProjectionOnto_toLinearMap: the adjoint of restricted orthogonal projection is subspace inclusion.
• Submodule.norm_starProjection_comp_starProjection_comm: ‖P_U P_V‖ = ‖P_V P_U‖.
• Submodule.finrank_range_comp_starProjection_le: rank (T P_U) ≤ dim U.
• Submodule.finrank_inf_orthogonal_comm: dim (U ⊓ Vᗮ) = dim (V ⊓ Uᗮ) when dim U = dim V.
• Submodule.finrank_orthogonal_span_singleton_eq_finrank_sub_one: dim (𝕜 ∙ v)ᗮ = dim E - 1 for a nonzero vector v.
• TauCeti.exists_ne_zero_forall_inner_eq_zero_of_card_lt_finrank, TauCeti.exists_norm_eq_one_forall_inner_eq_zero_of_card_lt_finrank: fewer than dim E vectors have a common nonzero, and hence a common unit, orthogonal vector.
• TauCeti.ne_neg_of_inner_eq_zero: a vector orthogonal to a nonzero vector b is not -b.
• TauCeti.eventually_linearIndependent_starProjection_apply, TauCeti.eventually_linearIndependent_and_span_starProjection: projected bases of a continuously varying family of subspaces stay linearly independent, and stay bases under a complementary dimension count.
• LinearIndependent.finCons_orthogonal_span_singleton: a nonzero vector p followed by a linearly independent family in (𝕜 ∙ p)ᗮ is linearly independent.
• LinearIsometry.exists_mem_sphere_inner_eq_zero: a linear isometry into a space of larger finite dimension has a unit vector orthogonal to its range.
• Submodule.mul_norm_sq_le_norm_starProjection_sq_of_finrank_le: for a finite-dimensional subspace V and a subspace U with dim V ≤ dim U, a lower bound on ‖P_V u‖² over U transfers to the same bound on ‖P_U v‖² over V.
• Submodule.eq_starProjection_of_norm_le: a vector whose norm is at most that of its projection is its projection.
• Submodule.mem_iff_forall_mem_orthogonal_norm_le_norm_add: v ∈ U if and only if ‖v‖ ≤ ‖v + w‖ for every w ∈ Uᗮ.
• Submodule.norm_sub_add_sq_of_mem_of_mem_orthogonal: Pythagoras for ‖v - (b + c)‖² with b ∈ R and c ∈ Rᗮ, split along R and Rᗮ.
• Submodule.injOn_starProjection_iff_disjoint: P_V is injective on U if and only if U ⊓ Vᗮ = ⊥.
• Submodule.starProjection_sub_starProjection_sq_mul_starProjection, Submodule.starProjection_mul_starProjection_sub_starProjection_sq: (P_U - P_V)² P_U = P_U (P_U - P_V)² = P_U - P_U P_V P_U.
• Submodule.span_range_starProjection_orthogonal_basis_succ: if the zeroth coordinate of v in a basis is nonzero, the projections onto (𝕜 ∙ v)ᗮ of the other basis vectors span it.
• LinearMap.apply_sub_starProjection_ker, ContinuousLinearMap.comp_starProjection_orthogonal_ker: maps ignore their kernel component.

theorem Submodule.norm_starProjection_comp_starProjection_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ‖U.starProjection ∘SL V.starProjection‖ = ‖V.starProjection ∘SL U.starProjection‖

The two products of a pair of orthogonal projections have the same operator norm, that is, ‖T‖ = ‖T†‖ for T = P_U P_V. No completeness of E is assumed.

theorem Submodule.finrank_range_comp_starProjection_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [FiniteDimensional 𝕜 ↥U] (T : E →ₗ[𝕜] F) : Module.finrank 𝕜 ↥(T ∘ₗ ↑U.starProjection).range ≤ Module.finrank 𝕜 ↥U

A map T P_U that factors through the projection onto U has rank at most dim U.

theorem Submodule.finrank_inf_orthogonal_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥U] [FiniteDimensional 𝕜 ↥V] (h : Module.finrank 𝕜 ↥U = Module.finrank 𝕜 ↥V) : Module.finrank 𝕜 ↥(U ⊓ Vᗮ) = Module.finrank 𝕜 ↥(V ⊓ Uᗮ)

For finite-dimensional subspaces of the same dimension, U ⊓ Vᗮ and V ⊓ Uᗮ have the same dimension.

theorem Submodule.finrank_orthogonal_span_singleton_eq_finrank_sub_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {v : E} (hv : v ≠ 0) : Module.finrank 𝕜 ↥(𝕜 ∙ v)ᗮ = Module.finrank 𝕜 E - 1

In a finite-dimensional inner product space, the orthogonal complement of the span of a nonzero vector has codimension one. Unlike Submodule.finrank_orthogonal_span_singleton, the dimension of the ambient space is not fixed in advance.

theorem Submodule.mul_norm_sq_le_norm_starProjection_sq_of_finrank_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥V] (h : Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 ↥U) {k : ℝ} (hU : ∀ u ∈ U, k * ‖u‖ ^ 2 ≤ ‖V.starProjection u‖ ^ 2) {v : E} (hv : v ∈ V) : k * ‖v‖ ^ 2 ≤ ‖U.starProjection v‖ ^ 2

For a finite-dimensional subspace V and a subspace U with dim V ≤ dim U, a lower bound k ‖u‖² ≤ ‖P_V u‖² on the cosines of U towards V transfers to the same lower bound for V towards U.

theorem Submodule.eq_starProjection_of_norm_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {w : E} (hw : ‖w‖ ≤ ‖U.starProjection w‖) : w = U.starProjection w

A vector whose norm is at most that of its orthogonal projection onto U is that projection, since the projection never increases the norm and only fixes the norm of vectors of U.

theorem Submodule.mem_iff_forall_mem_orthogonal_norm_le_norm_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] {v : E} : v ∈ U ↔ ∀ w ∈ Uᗮ, ‖v‖ ≤ ‖v + w‖

A vector lies in U if and only if adding a vector of Uᗮ never decreases its norm.

theorem Submodule.injOn_starProjection_iff_disjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [V.HasOrthogonalProjection] : Set.InjOn ⇑V.starProjection ↑U ↔ Disjoint U Vᗮ

The orthogonal projection onto V is injective on U exactly when U ⊓ Vᗮ = ⊥, since its kernel is Vᗮ.

theorem Submodule.starProjection_sub_starProjection_sq_mul_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : (U.starProjection - V.starProjection) ^ 2 * U.starProjection = U.starProjection - U.starProjection * V.starProjection * U.starProjection

Compressing (P_U - P_V)² to U on the right gives P_U - P_U P_V P_U.

theorem Submodule.starProjection_mul_starProjection_sub_starProjection_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection * (U.starProjection - V.starProjection) ^ 2 = U.starProjection - U.starProjection * V.starProjection * U.starProjection

Compressing (P_U - P_V)² to U on the left gives P_U - P_U P_V P_U.

@[simp]

theorem Submodule.adjoint_subtype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] [FiniteDimensional 𝕜 E] : LinearMap.adjoint U.subtype = ↑U.orthogonalProjectionOnto

The adjoint of the inclusion U → E is the orthogonal projection E → U. Both maps are regarded as finite-dimensional algebraic linear maps.

@[simp]

theorem Submodule.adjoint_orthogonalProjectionOnto_toLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] [FiniteDimensional 𝕜 E] : LinearMap.adjoint ↑U.orthogonalProjectionOnto = U.subtype

The algebraic adjoint of the orthogonal projection E → U is the inclusion U → E. This is the elementary simplification rule for the adjoints of cross-projections and self-adjoint compressions, together with LinearMap.adjoint_comp.

theorem Submodule.span_range_starProjection_orthogonal_basis_succ {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {k : ℕ} (b : Module.Basis (Fin (k + 1)) 𝕜 E) {v : E} (hv : (b.repr v) 0 ≠ 0) : span 𝕜 (Set.range fun (j : Fin k) => (𝕜 ∙ v)ᗮ.starProjection (b j.succ)) = (𝕜 ∙ v)ᗮ

If the zeroth coordinate of v in a basis b is nonzero, then the orthogonal projections onto (𝕜 ∙ v)ᗮ of the remaining basis vectors span (𝕜 ∙ v)ᗮ.

theorem Submodule.norm_sub_add_sq_of_mem_of_mem_orthogonal {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (R : Submodule ℝ F) [R.HasOrthogonalProjection] (v : F) {b c : F} (hb : b ∈ R) (hc : c ∈ Rᗮ) : ‖v - (b + c)‖ ^ 2 = ‖R.starProjection v‖ ^ 2 + ‖v - R.starProjection v - c‖ ^ 2 - 2 * inner ℝ b (R.starProjection v) + ‖b‖ ^ 2

Pythagoras for the squared distance from b + c, where b ∈ R and c ∈ Rᗮ: the components of v - (b + c) along R and Rᗮ are P v - b and v - P v - c, where P is the orthogonal projection onto R.

theorem TauCeti.exists_ne_zero_forall_inner_eq_zero_of_card_lt_finrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (s : Finset E) (hs : s.card < Module.finrank 𝕜 E) : ∃ (e : E), e ≠ 0 ∧ ∀ u ∈ s, inner 𝕜 u e = 0

Fewer than dim E vectors have a common nonzero orthogonal vector: the orthogonal complement of their span is nontrivial.

theorem TauCeti.exists_norm_eq_one_forall_inner_eq_zero_of_card_lt_finrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (s : Finset E) (hs : s.card < Module.finrank 𝕜 E) : ∃ (e : E), ‖e‖ = 1 ∧ ∀ u ∈ s, inner 𝕜 u e = 0

Fewer than dim E vectors have a common orthogonal unit vector.

theorem TauCeti.ne_neg_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {a b : E} (hb : b ≠ 0) (hab : inner 𝕜 a b = 0) : a ≠ -b

A vector orthogonal to a nonzero vector b is not -b.

theorem TauCeti.eventually_linearIndependent_starProjection_apply {X : Type u_3} [TopologicalSpace X] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {K : X → Submodule ℝ F} {x₀ : X} (hK : ContinuousAt (fun (x : X) => (K x).starProjection) x₀) {ι : Type u_5} [Finite ι] {b : ι → F} (hb : LinearIndependent ℝ b) (hbK : ∀ (i : ι), b i ∈ K x₀) : ∀ᶠ (x : X) in nhds x₀, LinearIndependent ℝ fun (i : ι) => (K x).starProjection (b i)

Projecting linearly independent vectors of K x₀ onto K x keeps them linearly independent for x near x₀, when the orthogonal projections onto the subspaces K x are continuous at x₀.

theorem TauCeti.eventually_linearIndependent_and_span_starProjection {X : Type u_3} [TopologicalSpace X] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {K L : X → Submodule ℝ F} {x₀ : X} (hK : ContinuousAt (fun (x : X) => (K x).starProjection) x₀) (hL : ContinuousAt (fun (x : X) => (L x).starProjection) x₀) (hdim : ∀ᶠ (x : X) in nhds x₀, Module.finrank ℝ ↥(K x) + Module.finrank ℝ ↥(L x) = Module.finrank ℝ F) {k : ℕ} (b : Module.Basis (Fin k) ℝ ↥(K x₀)) : ∀ᶠ (x : X) in nhds x₀, (LinearIndependent ℝ fun (i : Fin k) => (K x).starProjection ↑(b i)) ∧ Submodule.span ℝ (Set.range fun (i : Fin k) => (K x).starProjection ↑(b i)) = K x

Let K x and L x be subspaces whose orthogonal projections are continuous at x₀ and whose dimensions add up to finrank ℝ F near x₀. Then projecting a basis of K x₀ onto K x gives, for every x near x₀, a basis of K x.

theorem LinearIndependent.finCons_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : ℕ} {p : E} (hp : p ≠ 0) {w : Fin m → E} (hw : LinearIndependent 𝕜 w) (hwp : ∀ (i : Fin m), w i ∈ (𝕜 ∙ p)ᗮ) : LinearIndependent 𝕜 (Fin.cons p w)

A nonzero vector followed by a linearly independent family in its orthogonal complement is linearly independent.

theorem LinearIsometry.exists_mem_sphere_inner_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) (h : Module.finrank ℝ F < Module.finrank ℝ E) : ∃ (v : ↑(Metric.sphere 0 1)), ∀ (x : F), inner ℝ (↑v) (ι x) = 0

A linear isometry into a space of larger finite dimension has a unit vector orthogonal to its range. The hypothesis on the dimensions forces the target to be finite-dimensional.

@[simp]

theorem LinearMap.apply_sub_starProjection_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (u : E →ₗ[𝕜] F) [u.ker.HasOrthogonalProjection] (x : E) : u (x - u.ker.starProjection x) = u x

A linear map does not see the component of a vector in its kernel.

@[simp]

theorem ContinuousLinearMap.comp_starProjection_orthogonal_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (u : E →L[𝕜] F) [(↑u).ker.HasOrthogonalProjection] : u ∘SL (↑u).kerᗮ.starProjection = u

Composing a continuous linear map with the orthogonal projection onto the orthogonal complement of its kernel does not change it.