Documentation

TauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Sylvester.Pairwise

The pairwise Sylvester bound in unitarily invariant seminorms #

Let A and B be symmetric operators on finite-dimensional inner product spaces E and F, over ℝ or ℂ, and suppose that every eigenvalue of A is at distance at least δ > 0 from every eigenvalue of B. No ordering or interval structure of the two spectra is assumed. This file proves that every solution of the Sylvester equation A X - X B = C satisfies

δ N(X) ≤ (π / 2) N(C)

for every unitarily invariant seminorm N. The estimate is first proved simultaneously for all Ky Fan sums, δ Kₖ(X) ≤ (π / 2) Kₖ(C); equivalently, (2 δ / π) X lies in the convex hull of the two-sided unitary orbit of C, and Fan dominance turns this into the bound for every N.

The integral representation #

The constant π / 2 is the mass ∫ |r| = π / 2 of the real Haagerup–Zsidó kernel r, which inverts the variable outside the unit interval: ∫ r(t) sin (x t) dt = 1 / x for |x| ≥ 1 (TauCeti.HaagerupZsido.integral_realKernel_mul_sin). In orthonormal eigenbases with A eᵢ = αᵢ eᵢ and B fⱼ = βⱼ fⱼ, the coefficients of the solution are ⟪eᵢ, X fⱼ⟫ = ⟪eᵢ, C fⱼ⟫ / (αᵢ - βⱼ), and |αᵢ - βⱼ| ≥ δ, so

⟪eᵢ, X fⱼ⟫ = δ⁻¹ ∫ r(t) sin ((αᵢ - βⱼ) t / δ) ⟪eᵢ, C fⱼ⟫ dt.

Expanding sin (a - b) = sin a cos b - cos a sin b, for orthonormal families (uₗ) and (vₗ) the sum ∑ₗ ⟪uₗ, X vₗ⟫ becomes δ⁻¹ ∫ r(t) g(t) dt, where

g(t) = ∑ₗ (⟪sin (t A / δ) uₗ, C cos (t B / δ) vₗ⟫ - ⟪cos (t A / δ) uₗ, C sin (t B / δ) vₗ⟫)

is built from the functional calculi of A and B. Since sin² + cos² = 1, Ky Fan's maximum principle for pairs of contractions (LinearMap.norm_sum_inner_add_inner_le_kyFanSum) gives ‖g(t)‖ ≤ Kₖ(C) whenever there are at most k vectors in each family, and the variational characterization of the Ky Fan sums yields δ Kₖ(X) ≤ (π / 2) Kₖ(C). Working with the real kernel and the sine and cosine of A and B keeps the argument inside the scalar field, so no complexification is needed over ℝ.

Separation on invariant subspaces #

The separation hypothesis may also be restricted to subspaces: if S is invariant under A, T invariant under B, X takes values in S and vanishes on Tᗮ, and the eigenvalues of A on S are at distance at least δ from those of B on T, the same bound holds. Replacing A by r on Sᗮ and B by -r on Tᗮ, with r = ‖A‖ + ‖B‖ + δ, changes neither A X nor X B, and the new scalar eigenvalues are at distance at least δ from every other eigenvalue, so the bound on the whole spaces applies to the two reduced extensions. This is the form consumed by the pairwise sin Θ theorem, where X is a product of orthogonal projections.

Main statements #

References #

theorem ContinuousLinearMap.mul_kyFanSum_le_pi_div_two_mul_kyFanSum_sylvester_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Module.End.PointSpectraSeparated ↑A ⊤ ↑B ⊤ δ) (X : F →L[𝕜] E) (k : ℕ) :
δ * (↑X).kyFanSum k ≤ Real.pi / 2 * (↑((A.sylvester B) X)).kyFanSum k

The simultaneous Ky Fan estimate for the Sylvester equation. Let A and B be symmetric operators on finite-dimensional inner product spaces. If every eigenvalue of A is at distance at least δ from every eigenvalue of B, then for every k the Ky Fan k-sums satisfy δ Kₖ(X) ≤ (π / 2) Kₖ(A X - X B). In particular every solution of the Sylvester equation A X - X B = C satisfies δ Kₖ(X) ≤ (π / 2) Kₖ(C) for all k at once.

theorem ContinuousLinearMap.smul_mem_twoSidedUnitaryOrbitHull_sylvester_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Module.End.PointSpectraSeparated ↑A ⊤ ↑B ⊤ δ) (hδ : 0 ≤ δ) (X : F →L[𝕜] E) :
↑(2 * δ / Real.pi) • ↑X ∈ (↑((A.sylvester B) X)).twoSidedUnitaryOrbitHull

The unitary-orbit form of the pairwise Sylvester bound. Let A and B be symmetric operators on finite-dimensional inner product spaces. If every eigenvalue of A is at distance at least δ ≥ 0 from every eigenvalue of B, then (2 δ / π) X lies in the convex hull of the two-sided unitary orbit {U (A X - X B) V} of A X - X B.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ} (N : UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Module.End.PointSpectraSeparated ↑A ⊤ ↑B ⊤ δ) (X : F →L[𝕜] E) :
δ * N ↑X ≤ Real.pi / 2 * N ↑((A.sylvester B) X)

The pairwise Sylvester bound. Let A and B be symmetric operators on finite-dimensional inner product spaces. If every eigenvalue of A is at distance at least δ from every eigenvalue of B, then δ N(X) ≤ (π / 2) N(A X - X B) for every unitarily invariant seminorm N. In particular every solution of the Sylvester equation A X - X B = C satisfies δ N(X) ≤ (π / 2) N(C).

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_pi_div_two_mul_map_sylvester_apply_of_mem {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ} (N : UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) {S : Submodule 𝕜 E} {T : Submodule 𝕜 F} (hS : ∀ x ∈ S, A x ∈ S) (hT : ∀ y ∈ T, B y ∈ T) (h : Module.End.PointSpectraSeparated (↑A) S (↑B) T δ) {X : F →L[𝕜] E} (hXS : ∀ (y : F), X y ∈ S) (hXT : ∀ y ∈ Tᗮ, X y = 0) :
δ * N ↑X ≤ Real.pi / 2 * N ↑((A.sylvester B) X)

The pairwise Sylvester bound on invariant subspaces. Let A and B be symmetric operators on finite-dimensional inner product spaces, let S be invariant under A and T invariant under B, and let X take values in S and vanish on Tᗮ. If every eigenvalue of A on S is at distance at least δ from every eigenvalue of B on T, then δ N(X) ≤ (π / 2) N(A X - X B) for every unitarily invariant seminorm N.