Projections onto selected orthonormal-basis spans

Parseval's identity for a finite orthonormal family computes the squared norm of the projection onto a coordinate block. The complementary coordinate block spans the orthogonal complement of the selected span.

Main result

• OrthonormalBasis.norm_starProjection_orthogonal_spanIndices_sq: the complementary projection norm as a sum of squared inner products.

Source

The selected-span construction is adapted from the AIQ-Kitware DKPS formalization (ForTauCeti/Analysis/InnerProductSpace/BasisSpan.lean, Apache-2.0). This proof specializes the orthonormal-family Parseval identity.

theorem OrthonormalBasis.norm_starProjection_orthogonal_spanIndices_sq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (s : Finset ι) (x : E) : ‖(b.spanIndices ↑s)ᗮ.starProjection x‖ ^ 2 = ∑ k ∈ sᶜ, ‖inner 𝕜 (b k) x‖ ^ 2

The squared norm of the orthogonal projection onto the complement of a selected coordinate block equals the sum of squared inner products with the complementary basis vectors.