Gram-operator perturbation

For A, Â : E →ₗ[𝕜] F between finite-dimensional inner product spaces, the singular subspaces are the spectral subspaces of the Gram operators A⋆A and Â⋆Â. The Yu–Wang–Samworth singular-vector bound applies the symmetric result to these Gram operators, so it needs the Gram perturbation Â⋆Â − A⋆A bounded in terms of  − A.

Main results

• TauCeti.norm_adjoint_apply_le: the adjoint of a c-bounded operator is c-bounded (‖A⋆‖ ≤ ‖A‖ in elementwise form).
• TauCeti.norm_gram_sub_gram_apply_le: ‖(Â⋆Â − A⋆A) x‖ ≤ (a + â) ε ‖x‖ when A, Â, Â − A are a-, â-, ε-bounded, via Â⋆Â − A⋆A = Â⋆(Â − A) + (Â − A)⋆A.
• TauCeti.abs_sq_singularValues_sub_le: Weyl for squared singular values, |σₖ(Â)² − σₖ(A)²| ≤ (a + â) ε — the singular-value stability underlying the singular-subspace bound.
• TauCeti.sum_sq_singularValues: the squared Frobenius norm equals the sum of squared singular values, ∑ᵢ σᵢ(A)² = ∑ₖ ‖A bₖ‖².
• TauCeti.eigenvalues_conj_unitary: the sorted eigenvalues of a symmetric operator are invariant under unitary conjugation S ↦ U S U⁻¹.

References

• Y. Yu, T. Wang, R. J. Samworth, A useful variant of the Davis–Kahan theorem for statisticians, Biometrika 102 (2015), §"singular-vector extension".

theorem TauCeti.norm_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] {A : E →ₗ[𝕜] F} {c : ℝ} (hc : 0 ≤ c) (h : ∀ (x : E), ‖A x‖ ≤ c * ‖x‖) (y : F) : ‖(LinearMap.adjoint A) y‖ ≤ c * ‖y‖

The adjoint preserves an operator-norm bound. If ‖A x‖ ≤ c ‖x‖ for all x, then ‖A⋆ y‖ ≤ c ‖y‖ for all y — the elementwise form of ‖A⋆‖ = ‖A‖. Proof: ‖A⋆ y‖² = re⟪y, A (A⋆ y)⟫ ≤ ‖y‖ ‖A (A⋆ y)‖ ≤ c ‖y‖ ‖A⋆ y‖.

theorem TauCeti.norm_gram_sub_gram_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  : E →ₗ[𝕜] F} {a â ε : ℝ} (hâ : 0 ≤ â) (hε : 0 ≤ ε) (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (h : ∀ (x : E), ‖ x‖ ≤ â * ‖x‖) (hE : ∀ (x : E), ‖( - A) x‖ ≤ ε * ‖x‖) (x : E) : ‖(LinearMap.adjoint  ∘ₗ  - LinearMap.adjoint A ∘ₗ A) x‖ ≤ (a + â) * ε * ‖x‖

Gram-operator perturbation bound. With A, Â, Â − A bounded by a, â, ε respectively, ‖(Â⋆Â − A⋆A) x‖ ≤ (a + â) ε ‖x‖. From the splitting Â⋆Â − A⋆A = Â⋆(Â − A) + (Â − A)⋆A, the two pieces are bounded by â ε and ε a (using norm_adjoint_apply_le).

theorem TauCeti.sum_re_inner_abs_self_eq_sum_singularValues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) : ∑ k : Fin n, RCLike.re (inner 𝕜 ((operatorAbs A) (b k)) (b k)) = ∑ i : Fin n, A.singularValues ↑i

Trace of the modulus = sum of singular values. For an endomorphism A : E →ₗ[𝕜] E, ∑ₖ re⟪|A| bₖ, bₖ⟫ = ∑ᵢ σᵢ(A) in any orthonormal basis b. The modulus |A| = √(A⋆A) is diagonal in the A⋆A-eigenbasis with entries √λᵢ(A⋆A) = σᵢ(A), and the trace is basis-independent.

theorem TauCeti.singularValues_le_one_of_contraction {𝕜 : 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 →ₗ[𝕜] F} (h : ∀ (x : E), ‖A x‖ ≤ ‖x‖) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n) : A.singularValues ↑i ≤ 1

Contraction ⇒ singular values ≤ 1. If A is a contraction (‖A x‖ ≤ ‖x‖), then every singular value satisfies σᵢ(A) ≤ 1. Each eigenvalue λᵢ(A⋆A) = re⟪A wᵢ, A wᵢ⟫ = ‖A wᵢ‖² ≤ 1 (wᵢ the unit eigenvector), and σᵢ = √λᵢ.

theorem TauCeti.sum_sq_singularValues {𝕜 : 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 →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) : ∑ i : Fin n, A.singularValues ↑i ^ 2 = ∑ k : Fin n, ‖A (b k)‖ ^ 2

Squared Frobenius norm = sum of squared singular values. For any orthonormal basis b of E, ∑ᵢ σᵢ(A)² = ∑ₖ ‖A bₖ‖². Via the dictionary σᵢ² = λᵢ(A⋆A), basis independence of the trace, and re⟪bₖ, A⋆A bₖ⟫ = ‖A bₖ‖².

theorem TauCeti.sum_sq_norm_le_sum_re_inner_abs_of_contraction {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (h : ∀ (x : E), ‖A x‖ ≤ ‖x‖) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) : ∑ k : Fin n, ‖A (b k)‖ ^ 2 ≤ ∑ k : Fin n, RCLike.re (inner 𝕜 ((operatorAbs A) (b k)) (b k))

Frobenius² ≤ trace of the modulus, for a contraction. If A : E →ₗ[𝕜] E is a contraction, then ∑ₖ ‖A bₖ‖² ≤ ∑ₖ re⟪|A| bₖ, bₖ⟫, i.e. ∑ σᵢ² ≤ ∑ σᵢ (each σᵢ ∈ [0, 1]). This is the core inequality of the aligned-basis (orthogonal-Procrustes) argument: ∑‖wⱼ − uⱼ‖² = 2d − 2∑σ ≤ 2d − 2∑σ² = 2·sinΘ².

theorem TauCeti.sum_sq_norm_apply_unitary_comp {𝕜 : 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 →ₗ[𝕜] F) (U : E ≃ₗᵢ[𝕜] E) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (b : OrthonormalBasis (Fin n) 𝕜 E) : ∑ k : Fin n, ‖A (U (b k))‖ ^ 2 = ∑ k : Fin n, ‖A (b k)‖ ^ 2

Unitary invariance of the Frobenius sum. Pre-composing with a unitary U does not change ∑ₖ ‖A (b k)‖²: ∑ₖ ‖A (U bₖ)‖² = ∑ₖ ‖A bₖ‖². Both equal the sum of squared singular values (sum_sq_singularValues), since k ↦ U bₖ is another orthonormal basis.

theorem TauCeti.abs_sq_singularValues_sub_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 →ₗ[𝕜] F} {a â ε : ℝ} (hâ : 0 ≤ â) (hε : 0 ≤ ε) (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (h : ∀ (x : E), ‖ x‖ ≤ â * ‖x‖) (hE : ∀ (x : E), ‖( - A) x‖ ≤ ε * ‖x‖) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (k : Fin n) : |Â.singularValues ↑k ^ 2 - A.singularValues ↑k ^ 2| ≤ (a + â) * ε

Gram-transported Weyl bound for squared singular values. The k-th squared singular values of A and Â differ by at most the Gram perturbation bound: |σₖ(Â)² − σₖ(A)²| ≤ (a + â) ε. Via the dictionary σₖ² = λₖ(·⋆·) (sq_singularValues_fin) and Weyl's inequality on the Gram operators, fed by the perturbation bound norm_gram_sub_gram_apply_le.

This is weaker than Weyl's inequality for singular values, in three ways, and the name is deliberately not "Weyl's inequality" on that account: it bounds the squares, its constant carries the extra factor a + â so the bound degrades with the size of the operators, and it needs the auxiliary hypotheses hA, hÂ that the genuine theorem does not. The sharp form is ContinuousLinearMap.abs_singularValues_sub_singularValues_le (ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/FiniteDimensional.lean), |σₙ(T) − σₙ(S)| ≤ ‖T − S‖, which implies this one but not conversely — dividing back out by σₖ(A) + σₖ(Â) recovers nothing when the singular values are small. This version survives because it is the shape the Gram-side arguments produce.

Extreme singular values: variational characterization

The largest singular value is the operator norm and the smallest is the minimum gain, both attained. These are the quantitative inputs for the operator-norm principal-angle identification.

theorem TauCeti.singularValues_last_mul_norm_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] {n : ℕ} (A : E →ₗ[𝕜] F) (hn : Module.finrank 𝕜 E = n) (hn0 : 0 < n) (x : E) : A.singularValues (n - 1) * ‖x‖ ≤ ‖A x‖

The smallest singular value is a lower bound for the gain: σ_{n-1}(A) * ‖x‖ ≤ ‖A x‖.

theorem TauCeti.exists_norm_apply_eq_singularValues_last {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {n : ℕ} (A : E →ₗ[𝕜] F) (hn : Module.finrank 𝕜 E = n) (hn0 : 0 < n) : ∃ (x : E), ‖x‖ = 1 ∧ ‖A x‖ = A.singularValues (n - 1)

The smallest singular value is attained.

theorem TauCeti.norm_apply_le_singularValues_zero_mul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {n : ℕ} (A : E →ₗ[𝕜] F) (hn : Module.finrank 𝕜 E = n) (hn0 : 0 < n) (x : E) : ‖A x‖ ≤ A.singularValues 0 * ‖x‖

The largest singular value bounds the gain: ‖A x‖ ≤ σ₀(A) * ‖x‖ (the elementwise form of σ₀ = ‖A‖).

theorem TauCeti.exists_norm_apply_eq_singularValues_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {n : ℕ} (A : E →ₗ[𝕜] F) (hn : Module.finrank 𝕜 E = n) (hn0 : 0 < n) : ∃ (x : E), ‖x‖ = 1 ∧ ‖A x‖ = A.singularValues 0

The largest singular value is attained.

Singular values of the adjoint (square case)

σ(A⋆) = σ(A) for a square operator A : E →ₗ[𝕜] E. The Gram operators A⋆A and A A⋆ are unitarily conjugate (A A⋆ = U (A⋆A) U⁻¹ with U = choosePolarUnitary A), so they have equal sorted eigenvalues, hence A and A⋆ have equal singular values. This is the symmetry cosPrincipalAngles needs (plan step W0.1(d)).

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.SingularSubspace, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 29506b0.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Opus 4.8; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

theorem TauCeti.isSymmetric_conj_unitary {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (U : E ≃ₗᵢ[𝕜] E) : (↑U.toLinearEquiv ∘ₗ S ∘ₗ ↑U.symm.toLinearEquiv).IsSymmetric

The conjugate U S U⁻¹ of a symmetric operator by a unitary is symmetric.

theorem TauCeti.eigenvalues_conj_unitary {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {S : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (U : E ≃ₗᵢ[𝕜] E) : ⋯.eigenvalues hn = hS.eigenvalues hn

Unitary conjugation preserves sorted eigenvalues. For a symmetric operator S and a unitary U, S and U S U⁻¹ have the same sorted eigenvalues. (Courant–Fischer: the Rayleigh minimax is invariant under the subspace bijection V ↦ U V.)

theorem TauCeti.comp_adjoint_eq_conj_adjoint_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) : A ∘ₗ LinearMap.adjoint A = ↑(choosePolarUnitary A).toLinearEquiv ∘ₗ (LinearMap.adjoint A ∘ₗ A) ∘ₗ ↑(choosePolarUnitary A).symm.toLinearEquiv

The Gram operators A A⋆ and A⋆A are unitarily conjugate: A A⋆ = U (A⋆A) U⁻¹ with U = choosePolarUnitary A. From A = U |A|, A⋆ = |A| U⁻¹, so A A⋆ = U |A|² U⁻¹ = U (A⋆A) U⁻¹.

theorem TauCeti.eigenvalues_gram_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (A : E →ₗ[𝕜] E) (hn : Module.finrank 𝕜 E = n) : ⋯.eigenvalues hn = ⋯.eigenvalues hn

The Gram operators of A and A⋆ have equal sorted eigenvalues.