Eigenvector cross-term identity for a perturbation

For symmetric operators T, S on a finite-dimensional inner product space, with u i the i-th eigenvector of T (eigenvalue λ i) and v j the j-th eigenvector of S (eigenvalue μ j),

⟪u i, (S - T) (v j)⟫ = (μ j - λ i) * ⟪u i, v j⟫.

This three-line identity is the seed of every Davis–Kahan-style subspace perturbation bound: cross terms between well-separated parts of the spectra are controlled by the perturbation S - T divided by the eigenvalue gap.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.Spectrum, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 56f7495.
• 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 Fable 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

theorem TauCeti.inner_eigenvectorBasis_map_sub_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i j : Fin n) : inner 𝕜 ((hT.eigenvectorBasis hn) i) ((S - T) ((hS.eigenvectorBasis hn) j)) = ↑(hS.eigenvalues hn j - hT.eigenvalues hn i) * inner 𝕜 ((hT.eigenvectorBasis hn) i) ((hS.eigenvectorBasis hn) j)

Cross-term identity. The matrix entry of the perturbation S - T between the i-th eigenvector of T and the j-th eigenvector of S is the eigenvalue difference times the overlap of the two eigenvectors.