Coordinate isometries of orthonormal families

The synthesis map of an orthonormal family is an isometry from Euclidean coefficient space into the ambient inner-product space. Its coordinate formula and action on the standard basis make the identified finite-dimensional subspace directly usable in operator constructions. In the other direction, Bessel's inequality makes the analysis map of an orthonormal family a contraction.

The orthogonal projection onto the span of a finite orthonormal family is x ↦ ∑ᵢ ⟪vᵢ, x⟫ vᵢ, synthesis after analysis, that is, the frame operator of the family. So Bessel's inequality becomes an equality on the span: ‖P x‖² = ∑ᵢ ‖⟪vᵢ, x⟫‖².

Combining an orthonormal family with the rows of a matrix A gives an orthonormal family exactly when A * Aᴴ = 1 (Orthonormal.orthonormal_sum_smul_iff); for square matrices this identifies the changes of orthonormal frame with the unitary group.

noncomputable def Orthonormal.synthesisMapIsometry {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) : EuclideanSpace 𝕜 ι →ₗᵢ[𝕜] E

The synthesis map of an orthonormal family is a linear isometry from Euclidean coefficient space into its ambient inner-product space.

@[simp]

theorem Orthonormal.synthesisMapIsometry_toLinearMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) : hv.synthesisMapIsometry.toLinearMap = TauCeti.synthesisMap 𝕜 v

The underlying linear map of the coordinate isometry is the synthesis map.

@[simp]

theorem Orthonormal.synthesisMapIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (a : EuclideanSpace 𝕜 ι) : hv.synthesisMapIsometry a = ∑ i : ι, a.ofLp i • v i

The coordinate isometry sends a coefficient vector to the corresponding linear combination of the orthonormal family.

@[simp]

theorem Orthonormal.synthesisMapIsometry_single {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (i : ι) (c : 𝕜) : hv.synthesisMapIsometry (EuclideanSpace.single i c) = c • v i

The coordinate isometry sends the single-coordinate vector supported at i with coefficient c to c • v i.

theorem Orthonormal.range_synthesisMapIsometry {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) : hv.synthesisMapIsometry.range = Submodule.span 𝕜 (Set.range v)

The range of the coordinate synthesis isometry is the span of the orthonormal family.

@[simp]

theorem Orthonormal.adjoint_synthesisMapIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} [CompleteSpace E] (hv : Orthonormal 𝕜 v) (y : E) (i : ι) : ((ContinuousLinearMap.adjoint hv.synthesisMapIsometry.toContinuousLinearMap) y).ofLp i = inner 𝕜 (v i) y

The adjoint of the coordinate synthesis isometry reads inner products with the family.

theorem Orthonormal.norm_analysisMap_le {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (x : E) : ‖(TauCeti.analysisMap 𝕜 v) x‖ ≤ ‖x‖

Bessel's inequality for the analysis map of an orthonormal family: the coefficient vector (⟪vᵢ, x⟫)ᵢ has norm at most ‖x‖.

theorem Orthonormal.starProjection_apply_eq_sum {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Submodule.span 𝕜 (Set.range v) = U) (x : E) : U.starProjection x = ∑ i : ι, inner 𝕜 (v i) x • v i

The orthogonal projection onto the span U of a finite orthonormal family is x ↦ ∑ᵢ ⟪vᵢ, x⟫ vᵢ.

theorem Orthonormal.toLinearMap_starProjection_eq_frameOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Submodule.span 𝕜 (Set.range v) = U) : ↑U.starProjection = TauCeti.frameOperator 𝕜 v

The orthogonal projection onto the span U of a finite orthonormal family is its frame operator, synthesis after analysis.

theorem Orthonormal.norm_starProjection_sq_eq_sum {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Submodule.span 𝕜 (Set.range v) = U) (x : E) : ‖U.starProjection x‖ ^ 2 = ∑ i : ι, ‖inner 𝕜 (v i) x‖ ^ 2

Parseval's identity on the span U of a finite orthonormal family: the orthogonal projection of x onto U has squared norm ∑ᵢ ‖⟪vᵢ, x⟫‖².

theorem Orthonormal.orthonormal_sum_smul_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} {κ : Type u_4} [DecidableEq κ] (hv : Orthonormal 𝕜 v) (A : Matrix κ ι 𝕜) : (Orthonormal 𝕜 fun (j : κ) => ∑ i : ι, A j i • v i) ↔ A * A.conjTranspose = 1

Taking combinations of an orthonormal family with the rows of a matrix A produces an orthonormal family exactly when A has orthonormal rows, that is, A * Aᴴ = 1. For a square matrix this says that A is unitary.

@[simp]

theorem OrthonormalBasis.synthesisMapIsometry_orthonormal {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : ⋯.synthesisMapIsometry = b.repr.symm.toLinearIsometry

The synthesis isometry of an orthonormal basis is the inverse of its coordinate map.