Population-gap bounds for right and left singular vectors

For rectangular maps A and Â, bounds with constants a, â, and ε on A, Â, and  - A control the cross-block overlap of their right singular bases: Γ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, v̂ⱼ⟫|² ≤ 4 |s| ((a + â) ε)². The theorem is stated in multiplied form, which also covers Γ = 0.

The separation is imposed only on the squared singular values of the population operator. No gap is required for the perturbed operator, and the index block need not be contiguous.

The same estimate holds for the eigenbases of the target Gram operators A A† and  †, including their zero eigenspaces.

The pointwise bound for A† A is available in TauCeti.Analysis.InnerProductSpace.Gram.Perturbation.

Provenance

Adapted from the maintained AIQ-Kitware DKPS formalization (Apache-2.0):

• ForTauCeti/Analysis/InnerProductSpace/Singular/Subspace.lean (original Gram perturbation reduction, Jon Crall and Claude Opus 4.8).
• YuWangSamworth2015/YuWangSamworth2015/Core/SingularSubspace.lean (singular-vector population bound, Jon Crall and GPT 5.6 High).

References

• Y. Yu, T. Wang and R. J. Samworth, A useful variant of the Davis--Kahan theorem for statisticians, Biometrika 102 (2015), 315--323.

theorem LinearMap.sq_mul_sum_sum_norm_inner_rightSingularBasis_sq_le_four_mul_card_mul_sq {𝕜 : 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 ≤ Γ) (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (h : ∀ (x : E), ‖ x‖ ≤ â * ‖x‖) (hE : ∀ (x : E), ‖( - A) x‖ ≤ ε * ‖x‖) (s : Finset (Fin (Module.finrank 𝕜 E))) (hgap : ∀ j ∈ s, ∀ k ∉ s, Γ ≤ |A.singularValues ↑j ^ 2 - A.singularValues ↑k ^ 2|) : Γ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 (A.rightSingularBasis k) (Â.rightSingularBasis j)‖ ^ 2 ≤ 4 * ↑s.card * ((a + â) * ε) ^ 2

Yu–Wang–Samworth bound for right singular vectors. A population gap in squared singular values gives Γ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, v̂ⱼ⟫|² ≤ 4 |s| ((a + â) ε)², where vₖ and v̂ⱼ belong to the right singular bases of A and Â. Only the population squared singular values need a gap.

theorem LinearMap.sq_mul_sum_sum_norm_inner_self_comp_adjoint_eigenvectorBasis_sq_le_four_mul_card_mul_sq {𝕜 : 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 ≤ Γ) (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (h : ∀ (x : E), ‖ x‖ ≤ â * ‖x‖) (hE : ∀ (x : E), ‖( - A) x‖ ≤ ε * ‖x‖) (s : Finset (Fin (Module.finrank 𝕜 F))) (hgap : ∀ j ∈ s, ∀ k ∉ s, Γ ≤ |⋯.eigenvalues ⋯ j - ⋯.eigenvalues ⋯ k|) : Γ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((⋯.eigenvectorBasis ⋯) k) ((⋯.eigenvectorBasis ⋯) j)‖ ^ 2 ≤ 4 * ↑s.card * ((a + â) * ε) ^ 2

Yu–Wang–Samworth bound for left singular vectors. A population gap in the eigenvalues of the target Gram operator gives the same cross-block bound as for right singular vectors. The eigenbases of A A† and  † include complete bases of the kernels, so no positive-rank assumption is needed.

Adapted by target-Gram duality from the left-singular population bound in YuWangSamworth2015/YuWangSamworth2015/Rectangular/Theorem4.lean in the Kitware DKPS formalization (Jon Crall and GPT 5.6 High; Apache-2.0).