Principal angles between two subspaces

For subspaces U and V of an inner product space with orthogonal projections P_U and P_V, the relative position of U and V is recorded by the two cross-projections

• the cosine map P_V P_U, which projects vectors of U onto V, and
• the directed sine map P_{Vᗮ} P_U, which keeps the component of a vector of U orthogonal to V,

together with the double-angle operator 2 P_{Uᗮ} P_V P_U, the off-diagonal U → Uᗮ block of 2 P_V, in which sin 2Θ bounds are stated.

In finite dimension the singular values of the cosine map and of the directed sine map are the principal cosines and the principal sines of U and V, each listed in nonincreasing order and padded with zeros, and the principal angles are the arcsines of the principal sines, so they lie in [0, π/2]. These are the quantities in which perturbation bounds for spectral subspaces (the Davis–Kahan sin Θ theorems) are stated; the operator norm of the directed sine map is the directed gap Submodule.directedProjectionGap U V.

The map Submodule.sinThetaEmbedding Z U restricts the directed sine projection to a subspace Z, so it has source Z rather than the ambient space. Its singular values are the directed principal sines, including the zero tail.

The principal cosines are symmetric in U and V. The principal sines are symmetric only when U and V have the same finite dimension (Submodule.principalSines_comm), the main result of this file. Without the dimension hypothesis the statement fails: for a line U inside a plane V, all principal sines of U and V vanish but one principal sine of V and U is 1.

When U is the range of an isometry X : F →L[𝕜] E, for instance the trial map of the Rayleigh–Ritz procedure, the angles are read off X directly: the sine embedding P_{Vᗮ} X and the cosine embedding P_V X have as singular values the principal sines and cosines of U and V, and the operator norm of the sine embedding is the directed gap from U to V.

Main definitions

• Submodule.cosThetaMap U V: the cosine map P_V P_U.
• Submodule.sinThetaMap U V: the directed sine map P_{Vᗮ} P_U.
• Submodule.sinThetaEmbedding Z U: the projection onto Uᗮ restricted to Z, viewed as a continuous linear map from Z into the ambient space.
• Submodule.sinTwoAngleOperator U V: the double-angle operator 2 P_{Uᗮ} P_V P_U.
• Submodule.principalCosines U V, Submodule.principalSines U V: the singular values of the cosine map and of the directed sine map.
• Submodule.principalAngles U V: the arcsines of the principal sines.

Main results

• Submodule.sinThetaEmbedding_apply, Submodule.singularValues_sinThetaEmbedding: the sine embedding acts by projection onto Uᗮ and has directed principal sines as its singular values, without an equal-dimension assumption.
• Submodule.principalSines_range_eq_singularValues, Submodule.principalCosines_range_eq_singularValues: for an isometry X, the principal sines and cosines of range X and V are the singular values of the sine and cosine embeddings.
• Submodule.norm_starProjection_orthogonal_comp: the operator norm of the sine embedding of an isometry is the directed gap.
• Submodule.principalCosines_comm: the principal cosines are symmetric in U and V.
• Submodule.principalSines_comm, Submodule.principalAngles_comm: for subspaces of the same dimension, the principal sines and the principal angles are symmetric in U and V.
• Submodule.principalSines_eq_zero_iff, Submodule.principalAngles_eq_zero_iff: all principal angles of U and V vanish exactly when U ≤ V; in particular the principal angles of a subspace with itself vanish (Submodule.principalAngles_self).
• Submodule.principalCosines_eq_zero_iff: all principal cosines vanish exactly when U ⟂ V.
• Submodule.sin_principalAngles: the sine of the i-th principal angle is the i-th principal sine.
• Submodule.principalSines_zero: the largest principal sine is the directed gap ‖P_{Vᗮ} P_U‖; hence Submodule.forall_principalSines_lt_iff: all principal sines are below c exactly when the directed gap is.
• Submodule.ncard_ofPred_principalAngles_eq_pi_div_two: the number of principal angles from U to V equal to π/2 is dim (U ⊓ Vᗮ); hence Submodule.forall_principalAngles_lt_pi_div_two_iff: all of them are strictly below π/2 exactly when no nonzero vector of U is orthogonal to V.
• Submodule.directedProjectionGap_lt_one_iff: the directed gap from U to V is less than 1 exactly when no nonzero vector of U is orthogonal to V.
• Submodule.forall_principalAngles_lt_iff: all principal angles are below a threshold θ ∈ [-π/2, π/2] exactly when the directed gap is less than sin θ; in particular (Submodule.forall_principalAngles_lt_pi_div_four_iff) they are below π/4 exactly when the directed gap is less than √2/2.
• Submodule.norm_sinTwoAngleOperator_le_one: the double-angle operator is a contraction, and Submodule.sinTwoAngleOperator_eq_zero_iff: it vanishes exactly when P_U and P_V commute.

References

• Å. Björck, G. H. Golub, Numerical methods for computing angles between linear subspaces, Math. Comp. 27 (1973), 579–594.
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1–46.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §VII.1.

The cross-projections

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

The cosine map P_V P_U of two subspaces with orthogonal projections.

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

The directed sine map P_{Vᗮ} P_U of two subspaces with orthogonal projections: it keeps the component orthogonal to V of the projection of a vector onto U.

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

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

@[simp]

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

@[simp]

theorem Submodule.sinThetaMap_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (x : E) : (U.sinThetaMap V) x = Vᗮ.starProjection (U.starProjection x)

theorem Submodule.cosThetaMap_add_sinThetaMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.cosThetaMap V + U.sinThetaMap V = U.starProjection

The cosine and sine maps split the projection onto U: P_V P_U + P_{Vᗮ} P_U = P_U.

theorem Submodule.norm_sinThetaMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ‖U.sinThetaMap V‖ = U.directedProjectionGap V

The operator norm of the directed sine map is the directed gap from U to V.

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

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

@[simp]

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

The cosine map vanishes exactly when U and V are orthogonal.

@[simp]

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

The directed sine map vanishes exactly when U ≤ V.

@[simp]

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

The double-angle operator

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

The double-angle operator 2 P_{Uᗮ} P_V P_U of two subspaces with orthogonal projections: the off-diagonal U → Uᗮ block of 2 P_V relative to E = U ⊕ Uᗮ. It is the operator in which sin 2Θ perturbation bounds for spectral subspaces are stated.

theorem Submodule.sinTwoAngleOperator_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinTwoAngleOperator V = 2 • Uᗮ.starProjection ∘SL V.starProjection ∘SL U.starProjection

@[simp]

theorem Submodule.sinTwoAngleOperator_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (x : E) : (U.sinTwoAngleOperator V) x = 2 • Uᗮ.starProjection (V.starProjection (U.starProjection x))

theorem Submodule.sinTwoAngleOperator_eq_smul_sinThetaMap_comp_cosThetaMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinTwoAngleOperator V = 2 • V.sinThetaMap U ∘SL U.cosThetaMap V

The double-angle operator is twice the directed sine map from V to U composed with the cosine map from U to V: 2 P_{Uᗮ} P_V P_U = 2 (P_{Uᗮ} P_V) (P_V P_U).

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

The double-angle operator is a contraction: ‖2 P_{Uᗮ} P_V P_U‖ ≤ 1, the operator form of sin 2θ ≤ 1.

theorem Submodule.sinTwoAngleOperator_eq_zero_of_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ≤ V) : U.sinTwoAngleOperator V = 0

The double-angle operator vanishes when U ≤ V.

theorem Submodule.sinTwoAngleOperator_eq_zero_of_isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (h : U ⟂ V) : U.sinTwoAngleOperator V = 0

The double-angle operator vanishes when U and V are orthogonal.

@[simp]

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

@[simp]

theorem Submodule.sinTwoAngleOperator_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinTwoAngleOperator V = 0 ↔ Commute U.starProjection V.starProjection

The double-angle operator vanishes exactly when the orthogonal projections onto U and V commute.

Principal cosines, sines and angles

In a finite-dimensional space every submodule has an orthogonal projection (Submodule.HasOrthogonalProjection.ofCompleteSpace), so the principal cosines, sines and angles take their two subspaces without that hypothesis.

noncomputable def Submodule.principalCosines {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : ℕ →₀ ℝ

The principal cosines of U and V: the singular values of the cosine map P_V P_U, in nonincreasing order and padded with zeros.

noncomputable def Submodule.principalSines {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : ℕ →₀ ℝ

The principal sines of U and V: the singular values of the directed sine map P_{Vᗮ} P_U, in nonincreasing order and padded with zeros.

noncomputable def Submodule.principalAngles {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : ℕ →₀ ℝ

The principal angles of U and V: the arcsines of the principal sines. They lie in [0, π/2] and are listed in nonincreasing order.

theorem Submodule.principalCosines_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalCosines V = (↑(U.cosThetaMap V)).singularValues

theorem Submodule.principalSines_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalSines V = (↑(U.sinThetaMap V)).singularValues

theorem Submodule.principalAngles_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalAngles V = Finsupp.mapRange Real.arcsin Real.arcsin_zero (U.principalSines V)

theorem Submodule.principalAngles_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : (U.principalAngles V) i = Real.arcsin ((U.principalSines V) i)

theorem Submodule.principalCosines_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : 0 ≤ (U.principalCosines V) i

theorem Submodule.principalSines_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : 0 ≤ (U.principalSines V) i

theorem Submodule.principalCosines_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : (U.principalCosines V) i ≤ 1

theorem Submodule.principalSines_le_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : (U.principalSines V) i ≤ 1

theorem Submodule.principalCosines_antitone {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : Antitone ⇑(U.principalCosines V)

theorem Submodule.principalSines_antitone {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : Antitone ⇑(U.principalSines V)

theorem Submodule.principalAngles_antitone {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : Antitone ⇑(U.principalAngles V)

theorem Submodule.principalAngles_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : 0 ≤ (U.principalAngles V) i

theorem Submodule.principalAngles_le_pi_div_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : (U.principalAngles V) i ≤ Real.pi / 2

@[simp]

theorem Submodule.sin_principalAngles {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) (i : ℕ) : Real.sin ((U.principalAngles V) i) = (U.principalSines V) i

The sine of the i-th principal angle is the i-th principal sine.

theorem Submodule.principalSines_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : (U.principalSines V) 0 = U.directedProjectionGap V

The largest principal sine from U to V is the directed gap ‖P_{Vᗮ} P_U‖.

theorem Submodule.forall_principalSines_lt_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) {c : ℝ} : (∀ (i : ℕ), (U.principalSines V) i < c) ↔ U.directedProjectionGap V < c

All principal sines from U to V are below c exactly when the largest one, the directed gap ‖P_{Vᗮ} P_U‖, is.

theorem Submodule.principalCosines_of_finrank_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) {i : ℕ} (hi : Module.finrank 𝕜 ↥U ≤ i) : (U.principalCosines V) i = 0

There are at most dim U nonzero principal cosines.

theorem Submodule.principalSines_of_finrank_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) {i : ℕ} (hi : Module.finrank 𝕜 ↥U ≤ i) : (U.principalSines V) i = 0

There are at most dim U nonzero principal sines.

theorem Submodule.principalAngles_of_finrank_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) {i : ℕ} (hi : Module.finrank 𝕜 ↥U ≤ i) : (U.principalAngles V) i = 0

There are at most dim U nonzero principal angles.

@[simp]

theorem Submodule.principalCosines_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalCosines V = 0 ↔ U ⟂ V

The principal cosines of U and V all vanish exactly when U and V are orthogonal.

@[simp]

theorem Submodule.principalSines_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalSines V = 0 ↔ U ≤ V

The principal sines of U and V all vanish exactly when U ≤ V.

@[simp]

theorem Submodule.principalAngles_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalAngles V = 0 ↔ U ≤ V

The principal angles of U and V all vanish exactly when U ≤ V.

@[simp]

theorem Submodule.principalSines_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U : Submodule 𝕜 E) : U.principalSines U = 0

@[simp]

theorem Submodule.principalAngles_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U : Submodule 𝕜 E) : U.principalAngles U = 0

The principal angles of a subspace with itself vanish.

theorem Submodule.principalCosines_comm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.principalCosines V = V.principalCosines U

The principal cosines are symmetric in the two subspaces.

Symmetry of the principal sines

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

Equal-rank symmetry of the principal sines. For subspaces of the same dimension, the principal sines of U and V are those of V and U.

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

Equal-rank symmetry of the principal angles. For subspaces of the same dimension, the principal angles of U and V are those of V and U.

Right principal angles

theorem Submodule.ncard_ofPred_principalAngles_eq_pi_div_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : {i : ℕ | (U.principalAngles V) i = Real.pi / 2}.ncard = Module.finrank 𝕜 ↥(U ⊓ Vᗮ)

Counting right principal angles. The number of principal angles from U to V equal to π/2 is the dimension of U ⊓ Vᗮ, the subspace of vectors of U orthogonal to V.

theorem Submodule.forall_principalAngles_lt_pi_div_two_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : (∀ (i : ℕ), (U.principalAngles V) i < Real.pi / 2) ↔ Disjoint U Vᗮ

All principal angles from U to V are strictly below π/2 exactly when no nonzero vector of U is orthogonal to V.

theorem Submodule.forall_principalAngles_lt_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) {θ : ℝ} (hθ : θ ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : (∀ (i : ℕ), (U.principalAngles V) i < θ) ↔ U.directedProjectionGap V < Real.sin θ

For a threshold θ ∈ [-π/2, π/2], all principal angles from U to V are strictly below θ exactly when the directed gap ‖P_{Vᗮ} P_U‖, the largest principal sine, is less than sin θ.

theorem Submodule.forall_principalAngles_lt_pi_div_two_iff_directedProjectionGap_lt_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : (∀ (i : ℕ), (U.principalAngles V) i < Real.pi / 2) ↔ U.directedProjectionGap V < 1

All principal angles from U to V are strictly below π/2 exactly when the directed gap ‖P_{Vᗮ} P_U‖, the largest principal sine, is less than 1.

theorem Submodule.directedProjectionGap_lt_one_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : U.directedProjectionGap V < 1 ↔ Disjoint U Vᗮ

In finite dimension, the directed gap ‖P_{Vᗮ} P_U‖ from U to V is less than 1 exactly when no nonzero vector of U is orthogonal to V.

theorem Submodule.forall_principalAngles_lt_pi_div_four_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) : (∀ (i : ℕ), (U.principalAngles V) i < Real.pi / 4) ↔ U.directedProjectionGap V < √2 / 2

All principal angles from U to V are strictly below π/4 exactly when the directed gap ‖P_{Vᗮ} P_U‖ is less than √2/2.

Angles of the range of an isometry

theorem Submodule.norm_starProjection_orthogonal_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {X : F →L[𝕜] E} (V : Submodule 𝕜 E) [V.HasOrthogonalProjection] (hX : Isometry ⇑X) [(↑X).range.HasOrthogonalProjection] : ‖Vᗮ.starProjection ∘SL X‖ = (↑X).range.directedProjectionGap V

The operator norm of the sine embedding P_{Vᗮ} X of an isometry X is the directed gap from range X to V.

theorem Submodule.principalCosines_range_eq_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {X : F →L[𝕜] E} (V : Submodule 𝕜 E) (hX : Isometry ⇑X) : (↑X).range.principalCosines V = (↑(V.starProjection ∘SL X)).singularValues

The principal cosines of the range of an isometry X and of V are the singular values of the cosine embedding P_V X.

theorem Submodule.principalSines_range_eq_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {X : F →L[𝕜] E} (V : Submodule 𝕜 E) (hX : Isometry ⇑X) : (↑X).range.principalSines V = (↑(Vᗮ.starProjection ∘SL X)).singularValues

The principal sines of the range of an isometry X and of V are the singular values of the sine embedding P_{Vᗮ} X.

Directed sine embedding of a subspace

noncomputable def Submodule.sinThetaEmbedding {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (Z U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : ↥Z →L[𝕜] E

The directed sine embedding from Z to U: orthogonally project Z onto Uᗮ, viewed as a map into the ambient space.

theorem Submodule.sinThetaEmbedding_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (Z U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Z.sinThetaEmbedding U = Uᗮ.starProjection ∘SL Z.subtypeL

The directed sine embedding is orthogonal projection onto Uᗮ composed with the inclusion of Z into E.

@[simp]

theorem Submodule.sinThetaEmbedding_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (Z U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (x : ↥Z) : (Z.sinThetaEmbedding U) x = Uᗮ.starProjection ↑x

The directed sine embedding acts by projection onto Uᗮ.

theorem Submodule.singularValues_sinThetaEmbedding {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (Z U : Submodule 𝕜 E) : (↑(Z.sinThetaEmbedding U)).singularValues = Z.principalSines U

The singular values of the directed sine embedding are the principal sines from Z to U, including the zero tail. No equality of subspace ranks is required.

theorem Submodule.adjoint_apply_leftSingularVector_starProjection_orthogonal_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (U : Submodule 𝕜 E) (X : F →ₗ[𝕜] E) {i : Fin (Module.finrank 𝕜 F)} : (LinearMap.adjoint X) ((↑Uᗮ.starProjection ∘ₗ X).leftSingularVector i) = ↑((↑Uᗮ.starProjection ∘ₗ X).singularValues ↑i) • (↑Uᗮ.starProjection ∘ₗ X).rightSingularBasis i

The ambient adjoint of the trial map acts on a sine left singular vector by the same singular relation, including at a zero singular value.

Adapted from the Kitware DKPS formalization, DavisKahan/FiniteDimensional/TanTheta/RitzResidual.lean (Jon Crall and GPT 5.6 High; Apache-2.0).

@[simp]

theorem Submodule.inner_map_sub_leftSingularVector_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (X : F →ₗᵢ[𝕜] E) (i j : Fin (Module.finrank 𝕜 F)) : inner 𝕜 (X ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).rightSingularBasis i)) ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).leftSingularVector j - ↑((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).singularValues ↑j) • X ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).rightSingularBasis j)) = 0

Each Ritz vector X vᵢ is orthogonal to the unnormalized residual direction y_j - σ_j • X v_j.

theorem Submodule.inner_sub_leftSingularVector_eq_ite {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (X : F →ₗᵢ[𝕜] E) {i j : Fin (Module.finrank 𝕜 F)} (hi : (↑Uᗮ.starProjection ∘ₗ X.toLinearMap).singularValues ↑i ≠ 0) (hj : (↑Uᗮ.starProjection ∘ₗ X.toLinearMap).singularValues ↑j ≠ 0) : inner 𝕜 ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).leftSingularVector i - ↑((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).singularValues ↑i) • X.toLinearMap ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).rightSingularBasis i)) ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).leftSingularVector j - ↑((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).singularValues ↑j) • X.toLinearMap ((↑Uᗮ.starProjection ∘ₗ X.toLinearMap).rightSingularBasis j)) = if i = j then ↑(1 - (↑Uᗮ.starProjection ∘ₗ X.toLinearMap).singularValues ↑i ^ 2) else 0

For nonzero sines, the unnormalized residual directions yᵢ - σᵢ • X vᵢ are pairwise orthogonal, with squared norm 1 - σᵢ².