Documentation

TauCeti.Analysis.InnerProductSpace.YuWangSamworth.Basic

Population-gap residual bounds for corresponding eigenblocks #

Let T (the population operator) and S (its perturbation) be symmetric endomorphisms of an n-dimensional inner product space over ℝ or ℂ, with decreasingly ordered eigenvalues λ₀ ≥ ⋯ ≥ λₙ₋₁ of T, μ₀ ≥ ⋯ ≥ μₙ₋₁ of S, and orthonormal eigenbases (vₖ) of T and (uⱼ) of S. Fix an index block s. The Yu–Wang–Samworth variant of the Davis–Kahan theorem measures the motion of the eigenblock (uⱼ)_{j ∈ s} away from (vⱼ)_{j ∈ s} by the cross-block overlap ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, uⱼ⟫|², which is the squared Frobenius sine of the angles between the two eigenblocks. Unlike the classical theorem, its gap hypothesis is placed on the population spectrum alone: Δ ≤ |λⱼ - λₖ| for j ∈ s and k ∉ s.

The argument runs through the residual columns Rⱼ = λⱼ uⱼ - T uⱼ, which pair a population eigenvalue with a perturbed eigenvector, and sandwiches ∑_{j ∈ s} ‖Rⱼ‖² between the overlap and the size of S - T.

Combining the two sides bounds Δ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, uⱼ⟫|² by both 4 ‖S - T‖_F² and 4 |s| ε², with no gap assumed in the spectrum of S.

Main statements #

References #

The lower residual bound #

theorem LinearMap.IsSymmetric.norm_smul_sub_apply_sq_eq_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (c : ℝ) (x : E) :
‖↑c • x - T x‖ ^ 2 = ∑ k : Fin n, (c - hT.eigenvalues hn k) ^ 2 * ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) x‖ ^ 2

Eigenbasis expansion of a shifted residual. For symmetric T with eigenvalues λₖ and orthonormal eigenbasis (vₖ), every real c and vector x satisfy ‖c x - T x‖² = ∑ₖ (c - λₖ)² |⟪vₖ, x⟫|².

theorem LinearMap.IsSymmetric.sq_mul_sum_norm_inner_sq_le_norm_smul_sub_apply_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {c Δ : ℝ} (hΔ : 0 ≤ Δ) {t : Finset (Fin n)} (hgap : ∀ k ∈ t, Δ ≤ |c - hT.eigenvalues hn k|) (x : E) :
Δ ^ 2 * ∑ k ∈ t, ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) x‖ ^ 2 ≤ ‖↑c • x - T x‖ ^ 2

Gap bound for one shifted residual. If c is at distance at least Δ ≥ 0 from every eigenvalue λₖ of T with k ∈ t, then Δ² ∑_{k ∈ t} |⟪vₖ, x⟫|² ≤ ‖c x - T x‖².

theorem LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_sum_norm_smul_sub_apply_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {Δ : ℝ} (hΔ : 0 ≤ Δ) {s : Finset (Fin n)} (hgap : ∀ j ∈ s, ∀ k ∉ s, Δ ≤ |hT.eigenvalues hn j - hT.eigenvalues hn k|) (w : Fin n → E) :
Δ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) (w j)‖ ^ 2 ≤ ∑ j ∈ s, ‖↑(hT.eigenvalues hn j) • w j - T (w j)‖ ^ 2

The lower residual bound. Let Δ ≥ 0 separate the eigenvalues of T indexed by s from the remaining ones. Then for every family (wⱼ), the residuals λⱼ wⱼ - T wⱼ bound the overlap of the wⱼ with the complementary eigenvectors: Δ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, wⱼ⟫|² ≤ ∑_{j ∈ s} ‖λⱼ wⱼ - T wⱼ‖².

The upper residual bounds #

theorem LinearMap.IsSymmetric.smul_sub_apply_eigenvectorBasis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (c : ℝ) (j : Fin n) :
↑c • (hS.eigenvectorBasis hn) j - T ((hS.eigenvectorBasis hn) j) = ↑(c - hS.eigenvalues hn j) • (hS.eigenvectorBasis hn) j + (S - T) ((hS.eigenvectorBasis hn) j)

The residual decomposition. For an eigenvector uⱼ of S with eigenvalue μⱼ and any real c, c uⱼ - T uⱼ = (c - μⱼ) uⱼ + (S - T) uⱼ: an eigenvalue displacement plus the perturbation applied to uⱼ.

theorem LinearMap.IsSymmetric.norm_smul_sub_apply_eigenvectorBasis_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (c : ℝ) (j : Fin n) :
‖↑c • (hS.eigenvectorBasis hn) j - T ((hS.eigenvectorBasis hn) j)‖ ≤ |c - hS.eigenvalues hn j| + ‖(S - T) ((hS.eigenvectorBasis hn) j)‖

The residual norm bound. For an eigenvector uⱼ of S with eigenvalue μⱼ and any real c, ‖c uⱼ - T uⱼ‖ ≤ |c - μⱼ| + ‖(S - T) uⱼ‖.

theorem LinearMap.IsSymmetric.sum_norm_smul_sub_apply_eigenvectorBasis_sq_le_four_mul_frobenius_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (s : Finset (Fin n)) :
∑ j ∈ s, ‖↑(hT.eigenvalues hn j) • (hS.eigenvectorBasis hn) j - T ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤ 4 * (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E E) (S - T) ^ 2

The Frobenius upper residual bound. The residuals Rⱼ = λⱼ(T) uⱼ - T uⱼ of the eigenvectors uⱼ of S satisfy ∑_{j ∈ s} ‖Rⱼ‖² ≤ 4 ‖S - T‖_F² for every index block s.

theorem LinearMap.IsSymmetric.sum_norm_smul_sub_apply_eigenvectorBasis_sq_le_four_mul_card_mul_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {ε : ℝ} (hε : ∀ (x : E), ‖(S - T) x‖ ≤ ε * ‖x‖) (s : Finset (Fin n)) :
∑ j ∈ s, ‖↑(hT.eigenvalues hn j) • (hS.eigenvectorBasis hn) j - T ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤ 4 * ↑s.card * ε ^ 2

The operator-norm upper residual bound. If ‖(S - T) x‖ ≤ ε ‖x‖ for every x, then the residuals Rⱼ = λⱼ(T) uⱼ - T uⱼ of the eigenvectors uⱼ of S satisfy ∑_{j ∈ s} ‖Rⱼ‖² ≤ 4 |s| ε² for every index block s.

The population-gap overlap bounds #

theorem LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_frobenius_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {Δ : ℝ} (hΔ : 0 ≤ Δ) {s : Finset (Fin n)} (hgap : ∀ j ∈ s, ∀ k ∉ s, Δ ≤ |hT.eigenvalues hn j - hT.eigenvalues hn k|) :
Δ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤ 4 * (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E E) (S - T) ^ 2

The Yu–Wang–Samworth overlap bound, Frobenius form. If Δ ≥ 0 separates the eigenvalues of the population operator T indexed by s from the remaining ones, then the eigenvectors uⱼ of the perturbation S satisfy Δ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, uⱼ⟫|² ≤ 4 ‖S - T‖_F². No gap is assumed in the spectrum of S.

theorem LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_card_mul_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {Δ : ℝ} (hΔ : 0 ≤ Δ) {s : Finset (Fin n)} (hgap : ∀ j ∈ s, ∀ k ∉ s, Δ ≤ |hT.eigenvalues hn j - hT.eigenvalues hn k|) {ε : ℝ} (hε : ∀ (x : E), ‖(S - T) x‖ ≤ ε * ‖x‖) :
Δ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤ 4 * ↑s.card * ε ^ 2

The Yu–Wang–Samworth overlap bound, operator-norm form. If Δ ≥ 0 separates the eigenvalues of the population operator T indexed by s from the remaining ones and ‖(S - T) x‖ ≤ ε ‖x‖ for every x, then the eigenvectors uⱼ of the perturbation S satisfy Δ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, uⱼ⟫|² ≤ 4 |s| ε². No gap is assumed in the spectrum of S.