The overlap operator of two finite families and their principal cosines #
For finite families u : ι → E and v : κ → E in an inner product space, the overlap operator
TauCeti.overlapOperator (defined with the frame operators in
TauCeti.Analysis.InnerProductSpace.Frame) is analysis by u after synthesis by v,
EuclideanSpace 𝕜 κ → EuclideanSpace 𝕜 ι, a ↦ (⟪uᵢ, ∑ⱼ aⱼ vⱼ⟫)ᵢ,
whose matrix in the standard coordinates is (⟪uᵢ, vⱼ⟫)ᵢⱼ. When E is finite-dimensional it is
S_u† S_v for the synthesis maps S_u, S_v; for orthonormal families these are the coordinate
isometries Orthonormal.synthesisMapIsometry, and the overlap operator records the relative
position of the two spanned subspaces in coordinates. On the diagonal it is the Gram operator.
For orthonormal families the singular values of the overlap operator are the principal cosines
cos θ₀ ≥ cos θ₁ ≥ ⋯ of the two spans (Björck–Golub): writing S_u, S_v for the coordinate
isometries, the cosine map of the spans U and V is P_V P_U = S_v (S_v† S_u) S_u†, and the
outer isometric factors do not change singular values. So these family-level cosines are the
subspace-level Submodule.principalCosines U V; for two unit vectors the single principal cosine
of the lines they span is ‖⟪u, v⟫‖. Defining them as singular values makes
nonnegativity, ordering and symmetry instances of the singular-value API rather than separate
arguments; the bound cos θₖ ≤ 1 comes from the overlap operator being a contraction. The sum of
their squares is the squared Frobenius norm ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖² of the overlap matrix, which gives
the squared Frobenius sine sin²_F Θ = ∑ₖ (1 - cos² θₖ) of two families of the same size as
d - ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖². Equivalently, sin²_F Θ = ∑ⱼ ‖P_{Uᗮ} vⱼ‖² is the total squared
distance of the vⱼ from the span U of the uᵢ. When the uᵢ are the members of an orthonormal
basis (bₖ) indexed by a coordinate block s, P_{Uᗮ} is the projection onto the span of the
complementary block, which gives the cross-block form sin²_F Θ = ∑ⱼ ∑_{k ∉ s} ‖⟪bₖ, vⱼ⟫‖².
For two eigenbases of symmetric operators and a common index block, this expresses the Frobenius
sine between corresponding eigenspaces through the overlaps of eigenvectors across the blocks.
The overlap operator and its Frobenius identity make sense for arbitrary finite families; the principal cosines and the squared Frobenius sine are defined only for orthonormal families.
Main declarations #
TauCeti.norm_overlapOperator_apply_le: for orthonormal families it is a contraction.TauCeti.sum_sq_singularValues_overlapOperator:∑ₖ σₖ² = ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖².TauCeti.cosPrincipalAngles: the principal cosines of two orthonormal families, as singular values of the overlap operator, withcosPrincipalAngles_nonneg,cosPrincipalAngles_le_one,cosPrincipalAngles_antitoneandcosPrincipalAngles_comm.Orthonormal.principalCosines_eq_cosPrincipalAngles: the principal cosines of the spans of two orthonormal families are the principal cosines of the families.Submodule.principalCosines_span_singleton: for unit vectorsuandv, the principal cosines of𝕜 ∙ uand𝕜 ∙ vare‖⟪u, v⟫‖followed by zeros.TauCeti.sinThetaSq: the squared Frobenius sine of two orthonormal families, withTauCeti.sinThetaSq_eq_card_sub_sum_norm_inner_sqandTauCeti.sinThetaSq_self.TauCeti.sinThetaSq_eq_sum_norm_starProjection_orthogonal_sq:sin²_F Θ = ∑ⱼ ‖P_{Uᗮ} vⱼ‖².Submodule.sq_sinThetaFrobenius_eq_sinThetaSq_of_orthonormal: for arbitrary finite orthonormal families the squared subspace Frobenius sine equalsTauCeti.sinThetaSq.OrthonormalBasis.sq_sinThetaFrobenius_spanIndices: the cross-overlap formula for independently indexed orthonormal-basis blocks.TauCeti.sinThetaSq_comp_subtypeVal_eq_sum_compl_norm_inner_sqandTauCeti.sinThetaSq_comp_subtypeVal_comp_subtypeVal_eq_sum_compl_norm_inner_sq: the cross-block form of the squared Frobenius sine for coordinate blocks of orthonormal bases.
Provenance #
The cross-block Frobenius sine identity is adapted from the AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0) and the canonical eigenblock bridge. The remaining overlap identities are TauCeti developments.
References #
- Å. Björck and G. H. Golub, Numerical methods for computing angles between linear subspaces, Math. Comp. 27 (1973), 579–594.
- G. H. Golub and C. F. Van Loan, Matrix Computations, fourth edition, Johns Hopkins University Press, 2013, Section 6.4.3.
- Y. Yu, T. Wang and R. J. Samworth, A useful variant of the Davis–Kahan theorem for statisticians, Biometrika 102 (2015), 315–323.
Contraction and Frobenius identity #
The overlap operator of two orthonormal families is a contraction.
Frobenius identity for the overlap operator: the squared singular values of the overlap
operator sum to the squared Frobenius norm ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖² of its matrix.
Principal cosines #
The principal cosines of orthonormal finite families u and v: the singular values of their
overlap operator, in nonincreasing order and padded by zeros. These are the cosines of the
principal angles between the two spans. For arbitrary families, the singular values of the overlap
operator are (overlapOperator 𝕜 u v).singularValues.
Instances For
The principal cosines are nonnegative.
The principal cosines form a nonincreasing sequence cos θ₀ ≥ cos θ₁ ≥ ⋯.
Swapping the two families leaves the principal cosines unchanged.
There are at most as many nonzero principal cosines as members of the second family.
There are at most as many nonzero principal cosines as members of the first family.
The principal cosines are at most 1.
The squared principal cosines are at most 1, so each term 1 - cos² θₖ of the squared
Frobenius sine is nonnegative.
The squares of the principal cosines sum to the squared Frobenius norm ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖² of
the overlap matrix.
The sum of the first n principal cosines is the n-th Ky Fan sum of the overlap operator.
The squared Frobenius sine #
The squared Frobenius sine sin²_F Θ = ∑ₖ (1 - cos² θₖ) between the spans of two orthonormal
families of the same size d, summed over their first d principal cosines.
Instances For
For orthonormal families of size d, sin²_F Θ = d - ∑ₖ cos² θₖ.
For orthonormal families of size d, sin²_F Θ = d - ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖², the size minus the
squared Frobenius norm of the overlap matrix: the squared Frobenius sine between the spans,
computed directly from the inner products.
Swapping the two families leaves the squared Frobenius sine unchanged.
The squared Frobenius sine is nonnegative.
An orthonormal family makes no angle with itself: its squared Frobenius sine vanishes.
All d principal cosines of an orthonormal family of size d with itself equal 1.
The squared Frobenius sine through projections and coordinate blocks #
The squared Frobenius sine is the total squared distance of the second family from the span
U of the first: sin²_F Θ = ∑ⱼ ‖P_{Uᗮ} vⱼ‖².
Cross-block form of the squared Frobenius sine. Let u be the members of an orthonormal
basis b indexed by a coordinate block s, and let v be any orthonormal family indexed by s.
Then sin²_F Θ = ∑ⱼ ∑_{k ∉ s} ‖⟪bₖ, vⱼ⟫‖²: the squared Frobenius sine is the energy of the vⱼ in
the complementary coordinates.
Eigenblock sine formula. For two orthonormal bases b and c and a common coordinate block
s, the squared Frobenius sine between the blocks (bᵢ)_{i ∈ s} and (cⱼ)_{j ∈ s} is the
cross-block sum ∑_{j ∈ s} ∑_{k ∉ s} ‖⟪bₖ, cⱼ⟫‖². Applied to eigenbases of two symmetric operators,
this compares the eigenspaces selected by the same eigenvalue indices.
The squared Frobenius sine of the spans of equally indexed orthonormal
families is their family-level squared Frobenius sine TauCeti.sinThetaSq.
The order reflects the directed projection P_{Uᗮ} P_V.
For independently indexed coordinate blocks of two orthonormal bases, the squared
Frobenius sine is the cross-block overlap sum over the selected vectors of b
and the complementary vectors of a. The two blocks need not have equal cardinality.
Principal cosines of the spans #
Family/subspace cosine bridge. The principal cosines of the spans U and V of two finite
orthonormal families, the singular values of P_V P_U, are the principal cosines of the families,
the singular values of their overlap operator.
One-dimensional cosine formula. For unit vectors u and v, the only principal cosine of
the lines 𝕜 ∙ u and 𝕜 ∙ v is ‖⟪u, v⟫‖.