The Sylvester operator: dimension-free bounds and the finite-dimensional equation

For bounded operators A : E →L[𝕜] E and B : F →L[𝕜] F, the Sylvester operator A.sylvester B sends X : F →L[𝕜] E to A ∘L X - X ∘L B. The Sylvester equation A X - X B = C is the linear equation through which spectral gaps control the motion of spectral subspaces under perturbation (Davis–Kahan, Bhatia–Davis–McIntosh).

Quadratic-form separation bounds solutions in operator norm, in every dimension. If re ⟪A x, x⟫ ≥ α ‖x‖² and re ⟪B y, y⟫ ≥ β ‖y‖², then (α + β) ‖X‖ ≤ ‖A X + X B‖; this needs neither symmetry, completeness nor finite dimension. Taking α = β = δ > 0 gives the Lyapunov bound ‖X‖ ≤ ‖A X + X B‖ / (2 δ). Replacing B by -B gives the separated Sylvester bound: if the form of A is at least c + g and that of B at most c, then g ‖X‖ ≤ ‖A X - X B‖. The reverse orientation follows in the same way. The proof evaluates the equation on unit vectors v with ‖X v‖ close to ‖X‖. For such v, the Cauchy–Schwarz inequality for the positive semidefinite form ‖X‖² ⟪·, ·⟫ - ⟪X ·, X ·⟫ (ContinuousLinearMap.sq_opNorm_sq_mul_re_inner_sub_re_inner_le) makes re ⟪X (B v), X v⟫ close to ‖X‖² re ⟪B v, v⟫.

When A is symmetric, the equation diagonalises on eigenvectors: if A u = α u and B v = β v with α real and β : 𝕜, then ⟪u, (A X - X B) v⟫ = (α - β) ⟪u, X v⟫. Only E needs an inner product for this identity. Dually, when B is symmetric, the rank-one operator formed from eigenvectors of A and B has Sylvester eigenvalue α - β; here only F needs an inner product, and α : 𝕜 may be arbitrary. In finite dimension, choosing orthonormal eigenbases (uᵢ) of A and (vⱼ) of B turns the equation into the scalar equations (αᵢ - βⱼ) Xᵢⱼ = Cᵢⱼ on the matrix coefficients Xᵢⱼ = ⟪uᵢ, X vⱼ⟫. If no eigenvalue of A is an eigenvalue of B, every αᵢ - βⱼ is nonzero, so the Sylvester operator is bijective and the unique solution is obtained by dividing each coefficient of C by the corresponding eigenvalue difference.

The spectral hypothesis is phrased as disjointness of the real point spectra Module.End.restrictedPointSpectrum A ⊤ and Module.End.restrictedPointSpectrum B ⊤. A positive separation Module.End.PointSpectraSeparated A ⊤ B ⊤ δ with 0 < δ supplies it through Module.End.PointSpectraSeparated.disjoint.

Main definitions

• ContinuousLinearMap.sylvester A B: the continuous linear map X ↦ A ∘L X - X ∘L B on F →L[𝕜] E.

Main statements

• ContinuousLinearMap.sub_smul_one_sylvester_sub_smul_one: the Sylvester operator is unchanged when A and B are shifted by the same scalar.
• ContinuousLinearMap.add_mul_norm_le_norm_comp_add_comp: if the forms of A and B are bounded below by α and β, then (α + β) ‖X‖ ≤ ‖A X + X B‖.
• ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le, ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_re_inner_le_of_le_re_inner: if the forms of A and B are separated by g, in either order, then g ‖X‖ ≤ ‖A X - X B‖.
• ContinuousLinearMap.inner_sylvester_apply_of_apply_eq_smul: for symmetric A and eigenvectors A u = α u, B v = β v, ⟪u, A.sylvester B X v⟫ = (α - β) ⟪u, X v⟫.
• ContinuousLinearMap.sylvester_rankOne_of_apply_eq_smul: for symmetric B and eigenvectors A u = α u, B v = β v, the Sylvester operator acts on rankOne 𝕜 u v as the scalar α - β.
• ContinuousLinearMap.inner_sylvester_apply_eigenvectorBasis: the same identity on the matrix coefficients in ordered eigenbases.
• ContinuousLinearMap.sylvester_injective: in finite dimension, for symmetric A and B with disjoint point spectra, the Sylvester operator is injective.
• ContinuousLinearMap.sylvester_sum_eigenvectorBasis: under the same hypotheses, dividing the eigenbasis coefficients of C by the eigenvalue differences gives a solution of A X - X B = C.
• ContinuousLinearMap.sylvester_bijective, ContinuousLinearMap.sylvester_apply_eq_iff: the Sylvester operator is bijective, and that coefficient formula gives the unique solution.

References

• J. J. Sylvester, Sur l'équation en matrices px = xq, C. R. Acad. Sci. Paris 99 (1884).
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §VII.2.
• R. Bhatia, C. Davis, A. McIntosh, Perturbation of spectral subspaces and solution of linear operator equations, Linear Algebra Appl. 52/53 (1983), 45–67.

noncomputable def ContinuousLinearMap.sylvester {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (A : E →L[𝕜] E) (B : F →L[𝕜] F) : (F →L[𝕜] E) →L[𝕜] F →L[𝕜] E

The Sylvester operator of A : E →L[𝕜] E and B : F →L[𝕜] F: the continuous linear map X ↦ A ∘L X - X ∘L B on F →L[𝕜] E. Its equation A.sylvester B X = C is the Sylvester equation A X - X B = C, and its kernel consists of the intertwiners A X = X B.

@[simp]

theorem ContinuousLinearMap.sylvester_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (A : E →L[𝕜] E) (B : F →L[𝕜] F) (X : F →L[𝕜] E) : (A.sylvester B) X = A ∘SL X - X ∘SL B

@[simp]

theorem ContinuousLinearMap.sub_smul_one_sylvester_sub_smul_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (A : E →L[𝕜] E) (B : F →L[𝕜] F) (c : 𝕜) : (A - c • 1).sylvester (B - c • 1) = A.sylvester B

The Sylvester operator is unchanged when both operators are shifted by the same scalar: (A - c) X - X (B - c) = A X - X B.

theorem ContinuousLinearMap.add_mul_norm_le_norm_comp_add_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {α β : ℝ} (hA : ∀ (x : E), α * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hB : ∀ (y : F), β * ‖y‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B y) y)) (X : F →L[𝕜] E) : (α + β) * ‖X‖ ≤ ‖A ∘SL X + X ∘SL B‖

The coercivity bound for A X + X B. If the real parts of the quadratic forms of A and B are bounded below by α and β, then (α + β) ‖X‖ ≤ ‖A X + X B‖ for every bounded operator X. Neither symmetry of A and B, completeness, nor finite dimension is assumed, and α, β may have any sign. The codomain E may be seminormed. For α = β = δ > 0 this is the Lyapunov bound: every solution of A X + X B = Y satisfies ‖X‖ ≤ ‖Y‖ / (2 δ).

theorem ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {c g : ℝ} (hA : ∀ (x : E), (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) (hB : ∀ (y : F), RCLike.re (inner 𝕜 (B y) y) ≤ c * ‖y‖ ^ 2) (X : F →L[𝕜] E) : g * ‖X‖ ≤ ‖(A.sylvester B) X‖

The separated Sylvester bound. If the real part of the quadratic form of A is at least c + g and that of B is at most c, then g ‖X‖ ≤ ‖A X - X B‖ for every bounded operator X. For g > 0, every solution of A X - X B = Y therefore satisfies ‖X‖ ≤ ‖Y‖ / g.

theorem ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_re_inner_le_of_le_re_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {c g : ℝ} (hA : ∀ (x : E), RCLike.re (inner 𝕜 (A x) x) ≤ c * ‖x‖ ^ 2) (hB : ∀ (y : F), (c + g) * ‖y‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B y) y)) (X : F →L[𝕜] E) : g * ‖X‖ ≤ ‖(A.sylvester B) X‖

The reverse separated Sylvester bound. If the real part of the quadratic form of A is at most c and that of B is at least c + g, then g ‖X‖ ≤ ‖A X - X B‖ for every bounded operator X. For g > 0, every solution of A X - X B = Y therefore satisfies ‖X‖ ≤ ‖Y‖ / g.

theorem ContinuousLinearMap.inner_sylvester_apply_of_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 E] [NormedSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} (hA : (↑A).IsSymmetric) (X : F →L[𝕜] E) {α : ℝ} {β : 𝕜} {u : E} {v : F} (hu : A u = ↑α • u) (hv : B v = β • v) : inner 𝕜 u (((A.sylvester B) X) v) = (↑α - β) * inner 𝕜 u (X v)

The Sylvester equation on eigenvectors. If A is symmetric, A u = α u and B v = β v with α real and β : 𝕜, then the coefficient of A X - X B between v and u is α - β times that of X. Only the space containing u needs an inner product.

theorem ContinuousLinearMap.sylvester_rankOne_of_apply_eq_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} (hB : (↑B).IsSymmetric) {α : 𝕜} {β : ℝ} {u : E} {v : F} (hu : A u = α • u) (hv : B v = ↑β • v) : (A.sylvester B) (((InnerProductSpace.rankOne 𝕜) u) v) = (α - ↑β) • ((InnerProductSpace.rankOne 𝕜) u) v

The Sylvester operator on rank-one operators. If B is symmetric, A u = α u and B v = β v with α : 𝕜 and β real, then the Sylvester operator acts on rankOne 𝕜 u v : x ↦ ⟪v, x⟫ u as the scalar α - β. Only the space containing v needs an inner product.

theorem ContinuousLinearMap.inner_sylvester_apply_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n m : ℕ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hn : Module.finrank 𝕜 E = n) (hm : Module.finrank 𝕜 F = m) (X : F →L[𝕜] E) (i : Fin n) (j : Fin m) : inner 𝕜 ((hA.eigenvectorBasis hn) i) (((A.sylvester B) X) ((hB.eigenvectorBasis hm) j)) = ↑(hA.eigenvalues hn i - hB.eigenvalues hm j) * inner 𝕜 ((hA.eigenvectorBasis hn) i) (X ((hB.eigenvectorBasis hm) j))

The Sylvester equation in eigenbases. For symmetric A and B with ordered orthonormal eigenbases (uᵢ), (vⱼ) and eigenvalues (αᵢ), (βⱼ), the matrix coefficients of C = A X - X B are Cᵢⱼ = (αᵢ - βⱼ) Xᵢⱼ, where Xᵢⱼ = ⟪uᵢ, X vⱼ⟫.

theorem ContinuousLinearMap.inner_eigenvectorBasis_apply_eq_inv_mul_inner_sylvester_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n m : ℕ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hn : Module.finrank 𝕜 E = n) (hm : Module.finrank 𝕜 F = m) (X : F →L[𝕜] E) (i : Fin n) (j : Fin m) (hij : hA.eigenvalues hn i - hB.eigenvalues hm j ≠ 0) : inner 𝕜 ((hA.eigenvectorBasis hn) i) (X ((hB.eigenvectorBasis hm) j)) = ↑(hA.eigenvalues hn i - hB.eigenvalues hm j)⁻¹ * inner 𝕜 ((hA.eigenvectorBasis hn) i) (((A.sylvester B) X) ((hB.eigenvectorBasis hm) j))

The solved form of the Sylvester equation in eigenbases. For symmetric A and B, the matrix coefficient Xᵢⱼ = ⟪uᵢ, X vⱼ⟫ is (αᵢ - βⱼ)⁻¹ times the coefficient Cᵢⱼ of C = A X - X B, provided αᵢ ≠ βⱼ.

theorem ContinuousLinearMap.sylvester_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Disjoint (Module.End.restrictedPointSpectrum ↑A ⊤) (Module.End.restrictedPointSpectrum ↑B ⊤)) : Function.Injective ⇑(A.sylvester B)

Uniqueness for the Sylvester equation. In finite dimension, if A and B are symmetric and no real eigenvalue of A is an eigenvalue of B, the Sylvester operator X ↦ A X - X B is injective.

theorem ContinuousLinearMap.sylvester_sum_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n m : ℕ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hn : Module.finrank 𝕜 E = n) (hm : Module.finrank 𝕜 F = m) (h : Disjoint (Module.End.restrictedPointSpectrum ↑A ⊤) (Module.End.restrictedPointSpectrum ↑B ⊤)) (C : F →L[𝕜] E) : (A.sylvester B) (∑ i : Fin n, ∑ j : Fin m, (↑(hA.eigenvalues hn i - hB.eigenvalues hm j)⁻¹ * inner 𝕜 ((hA.eigenvectorBasis hn) i) (C ((hB.eigenvectorBasis hm) j))) • ((InnerProductSpace.rankOne 𝕜) ((hA.eigenvectorBasis hn) i)) ((hB.eigenvectorBasis hm) j)) = C

The canonical solution of the Sylvester equation. In finite dimension, let A and B be symmetric with ordered orthonormal eigenbases (uᵢ), (vⱼ) and eigenvalues (αᵢ), (βⱼ), and suppose no real eigenvalue of A is an eigenvalue of B. Then the operator whose coefficients are ⟪uᵢ, C vⱼ⟫ / (αᵢ - βⱼ), namely the sum of (αᵢ - βⱼ)⁻¹ ⟪uᵢ, C vⱼ⟫ times the rank-one operators rankOne 𝕜 uᵢ vⱼ : x ↦ ⟪vⱼ, x⟫ uᵢ, solves A X - X B = C.

theorem ContinuousLinearMap.sylvester_bijective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (h : Disjoint (Module.End.restrictedPointSpectrum ↑A ⊤) (Module.End.restrictedPointSpectrum ↑B ⊤)) : Function.Bijective ⇑(A.sylvester B)

Bijectivity of the Sylvester operator. In finite dimension, if A and B are symmetric and no real eigenvalue of A is an eigenvalue of B, then for every C the Sylvester equation A X - X B = C has exactly one solution.

theorem ContinuousLinearMap.sylvester_apply_eq_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n m : ℕ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hn : Module.finrank 𝕜 E = n) (hm : Module.finrank 𝕜 F = m) (h : Disjoint (Module.End.restrictedPointSpectrum ↑A ⊤) (Module.End.restrictedPointSpectrum ↑B ⊤)) {X C : F →L[𝕜] E} : (A.sylvester B) X = C ↔ X = ∑ i : Fin n, ∑ j : Fin m, (↑(hA.eigenvalues hn i - hB.eigenvalues hm j)⁻¹ * inner 𝕜 ((hA.eigenvectorBasis hn) i) (C ((hB.eigenvectorBasis hm) j))) • ((InnerProductSpace.rankOne 𝕜) ((hA.eigenvectorBasis hn) i)) ((hB.eigenvectorBasis hm) j)

The solution of the Sylvester equation. In finite dimension, if A and B are symmetric and no real eigenvalue of A is an eigenvalue of B, then X solves A X - X B = C exactly when its coefficients in ordered orthonormal eigenbases (uᵢ), (vⱼ) of A and B are ⟪uᵢ, C vⱼ⟫ / (αᵢ - βⱼ).