Unitarily invariant seminorms and orthogonal projections

For arbitrary linear maps H : E → F, orthogonal projections P_U on E and P_V on F, the checkerboard operator H P_U - P_V H has seminorm at most that of H. The bound holds for every unitarily invariant seminorm, without spectral-gap assumptions. Two subspace reflections yield the sharp constant one.

The sine-angle operator |P_U - P_V| and the projector difference have the same singular values and hence the same unitarily invariant seminorm.

Main results

• TauCeti.UnitarilyInvariantSeminorm.map_sinAngleOperator_eq_map_sub_starProjection: their unitarily invariant seminorms agree.
• TauCeti.UnitarilyInvariantSeminorm.map_comp_starProjection_sub_starProjection_comp_le: N (H P_U - P_V H) ≤ N H.

Provenance

Factored from the symmetric two-orientation proof adapted from ForTauCeti/Analysis/InnerProductSpace/SinTheta/Perturbation.lean in the AIQ-Kitware DKPS formalization (Apache-2.0; Jon Crall, GPT-6).

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.map_sinAngleOperator_eq_map_sub_starProjection {K : Type u_1} {E : Type u_2} [RCLike K] [NormedAddCommGroup E] [InnerProductSpace K E] [FiniteDimensional K E] [CompleteSpace E] (N : UnitarilyInvariantSeminorm K E E) (U V : Submodule K E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : N ↑(U.sinAngleOperator V) = N ↑(U.starProjection - V.starProjection)

The sine-angle operator and the projector difference have the same value in every unitarily invariant seminorm, without spectral-gap assumptions.

theorem TauCeti.UnitarilyInvariantSeminorm.map_comp_starProjection_sub_starProjection_comp_le {K : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike K] [NormedAddCommGroup E] [InnerProductSpace K E] [NormedAddCommGroup F] [InnerProductSpace K F] (N : UnitarilyInvariantSeminorm K E F) (U : Submodule K E) (V : Submodule K F) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (H : E →ₗ[K] F) : N (H ∘ₗ ↑U.starProjection - ↑V.starProjection ∘ₗ H) ≤ N H

Checkerboard contraction. For any H, the off-diagonal difference H P_U - P_V H has no larger unitarily invariant seminorm than H. No symmetry, invariance or spectral-gap hypotheses on H are needed.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_sub_starProjection_le_map_comp_sub_comp {K : Type u_1} {E : Type u_2} [RCLike K] [NormedAddCommGroup E] [InnerProductSpace K E] [FiniteDimensional K E] (N : UnitarilyInvariantSeminorm K E E) {A B : E →L[K] E} (hAB : (↑(A - B)).IsSymmetric) {U V : Submodule K E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] {delta : ℝ} (hdelta : 0 ≤ delta) (hkyUV : ∀ (k : ℕ), (↑delta • ↑Vᗮ.orthogonalProjectionOnto ∘ₗ U.subtype).kyFanSum k ≤ (↑Vᗮ.orthogonalProjectionOnto ∘ₗ ↑(B - A) ∘ₗ U.subtype).kyFanSum k) (hkyVU : ∀ (k : ℕ), (↑delta • -LinearMap.adjoint (↑Uᗮ.orthogonalProjectionOnto ∘ₗ V.subtype)).kyFanSum k ≤ (LinearMap.adjoint (↑Uᗮ.orthogonalProjectionOnto ∘ₗ ↑(A - B) ∘ₗ V.subtype)).kyFanSum k) : delta * N ↑(U.starProjection - V.starProjection) ≤ N (↑(B - A) ∘ₗ ↑U.starProjection - ↑V.starProjection ∘ₗ ↑(B - A))

Block-sum majorization turns the two directed Ky Fan bounds into the checkerboard estimate: delta * N (P_U - P_V) ≤ N ((B - A) P_U - P_V (B - A)).