Directed Frobenius sine between subspaces

For subspaces U and V of a finite-dimensional inner product space, the Frobenius sine U.sinThetaFrobenius V is the Frobenius seminorm of the directed sine map P_{Vᗮ} P_U. It packages the quantity used in Frobenius subspace perturbation inequalities without selecting bases. The quantity is not generally symmetric and vanishes exactly when U ≤ V, so it is not a distance on arbitrary subspaces.

The Frobenius sine is the square root of the sum of the squared principal sines. The operator norm of the directed sine map sees only the largest principal sine; the Frobenius quantity accounts for all of them.

For a finite orthonormal family spanning U, the squared Frobenius sine from U to V equals the sum of squared norms of projections onto Vᗮ.

Main results

• OrthonormalBasis.sq_sinThetaFrobenius_spanIndices_eq_sum_projection: the squared Frobenius sine from a selected basis block to an arbitrary subspace.
• Submodule.sq_sinThetaFrobenius_eq_sum_projection_of_orthonormal: the squared Frobenius sine expressed through any orthonormal spanning family.

Source

• AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0): https://github.com/AIQ-Kitware/aiq-dkps-formalization
• Source file: ForTauCeti/Analysis/InnerProductSpace/SinTheta/Frobenius.lean.

noncomputable def Submodule.sinThetaFrobenius {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : ℝ

The Frobenius seminorm of the directed sine map between two subspaces.

theorem Submodule.sinThetaFrobenius_def {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinThetaFrobenius V = (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E E) ↑(U.sinThetaMap V)

The Frobenius sine is the Frobenius seminorm of the directed sine map P_{Vᗮ} P_U.

theorem Submodule.sinThetaFrobenius_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : 0 ≤ U.sinThetaFrobenius V

The Frobenius sine is nonnegative.

theorem Submodule.sinThetaFrobenius_eq_sqrt_sum_sq_principalSines {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinThetaFrobenius V = √((U.principalSines V).sum fun (x : ℕ) (s : ℝ) => s ^ 2)

The Frobenius sine is the Euclidean norm of the principal-sine list.

theorem Submodule.sq_sinThetaFrobenius {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.sinThetaFrobenius V ^ 2 = (U.principalSines V).sum fun (x : ℕ) (s : ℝ) => s ^ 2

The squared Frobenius sine equals the sum of the squared principal sines.

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

The Frobenius sine is symmetric for subspaces of equal finite dimension.

theorem Submodule.directedProjectionGap_le_sinThetaFrobenius {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.directedProjectionGap V ≤ U.sinThetaFrobenius V

The directed projection gap is bounded by the Frobenius sine.

@[simp]

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

The Frobenius sine vanishes precisely when the first subspace is contained in the second.

@[simp]

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

The Frobenius sine from a subspace to itself is zero.

Projection formula for the squared Frobenius sine

theorem OrthonormalBasis.sq_sinThetaFrobenius_spanIndices_eq_sum_projection {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (s : Finset ι) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : (b.spanIndices ↑s).sinThetaFrobenius U ^ 2 = ∑ j ∈ s, ‖Uᗮ.starProjection (b j)‖ ^ 2

For an arbitrary target subspace U, the squared Frobenius sine from a coordinate block of an orthonormal basis b to U is the total squared orthogonal projection of the selected vectors onto Uᗮ.

theorem Submodule.sq_sinThetaFrobenius_eq_sum_projection_of_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (V U : Submodule 𝕜 E) [V.HasOrthogonalProjection] [U.HasOrthogonalProjection] {κ : Type u_3} [Fintype κ] {v : κ → E} (hv : Orthonormal 𝕜 v) (hV : span 𝕜 (Set.range v) = V) : V.sinThetaFrobenius U ^ 2 = ∑ j : κ, ‖Uᗮ.starProjection (v j)‖ ^ 2

For any finite orthonormal family spanning V, the squared Frobenius sine from V to U is the sum of the squared orthogonal projections of its vectors onto Uᗮ. In particular, the value does not depend on the chosen family.