The cosine and sine angle operators of two subspaces

Let U and V be subspaces of a Hilbert space E with orthogonal projections P_U and P_V. The cosine angle operator of (U, V) is the modulus |P_V P_U| of the cosine map, and the sine angle operator is the modulus |P_U - P_V| of the difference of the two projections. They are the operator-valued cos Θ and sin Θ of the pair, defined in every dimension through the modulus ContinuousLinearMap.modulus of a bounded operator.

The two operators satisfy the operator form of cos² Θ + sin² Θ = 1 on U:

|P_V P_U|² + |P_U - P_V|² P_U = P_U.

The sine angle operator is symmetric in U and V, commutes with P_U (hence, by symmetry, with P_V) and with the cosine angle operator, and its compression to U is the modulus of the directed sine map P_{Vᗮ} P_U. Its operator norm is the projection gap ‖P_U - P_V‖, and its kernel is (U ⊓ V) ⊔ (Uᗮ ⊓ Vᗮ), the vectors on which the two projections agree.

Main definitions

• Submodule.cosAngleOperator U V: the cosine angle operator |P_V P_U|.
• Submodule.sinAngleOperator U V: the sine angle operator |P_U - P_V|.

Main results

• Submodule.cosAngleOperator_sq, Submodule.sinAngleOperator_sq: the squares are P_U P_V P_U and (P_U - P_V)².
• Submodule.cosAngleOperator_sq_add_sinAngleOperator_sq_mul_starProjection: the Pythagorean identity cos² Θ + sin² Θ P_U = P_U.
• Submodule.commute_starProjection_sinAngleOperator, Submodule.commute_cosAngleOperator_sinAngleOperator: the sine angle operator commutes with P_U and with the cosine angle operator.
• Submodule.sinAngleOperator_mul_starProjection: |P_U - P_V| P_U = |P_{Vᗮ} P_U|.
• Submodule.norm_sinAngleOperator: ‖|P_U - P_V|‖ is the projection gap.
• Submodule.singularValues_sinAngleOperator_eq_sub_starProjection: the sine-angle operator and projector difference have identical singular values.
• Submodule.ker_sinAngleOperator: the kernel of the sine angle operator is (U ⊓ V) ⊔ (Uᗮ ⊓ Vᗮ); Submodule.sinAngleOperator_eq_zero_iff: it vanishes exactly when U = V.

Provenance

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

References

• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1–46.
• T. Kato, Perturbation Theory for Linear Operators, 2nd ed., Springer (1976), §I.4.6.

noncomputable def Submodule.cosAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : E →L[𝕜] E

The cosine angle operator |P_V P_U| of two subspaces: the modulus of the cosine map.

noncomputable def Submodule.sinAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : E →L[𝕜] E

The sine angle operator |P_U - P_V| of two subspaces: the modulus of the difference of the orthogonal projections.

theorem Submodule.cosAngleOperator_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.cosAngleOperator V = (U.cosThetaMap V).modulus

theorem Submodule.sinAngleOperator_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinAngleOperator V = (U.starProjection - V.starProjection).modulus

theorem Submodule.isPositive_cosAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : (U.cosAngleOperator V).IsPositive

theorem Submodule.isPositive_sinAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : (U.sinAngleOperator V).IsPositive

Squares, norms and kernels

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

The square of the cosine angle operator is the compression P_U P_V P_U.

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

The square of the sine angle operator is the square of the difference of the projections.

@[simp]

theorem Submodule.norm_cosAngleOperator_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (x : E) : ‖(U.cosAngleOperator V) x‖ = ‖V.starProjection (U.starProjection x)‖

@[simp]

theorem Submodule.norm_sinAngleOperator_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (x : E) : ‖(U.sinAngleOperator V) x‖ = ‖U.starProjection x - V.starProjection x‖

@[simp]

theorem Submodule.singularValues_sinAngleOperator_eq_sub_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] [FiniteDimensional 𝕜 E] : (↑(U.sinAngleOperator V)).singularValues = (↑(U.starProjection - V.starProjection)).singularValues

The symmetric sine-angle operator and the difference of the two orthogonal projections have identical singular values.

@[simp]

theorem Submodule.norm_cosAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ‖U.cosAngleOperator V‖ = ‖U.cosThetaMap V‖

The operator norm of the cosine angle operator is that of the cosine map P_V P_U.

@[simp]

theorem Submodule.norm_sinAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ‖U.sinAngleOperator V‖ = U.projectionGap V

The operator norm of the sine angle operator is the projection gap ‖P_U - P_V‖.

theorem Submodule.norm_cosAngleOperator_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ‖U.cosAngleOperator V‖ ≤ 1

theorem Submodule.norm_sinAngleOperator_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ‖U.sinAngleOperator V‖ ≤ 1

theorem Submodule.mem_ker_cosAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] {x : E} : x ∈ (↑(U.cosAngleOperator V)).ker ↔ U.starProjection x ∈ Vᗮ

The kernel of the cosine angle operator is the set of vectors whose projection to U is orthogonal to V.

theorem Submodule.ker_sinAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : (↑(U.sinAngleOperator V)).ker = U ⊓ V ⊔ Uᗮ ⊓ Vᗮ

The kernel of the sine angle operator is (U ⊓ V) ⊔ (Uᗮ ⊓ Vᗮ): a vector is annihilated by |P_U - P_V| exactly when its components in U and in V coincide.

@[simp]

theorem Submodule.cosAngleOperator_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.cosAngleOperator V = 0 ↔ U ⟂ V

The cosine angle operator vanishes exactly when U and V are orthogonal.

@[simp]

theorem Submodule.sinAngleOperator_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinAngleOperator V = 0 ↔ U = V

The sine angle operator vanishes exactly when U = V.

Symmetries and special cases

theorem Submodule.sinAngleOperator_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : V.sinAngleOperator U = U.sinAngleOperator V

The sine angle operator is symmetric in the two subspaces.

@[simp]

theorem Submodule.sinAngleOperator_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : Uᗮ.sinAngleOperator Vᗮ = U.sinAngleOperator V

Passing to orthogonal complements does not change the sine angle operator.

@[simp]

theorem Submodule.sinAngleOperator_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.sinAngleOperator U = 0

@[simp]

theorem Submodule.cosAngleOperator_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.cosAngleOperator U = U.starProjection

The cosine angle operator of a subspace with itself is its orthogonal projection.

Interaction with the projections

@[simp]

theorem Submodule.cosAngleOperator_mul_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.cosAngleOperator V * U.starProjection = U.cosAngleOperator V

The cosine angle operator vanishes on Uᗮ: |P_V P_U| P_U = |P_V P_U|.

@[simp]

theorem Submodule.starProjection_mul_cosAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection * U.cosAngleOperator V = U.cosAngleOperator V

The cosine angle operator takes values in U: P_U |P_V P_U| = |P_V P_U|.

theorem Submodule.commute_starProjection_sinAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : Commute U.starProjection (U.sinAngleOperator V)

The sine angle operator commutes with the projection onto U.

theorem Submodule.cosAngleOperator_sq_add_sinAngleOperator_sq_mul_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.cosAngleOperator V ^ 2 + U.sinAngleOperator V ^ 2 * U.starProjection = U.starProjection

Pythagorean identity. On U, the squares of the cosine and sine angle operators add up to the identity: |P_V P_U|² + |P_U - P_V|² P_U = P_U.

theorem Submodule.sinAngleOperator_mul_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinAngleOperator V * U.starProjection = (U.sinThetaMap V).modulus

The compression of the sine angle operator to U is the modulus of the directed sine map: |P_U - P_V| P_U = |P_{Vᗮ} P_U|.

theorem Submodule.commute_cosAngleOperator_sinAngleOperator {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : Commute (U.cosAngleOperator V) (U.sinAngleOperator V)

The cosine and sine angle operators commute.