Perturbation of Gram operators

For bounded maps A, B : E →L[𝕜] F between real or complex Hilbert spaces, the source Gram operators A† A and B† B satisfy

‖A† A - B† B‖ ≤ (‖A‖ + ‖B‖) * ‖A - B‖.

The same bound holds for the target Gram operators A A† and B B†. These estimates transfer control of a rectangular operator perturbation to its positive Gram operators, whose spectra determine the squared singular values. They apply in arbitrary dimension, including trivial source or target spaces. In finite dimension, pointwise bounds on algebraic linear maps give a corresponding pointwise Gram perturbation estimates. The target-Gram version assumes a nontrivial source to infer nonnegativity of the pointwise bounds.

The identities expose the two terms linear in the perturbation A - B. The target-space statements follow from the source-space statements by taking adjoints. The proofs use Mathlib's isometric adjoint equivalence and the submultiplicativity of the operator norm.

Provenance

The pointwise source-Gram perturbation estimate for finite-dimensional linear maps is adapted from ForTauCeti/Analysis/InnerProductSpace/Singular/Subspace.lean in the AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0), by Jon Crall and Claude Opus 4.8.

The pointwise target-Gram estimate is extracted from the left singular-vector bound adapted from YuWangSamworth2015/YuWangSamworth2015/Rectangular/Theorem4.lean in the same Kitware formalization (Jon Crall and GPT 5.6 High; Apache-2.0).

References

• G. W. Stewart and J.-G. Sun, Matrix Perturbation Theory, Academic Press (1990), Chapter I (norm estimates for matrix products).

theorem ContinuousLinearMap.adjoint_comp_self_sub_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A B : E →L[𝕜] F) : adjoint A ∘SL A - adjoint B ∘SL B = adjoint A ∘SL (A - B) + adjoint (A - B) ∘SL B

The difference of the source Gram operators is the sum of two products with the perturbation A - B.

theorem ContinuousLinearMap.self_comp_adjoint_sub_self_comp_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A B : E →L[𝕜] F) : A ∘SL adjoint A - B ∘SL adjoint B = A ∘SL adjoint (A - B) + (A - B) ∘SL adjoint B

The difference of the target Gram operators is the sum of two products with the perturbation A - B.

theorem ContinuousLinearMap.norm_adjoint_comp_self_sub_adjoint_comp_self_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A B : E →L[𝕜] F) : ‖adjoint A ∘SL A - adjoint B ∘SL B‖ ≤ (‖A‖ + ‖B‖) * ‖A - B‖

Perturbing an operator changes its source Gram operator by at most the norm of the perturbation times the sum of the two operator norms.

theorem ContinuousLinearMap.norm_self_comp_adjoint_sub_self_comp_adjoint_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A B : E →L[𝕜] F) : ‖A ∘SL adjoint A - B ∘SL adjoint B‖ ≤ (‖A‖ + ‖B‖) * ‖A - B‖

Perturbing an operator changes its target Gram operator by at most the norm of the perturbation times the sum of the two operator norms.

theorem LinearMap.norm_adjoint_comp_self_sub_adjoint_comp_self_apply_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 B : E →ₗ[𝕜] F) {a b ε : ℝ} (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (hB : ∀ (x : E), ‖B x‖ ≤ b * ‖x‖) (hAB : ∀ (x : E), ‖(A - B) x‖ ≤ ε * ‖x‖) (x : E) : ‖(adjoint A ∘ₗ A - adjoint B ∘ₗ B) x‖ ≤ (a + b) * ε * ‖x‖

Pointwise source-Gram perturbation bound. Bounds on two rectangular linear maps and on their difference imply ‖(A† A - B† B) x‖ ≤ (a + b) ε ‖x‖ for each x in the source.

theorem LinearMap.norm_self_comp_adjoint_sub_self_comp_adjoint_apply_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] [Nontrivial E] (A B : E →ₗ[𝕜] F) {a b ε : ℝ} (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (hB : ∀ (x : E), ‖B x‖ ≤ b * ‖x‖) (hAB : ∀ (x : E), ‖(A - B) x‖ ≤ ε * ‖x‖) (x : F) : ‖(A ∘ₗ adjoint A - B ∘ₗ adjoint B) x‖ ≤ (a + b) * ε * ‖x‖

Pointwise target-Gram perturbation bound. Bounds on two rectangular linear maps and on their difference imply ‖(A A† - B B†) x‖ ≤ (a + b) ε ‖x‖ for each target vector. The nontrivial source ensures that the three pointwise bounds have nonnegative constants.