Projection geometry for finite orthonormal families

Reusable projection and Parseval identities for spans of finite orthonormal subfamilies. These results are independent of Davis--Kahan perturbation theory.

theorem TauCeti.norm_sq_starProjection_add_norm_sq_sub {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (K : Submodule 𝕜 F) [K.HasOrthogonalProjection] (x : F) : ‖K.starProjection x‖ ^ 2 + ‖x - K.starProjection x‖ ^ 2 = ‖x‖ ^ 2

Pythagoras across an orthogonal projection: ‖P_K x‖² + ‖x − P_K x‖² = ‖x‖².

x splits into its projection and the complementary component, which are orthogonal, so the norms add in square. Stated for any submodule carrying an orthogonal projection.

The three bridge lemmas hold for an orthonormal family in any inner product space: the span of a finite subfamily is finite-dimensional, so it always carries an orthogonal projection (the HasOrthogonalProjection instance is automatic when the ambient space is finite-dimensional, as in the spectral-subspace application below, and is requested explicitly otherwise).

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.ProjectionGeometry, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit f44d966.
• 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, 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.

@[simp]

theorem TauCeti.Orthonormal.starProjection_span_image_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_3} {w : ι → F} (hw : Orthonormal 𝕜 w) (s : Finset ι) [(Submodule.span 𝕜 (w '' ↑s)).HasOrthogonalProjection] (x : F) : (Submodule.span 𝕜 (w '' ↑s)).starProjection x = ∑ i ∈ s, inner 𝕜 (w i) x • w i

Projection onto the span of an orthonormal subfamily. For an orthonormal family w and a finite index set s, the orthogonal projection onto span 𝕜 (w '' s) acts as x ↦ ∑ i ∈ s, ⟪w i, x⟫ • w i.

theorem TauCeti.Orthonormal.starProjection_span_image_apply_self {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_3} [DecidableEq ι] {w : ι → F} (hw : Orthonormal 𝕜 w) (s : Finset ι) [(Submodule.span 𝕜 (w '' ↑s)).HasOrthogonalProjection] (k : ι) : (Submodule.span 𝕜 (w '' ↑s)).starProjection (w k) = if k ∈ s then w k else 0

On a member w k of the orthonormal family, the projection onto span 𝕜 (w '' s) keeps it iff k ∈ s.

theorem TauCeti.Orthonormal.norm_sq_starProjection_span_image {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι : Type u_3} {w : ι → F} (hw : Orthonormal 𝕜 w) (s : Finset ι) [(Submodule.span 𝕜 (w '' ↑s)).HasOrthogonalProjection] (x : F) : ‖(Submodule.span 𝕜 (w '' ↑s)).starProjection x‖ ^ 2 = ∑ i ∈ s, ‖inner 𝕜 (w i) x‖ ^ 2

Parseval for the projection onto the span of an orthonormal subfamily: ‖P x‖² = ∑ i ∈ s, ‖⟪w i, x⟫‖².

theorem TauCeti.OrthonormalBasis.norm_sq_sub_starProjection_span_image {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {m : ℕ} (w : OrthonormalBasis (Fin m) 𝕜 F) (s : Finset (Fin m)) (x : F) : ‖x - (Submodule.span 𝕜 (⇑w '' ↑s)).starProjection x‖ ^ 2 = ∑ i ∈ sᶜ, ‖inner 𝕜 (w i) x‖ ^ 2

Complementary Parseval for a projection residual. For a subfamily of an orthonormal basis w, the residual of the projection onto its span carries the complementary Parseval sum: ‖x − P x‖² = ∑_{i ∉ s} ‖⟪w i, x⟫‖². Companion to Orthonormal.norm_sq_starProjection_span_image (‖P x‖² = ∑_{i ∈ s}); together they split Parseval ‖x‖² = ∑_i ‖⟪w i, x⟫‖² across s and its complement.

theorem TauCeti.sum_norm_sub_starProjection_span_sq_eq {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {m : ℕ} (u v : OrthonormalBasis (Fin m) 𝕜 F) (s : Finset (Fin m)) : ∑ k : Fin m, ‖((Submodule.span 𝕜 (⇑v '' ↑s)).starProjection - (Submodule.span 𝕜 (⇑u '' ↑s)).starProjection) (u k)‖ ^ 2 = 2 * ∑ i ∈ s, ∑ j ∈ sᶜ, ‖inner 𝕜 (u i) (v j)‖ ^ 2

Projector form of the Davis–Kahan identity. For two orthonormal bases u, v of a finite-dimensional inner product space over 𝕜 = ℝ, ℂ and an index set s, the squared Frobenius distance (computed in the basis u) between the orthogonal projections onto span (v '' s) and span (u '' s) is twice the cross overlap sum: ∑ₖ ‖(P_v − P_u) uₖ‖² = 2 ∑_{i ∈ s} ∑_{j ∉ s} ‖⟪uᵢ, vⱼ⟫‖².