Documentation

TauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Sylvester.Basic

Unitarily invariant bounds for the Sylvester equation #

This file bounds solutions of the Sylvester equation A X - X B = C in unitarily invariant seminorms, for operators on finite-dimensional inner product spaces.

The Frobenius bound #

Let A and B be symmetric operators on finite-dimensional inner product spaces E and F, with orthonormal eigenbases (uᵢ), (vⱼ) and eigenvalues (αᵢ), (βⱼ). The Sylvester operator X ↦ A X - X B multiplies the matrix coefficient Xᵢⱼ = ⟪uᵢ, X vⱼ⟫ by αᵢ - βⱼ, so the Frobenius seminorm of A X - X B is

‖A X - X B‖_F² = ∑ᵢ ∑ⱼ (αᵢ - βⱼ)² ‖Xᵢⱼ‖².

If the spectra of A and B are at distance at least δ, every factor (αᵢ - βⱼ)² is at least δ², and therefore δ ‖X‖_F ≤ ‖A X - X B‖_F. Equivalently, every solution of the Sylvester equation A X - X B = C satisfies δ ‖X‖_F ≤ ‖C‖_F. For the Frobenius seminorm the constant is 1; the corresponding bound for a general unitarily invariant seminorm under the same pairwise separation hypothesis carries the constant π / 2 (see TauCeti.Analysis.InnerProductSpace.UnitarilyInvariantSeminorm.Sylvester.Pairwise).

The interval/exterior bound #

If the spectrum of A lies in the interval [a, b] and that of B outside (a - δ, b + δ), then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N, again with constant 1; the same holds with the roles of A and B exchanged. With centre c = (a + b) / 2 and radius r = (b - a) / 2, for symmetric A and B the hypothesis gives ‖(A - c) x‖ ≤ r ‖x‖ and (r + δ) ‖y‖ ≤ ‖(B - c) y‖. Since A X - X B = (A - c) X - X (B - c), the ideal inequality N((A - c) X) ≤ r N(X) and its reverse (r + δ) N(X) ≤ N(X (B - c)) give (r + δ) N(X) ≤ r N(X) + N(A X - X B). This argument needs neither symmetry nor a real centre, so it is stated first for an arbitrary centre c : 𝕜 and norm bounds of this shape.

The spectral hypotheses 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 lie in [a, b] while those of B on T lie outside (a - δ, b + δ), the same bound holds. On the left only the values of X matter; on the right the symmetry of B lets the bounds along T pass through the adjoint of X. This is the form consumed by the sin Θ theorems, where X is a product of orthogonal projections.

Main statements #

In the namespace TauCeti.UnitarilyInvariantSeminorm:

References #

theorem ContinuousLinearMap.sq_frobenius_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 m : ℕ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hn : Module.finrank 𝕜 E = n) (hm : Module.finrank 𝕜 F = m) (X : F →L[𝕜] E) :
(TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 F E) ↑((A.sylvester B) X) ^ 2 = ∑ i : Fin n, ∑ j : Fin m, (hA.eigenvalues hn i - hB.eigenvalues hm j) ^ 2 * ‖inner 𝕜 ((hA.eigenvectorBasis hn) i) (X ((hB.eigenvectorBasis hm) j))‖ ^ 2

The Frobenius seminorm of A X - X B in eigenbases. For symmetric A and B with ordered orthonormal eigenbases (uᵢ), (vⱼ) and eigenvalues (αᵢ), (βⱼ), ‖A X - X B‖_F² = ∑ᵢ ∑ⱼ (αᵢ - βⱼ)² ‖⟪uᵢ, X vⱼ⟫‖².

theorem ContinuousLinearMap.mul_frobenius_le_frobenius_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) :

The Frobenius Sylvester bound. In finite dimension, if A and B are symmetric and every eigenvalue of A is at distance at least δ from every eigenvalue of B, then δ ‖X‖_F ≤ ‖A X - X B‖_F for every X. In particular every solution of the Sylvester equation A X - X B = C satisfies δ ‖X‖_F ≤ ‖C‖_F.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_norm_sub_smul_le_of_le_norm_sub_smul {𝕜 : 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} {c : 𝕜} {r δ : ℝ} (N : UnitarilyInvariantSeminorm 𝕜 F E) (hA : ∀ (x : E), ‖A x - c • x‖ ≤ r * ‖x‖) (hB : ∀ (y : F), (r + δ) * ‖y‖ ≤ ‖B y - c • y‖) (X : F →L[𝕜] E) :
δ * N ↑X ≤ N ↑((A.sylvester B) X)

Sylvester bound from a disc and the exterior of a larger disc. If ‖A x - c x‖ ≤ r ‖x‖ for every x and (r + δ) ‖y‖ ≤ ‖B y - c y‖ for every y, then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_le_norm_sub_smul_of_norm_sub_smul_le {𝕜 : 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} {c : 𝕜} {r δ : ℝ} (N : UnitarilyInvariantSeminorm 𝕜 F E) (hA : ∀ (x : E), (r + δ) * ‖x‖ ≤ ‖A x - c • x‖) (hB : ∀ (y : F), ‖B y - c • y‖ ≤ r * ‖y‖) (X : F →L[𝕜] E) :
δ * N ↑X ≤ N ↑((A.sylvester B) X)

Sylvester bound from the exterior of a disc and a smaller disc. If (r + δ) ‖x‖ ≤ ‖A x - c x‖ for every x and ‖B y - c y‖ ≤ r ‖y‖ for every y, then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_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} {a b δ : ℝ} (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.PointIntervalExteriorGap (↑A) S (↑B) T a b δ) {X : F →L[𝕜] E} (hXS : ∀ (y : F), X y ∈ S) (hXT : ∀ y ∈ Tᗮ, X y = 0) :
δ * N ↑X ≤ N ↑((A.sylvester B) X)

The interval/exterior 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 the eigenvalues of A on S lie in [a, b] and those of B on T outside (a - δ, b + δ), then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap_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} {a b δ : ℝ} (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.PointIntervalExteriorGap (↑B) T (↑A) S a b δ) {X : F →L[𝕜] E} (hXS : ∀ (y : F), X y ∈ S) (hXT : ∀ y ∈ Tᗮ, X y = 0) :
δ * N ↑X ≤ N ↑((A.sylvester B) X)

The interval/exterior Sylvester bound on invariant subspaces, reversed orientation. 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 the eigenvalues of B on T lie in [a, b] and those of A on S outside (a - δ, b + δ), then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N.

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap {𝕜 : 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} {a b δ : ℝ} (N : UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Module.End.PointIntervalExteriorGap ↑A ⊤ ↑B ⊤ a b δ) (X : F →L[𝕜] E) :
δ * N ↑X ≤ N ↑((A.sylvester B) X)

The interval/exterior Sylvester bound. Let A and B be symmetric operators on finite-dimensional inner product spaces. If the eigenvalues of A lie in [a, b] and those of B outside (a - δ, b + δ), then δ N(X) ≤ 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) ≤ N(C).

theorem TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap {𝕜 : 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} {a b δ : ℝ} (N : UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Module.End.PointIntervalExteriorGap ↑B ⊤ ↑A ⊤ a b δ) (X : F →L[𝕜] E) :
δ * N ↑X ≤ N ↑((A.sylvester B) X)

The interval/exterior Sylvester bound, reversed orientation. Let A and B be symmetric operators on finite-dimensional inner product spaces. If the eigenvalues of B lie in [a, b] and those of A outside (a - δ, b + δ), then δ N(X) ≤ 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) ≤ N(C).