Finite frames: analysis, synthesis, frame and Gram operators

A finite family v : ι → E in an inner product space sits between E and the coefficient space EuclideanSpace 𝕜 ι through two maps:

• the analysis map x ↦ (⟪vᵢ, x⟫)ᵢ, from E to coefficient space;
• the synthesis map a ↦ ∑ᵢ aᵢ vᵢ, from coefficient space to E.

They are adjoint to each other. Composing them in the two orders gives the frame operator x ↦ ∑ᵢ ⟪vᵢ, x⟫ vᵢ on E and the Gram operator on coefficient space, whose matrix is Mathlib's Gram matrix Matrix.gram 𝕜 v. Both are positive. They record the same quadratic data on opposite carriers: the frame operator's form is x ↦ ∑ᵢ ‖⟪vᵢ, x⟫‖², and since the two operators are A† A and A A† for the analysis map A, their sorted eigenvalues agree through the smaller dimension (LinearMap.eigenvalues_adjoint_comp_self_eq_eigenvalues_self_comp_adjoint).

This turns lower frame bounds into Gram-spectrum bounds and back: the inequality a ‖x‖² ≤ ∑ᵢ ‖⟪vᵢ, x⟫‖² for all x holds exactly when the sorted Gram eigenvalues below finrank 𝕜 E are at least a, provided the family has at least finrank 𝕜 E members.

For two finite families u and v, analysis by u after synthesis by v is their overlap operator, whose matrix is (⟪uᵢ, vⱼ⟫)ᵢⱼ; on the diagonal it is the Gram operator.

A Parseval frame is a family whose frame operator is the identity. Its analysis map is an isometry and its synthesis map a contraction. A weighted decomposition ∑ᵢ cᵢ ⟪uᵢ, x⟫ uᵢ = x with nonnegative weights, such as the contact-point decomposition of John's theorem, makes √cᵢ • uᵢ a Parseval frame, which gives the synthesis bound ‖∑ᵢ cᵢ bᵢ uᵢ‖ ≤ (∑ᵢ cᵢ ‖bᵢ‖²)^(1/2).

The definitions and the algebraic identities need no finiteness of E; the comparisons with adjoints and eigenvalues assume E finite-dimensional.

Main declarations

• TauCeti.analysisMap, TauCeti.synthesisMap: the analysis and synthesis maps of a family.
• TauCeti.inner_synthesisMap_left, TauCeti.adjoint_analysisMap: synthesis is the adjoint of analysis.
• TauCeti.linearIndependent_iff_injective_synthesisMap: synthesis is injective exactly for a linearly independent family.
• TauCeti.bijective_synthesisMap: synthesis is bijective for a linearly independent spanning family.
• TauCeti.bilinearComp_synthesisMap_eq_sum: a bilinear form read through synthesis, expanded in coordinates.
• TauCeti.frameOperator, TauCeti.gramOperator: the frame and Gram operators.
• TauCeti.gramOperator_eq_toEuclideanLin_gram: the Gram operator is the Gram matrix acting on coefficient space.
• TauCeti.overlapOperator: the overlap operator a ↦ (⟪uᵢ, ∑ⱼ aⱼ vⱼ⟫)ᵢ of two families, with matrix (⟪uᵢ, vⱼ⟫)ᵢⱼ (TauCeti.overlapOperator_eq_toEuclideanLin); swapping the families gives the adjoint (TauCeti.adjoint_overlapOperator), and it is S_u† S_v (TauCeti.adjoint_synthesisMap_comp_synthesisMap).
• TauCeti.isPositive_frameOperator, TauCeti.isPositive_gramOperator: both are positive.
• OrthonormalBasis.frameOperator_eq_id: an orthonormal basis has the identity as frame operator.
• OrthonormalBasis.synthesisMap_eq_repr_symm: the synthesis map of an orthonormal basis is the inverse of its coordinate map.
• TauCeti.norm_analysisMap_sq: ‖analysis x‖² = ∑ᵢ ‖⟪vᵢ, x⟫‖².
• TauCeti.norm_analysisMap_of_frameOperator_eq_id, TauCeti.norm_synthesisMap_le_of_frameOperator_eq_id: for a Parseval frame, analysis is an isometry and synthesis a contraction.
• TauCeti.frameOperator_sqrt_smul_eq_id: a weighted decomposition of the identity gives a Parseval frame.
• TauCeti.norm_sum_mul_smul_le_sqrt, TauCeti.norm_sum_mul_smul_le_sqrt_mul: the resulting bounds on weighted combinations.
• TauCeti.eigenvalues_frameOperator_eq_eigenvalues_gramOperator: the two sorted spectra agree through the smaller dimension.
• TauCeti.le_eigenvalues_gramOperator: a lower frame bound a bounds the Gram eigenvalues below finrank 𝕜 E from below by a.
• TauCeti.mul_norm_sq_le_sum_norm_inner_sq_of_le_eigenvalues_gramOperator: conversely, such a Gram-spectrum bound gives the lower frame bound when the family has at least finrank 𝕜 E members.

References

• O. Christensen, An Introduction to Frames and Riesz Bases, second edition, Birkhäuser, 2016, Chapter 1 (frames in finite-dimensional inner product spaces, the frame operator and the Gram matrix).

Analysis and synthesis

noncomputable def TauCeti.analysisMap (𝕜 : Type u_1) {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : ι → E) : E →ₗ[𝕜] EuclideanSpace 𝕜 ι

The analysis map x ↦ (⟪vᵢ, x⟫)ᵢ of a finite family v, from the ambient space to coefficient space.

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

The synthesis map a ↦ ∑ᵢ aᵢ vᵢ of a finite family v, from coefficient space to the ambient space.

theorem TauCeti.range_synthesisMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : (synthesisMap 𝕜 v).range = Submodule.span 𝕜 (Set.range v)

The range of synthesis is the span of the finite family.

@[simp]

theorem TauCeti.analysisMap_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : ι → E) (x : E) (i : ι) : ((analysisMap 𝕜 v) x).ofLp i = inner 𝕜 (v i) x

@[simp]

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

theorem TauCeti.linearIndependent_iff_injective_synthesisMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : LinearIndependent 𝕜 v ↔ Function.Injective ⇑(synthesisMap 𝕜 v)

A finite family is linearly independent exactly when its synthesis map is injective.

theorem TauCeti.synthesisMap_single {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v : ι → E) (i : ι) (c : 𝕜) : (synthesisMap 𝕜 v) (EuclideanSpace.single i c) = c • v i

theorem TauCeti.bijective_synthesisMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : LinearIndependent 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) : Function.Bijective ⇑(synthesisMap 𝕜 v)

The synthesis map of a linearly independent family spanning the space is bijective.

theorem TauCeti.bilinearComp_synthesisMap_eq_sum {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (Q : E →L[𝕜] E →L[𝕜] 𝕜) (v : ι → E) : Q.bilinearComp (LinearMap.toContinuousLinearMap (synthesisMap 𝕜 v)) (LinearMap.toContinuousLinearMap (synthesisMap 𝕜 v)) = ∑ i : ι, ∑ j : ι, (Q (v i)) (v j) • ContinuousLinearMap.smulRight (EuclideanSpace.proj i) (EuclideanSpace.proj j)

A bilinear form read through the synthesis map of a family is the sum of its values on pairs of members of the family times the elementary bilinear forms.

theorem TauCeti.inner_synthesisMap_left {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (a : EuclideanSpace 𝕜 ι) (x : E) : inner 𝕜 ((synthesisMap 𝕜 v) a) x = inner 𝕜 a ((analysisMap 𝕜 v) x)

The synthesis map is adjoint to the analysis map: ⟪∑ᵢ aᵢ vᵢ, x⟫ = ⟪a, (⟪vᵢ, x⟫)ᵢ⟫.

theorem TauCeti.norm_analysisMap_sq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (x : E) : ‖(analysisMap 𝕜 v) x‖ ^ 2 = ∑ i : ι, ‖inner 𝕜 (v i) x‖ ^ 2

‖analysis x‖² = ∑ᵢ ‖⟪vᵢ, x⟫‖².

The frame and Gram operators

noncomputable def TauCeti.frameOperator (𝕜 : Type u_1) {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : E →ₗ[𝕜] E

The frame operator x ↦ ∑ᵢ ⟪vᵢ, x⟫ vᵢ of a finite family: synthesis after analysis.

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

The Gram operator of a finite family on coefficient space: analysis after synthesis. Its matrix is the Gram matrix Matrix.gram 𝕜 v (TauCeti.gramOperator_eq_toEuclideanLin_gram).

theorem TauCeti.frameOperator_def {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : frameOperator 𝕜 v = synthesisMap 𝕜 v ∘ₗ analysisMap 𝕜 v

theorem TauCeti.gramOperator_def {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : gramOperator 𝕜 v = analysisMap 𝕜 v ∘ₗ synthesisMap 𝕜 v

@[simp]

theorem TauCeti.frameOperator_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (x : E) : (frameOperator 𝕜 v) x = ∑ i : ι, inner 𝕜 (v i) x • v i

@[simp]

theorem TauCeti.gramOperator_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (a : EuclideanSpace 𝕜 ι) (i : ι) : ((gramOperator 𝕜 v) a).ofLp i = ∑ j : ι, inner 𝕜 (v i) (v j) * a.ofLp j

theorem TauCeti.gramOperator_eq_toEuclideanLin_gram {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (v : ι → E) : gramOperator 𝕜 v = Matrix.toEuclideanLin (Matrix.gram 𝕜 v)

The Gram operator is the Gram matrix Matrix.gram 𝕜 v acting on coefficient space.

theorem TauCeti.inner_frameOperator_left {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (x y : E) : inner 𝕜 ((frameOperator 𝕜 v) x) y = inner 𝕜 ((analysisMap 𝕜 v) x) ((analysisMap 𝕜 v) y)

The sesquilinear form of the frame operator is the inner product of analysis coefficients.

theorem TauCeti.inner_gramOperator_right {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (a b : EuclideanSpace 𝕜 ι) : inner 𝕜 a ((gramOperator 𝕜 v) b) = inner 𝕜 ((synthesisMap 𝕜 v) a) ((synthesisMap 𝕜 v) b)

The sesquilinear form of the Gram operator is the inner product of the synthesized vectors.

theorem TauCeti.re_inner_frameOperator_apply_self {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) (x : E) : RCLike.re (inner 𝕜 ((frameOperator 𝕜 v) x) x) = ∑ i : ι, ‖inner 𝕜 (v i) x‖ ^ 2

The quadratic form of the frame operator is x ↦ ∑ᵢ ‖⟪vᵢ, x⟫‖².

theorem TauCeti.isSymmetric_frameOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : (frameOperator 𝕜 v).IsSymmetric

The frame operator is symmetric.

theorem TauCeti.isPositive_frameOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : (frameOperator 𝕜 v).IsPositive

The frame operator is positive.

theorem TauCeti.isPositive_gramOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : (gramOperator 𝕜 v).IsPositive

The Gram operator is positive.

theorem TauCeti.isSymmetric_gramOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : (gramOperator 𝕜 v).IsSymmetric

The Gram operator is symmetric.

The overlap operator of two families

noncomputable def TauCeti.overlapOperator (𝕜 : Type u_1) {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {κ : Type u_4} [Fintype κ] (u : ι → E) (v : κ → E) : EuclideanSpace 𝕜 κ →ₗ[𝕜] EuclideanSpace 𝕜 ι

The overlap operator of finite families u : ι → E and v : κ → E: analysis by u after synthesis by v, with matrix (⟪uᵢ, vⱼ⟫)ᵢⱼ (TauCeti.overlapOperator_eq_toEuclideanLin). On the diagonal it is the Gram operator (TauCeti.overlapOperator_self).

theorem TauCeti.overlapOperator_def {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {κ : Type u_4} [Fintype κ] (u : ι → E) (v : κ → E) : overlapOperator 𝕜 u v = analysisMap 𝕜 u ∘ₗ synthesisMap 𝕜 v

@[simp]

theorem TauCeti.overlapOperator_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {κ : Type u_4} [Fintype κ] (u : ι → E) (v : κ → E) (a : EuclideanSpace 𝕜 κ) (i : ι) : ((overlapOperator 𝕜 u v) a).ofLp i = ∑ j : κ, inner 𝕜 (u i) (v j) * a.ofLp j

The i-th coordinate of the overlap operator applied to a is ∑ⱼ ⟪uᵢ, vⱼ⟫ aⱼ, the matrix (⟪uᵢ, vⱼ⟫)ᵢⱼ acting on the coefficients a.

@[simp]

theorem TauCeti.overlapOperator_single {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (u : ι → E) (v : κ → E) (j : κ) (c : 𝕜) : (overlapOperator 𝕜 u v) (EuclideanSpace.single j c) = c • (analysisMap 𝕜 u) (v j)

The overlap operator sends the j-th coordinate vector, scaled by c, to c times the coefficients (⟪uᵢ, vⱼ⟫)ᵢ of vⱼ.

theorem TauCeti.overlapOperator_eq_toEuclideanLin {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (u : ι → E) (v : κ → E) : overlapOperator 𝕜 u v = Matrix.toEuclideanLin (Matrix.of fun (i : ι) (j : κ) => inner 𝕜 (u i) (v j))

The overlap operator is the matrix (⟪uᵢ, vⱼ⟫)ᵢⱼ acting on coefficient space.

@[simp]

theorem TauCeti.overlapOperator_self {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : ι → E) : overlapOperator 𝕜 v v = gramOperator 𝕜 v

The overlap operator of a family with itself is its Gram operator.

theorem TauCeti.inner_overlapOperator_left {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {κ : Type u_4} [Fintype κ] (u : ι → E) (v : κ → E) (b : EuclideanSpace 𝕜 ι) (a : EuclideanSpace 𝕜 κ) : inner 𝕜 ((overlapOperator 𝕜 v u) b) a = inner 𝕜 b ((overlapOperator 𝕜 u v) a)

The overlap operators in the two orders are adjoint to each other: ⟪O_{v,u} b, a⟫ = ⟪b, O_{u,v} a⟫.

@[simp]

theorem TauCeti.adjoint_overlapOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {κ : Type u_4} [Fintype κ] (u : ι → E) (v : κ → E) : LinearMap.adjoint (overlapOperator 𝕜 u v) = overlapOperator 𝕜 v u

Swapping the two families gives the adjoint overlap operator.

Parseval frames

theorem TauCeti.norm_analysisMap_of_frameOperator_eq_id {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : frameOperator 𝕜 v = LinearMap.id) (x : E) : ‖(analysisMap 𝕜 v) x‖ = ‖x‖

A family whose frame operator is the identity, a Parseval frame, has an isometric analysis map: ‖(⟪vᵢ, x⟫)ᵢ‖ = ‖x‖.

theorem TauCeti.norm_synthesisMap_le_of_frameOperator_eq_id {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hv : frameOperator 𝕜 v = LinearMap.id) (a : EuclideanSpace 𝕜 ι) : ‖(synthesisMap 𝕜 v) a‖ ≤ ‖a‖

The synthesis map of a Parseval frame is a contraction: ‖∑ᵢ aᵢ vᵢ‖ ≤ ‖a‖.

theorem TauCeti.frameOperator_sqrt_smul_eq_id {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {u : ι → E} {c : ι → ℝ} (hc : ∀ (i : ι), 0 ≤ c i) (h : ∀ (x : E), ∑ i : ι, ↑(c i) • inner 𝕜 (u i) x • u i = x) : (frameOperator 𝕜 fun (i : ι) => ↑√(c i) • u i) = LinearMap.id

A decomposition ∑ᵢ cᵢ ⟪uᵢ, x⟫ uᵢ = x of every vector, with nonnegative weights cᵢ, makes the rescaled family √cᵢ • uᵢ a Parseval frame.

theorem TauCeti.norm_sum_mul_smul_le_sqrt {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {u : ι → E} {c : ι → ℝ} (hc : ∀ (i : ι), 0 ≤ c i) (h : ∀ (x : E), ∑ i : ι, ↑(c i) • inner 𝕜 (u i) x • u i = x) (b : ι → 𝕜) : ‖∑ i : ι, (↑(c i) * b i) • u i‖ ≤ √(∑ i : ι, c i * ‖b i‖ ^ 2)

Synthesis bound for a weighted Parseval decomposition. If ∑ᵢ cᵢ ⟪uᵢ, x⟫ uᵢ = x for every x, with nonnegative weights cᵢ, then ‖∑ᵢ cᵢ bᵢ uᵢ‖ ≤ (∑ᵢ cᵢ ‖bᵢ‖²)^(1/2) for all coefficients bᵢ.

theorem TauCeti.norm_sum_mul_smul_le_sqrt_mul {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {u : ι → E} {c : ι → ℝ} (hc : ∀ (i : ι), 0 ≤ c i) (h : ∀ (x : E), ∑ i : ι, ↑(c i) • inner 𝕜 (u i) x • u i = x) {b : ι → 𝕜} {B : ℝ} (hb : ∀ (i : ι), ‖b i‖ ≤ B) : ‖∑ i : ι, (↑(c i) * b i) • u i‖ ≤ √(∑ i : ι, c i) * B

If ∑ᵢ cᵢ ⟪uᵢ, x⟫ uᵢ = x for every x, with nonnegative weights cᵢ, then combinations with coefficients of norm at most B satisfy ‖∑ᵢ cᵢ bᵢ uᵢ‖ ≤ √(∑ᵢ cᵢ) B.

Adjoints in finite dimension

@[simp]

theorem TauCeti.adjoint_analysisMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) : LinearMap.adjoint (analysisMap 𝕜 v) = synthesisMap 𝕜 v

The adjoint of the analysis map is the synthesis map.

@[simp]

theorem TauCeti.adjoint_synthesisMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) : LinearMap.adjoint (synthesisMap 𝕜 v) = analysisMap 𝕜 v

The adjoint of the synthesis map is the analysis map.

theorem TauCeti.frameOperator_eq_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) : frameOperator 𝕜 v = LinearMap.adjoint (analysisMap 𝕜 v) ∘ₗ analysisMap 𝕜 v

The frame operator is the source Gram operator A† A of the analysis map A.

theorem TauCeti.gramOperator_eq_self_comp_adjoint {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) : gramOperator 𝕜 v = analysisMap 𝕜 v ∘ₗ LinearMap.adjoint (analysisMap 𝕜 v)

The Gram operator is the target Gram operator A A† of the analysis map A.

theorem TauCeti.adjoint_synthesisMap_comp_synthesisMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {κ : Type u_4} [Fintype κ] (u : ι → E) (v : κ → E) : LinearMap.adjoint (synthesisMap 𝕜 u) ∘ₗ synthesisMap 𝕜 v = overlapOperator 𝕜 u v

In a finite-dimensional space the overlap operator is S_u† S_v for the synthesis maps S_u and S_v; for orthonormal families these are the coordinate isometries Orthonormal.synthesisMapIsometry.

Frame bounds and the Gram spectrum

theorem TauCeti.eigenvalues_frameOperator_eq_eigenvalues_gramOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) {d m : ℕ} (hd : Module.finrank 𝕜 E = d) (hm : Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = m) {i : ℕ} (hid : i < d) (him : i < m) : ⋯.eigenvalues hd ⟨i, hid⟩ = ⋯.eigenvalues hm ⟨i, him⟩

The sorted eigenvalues of the frame operator and of the Gram operator agree at every index below both finrank 𝕜 E and the size of the family.

theorem TauCeti.le_eigenvalues_gramOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) {a : ℝ} (h : ∀ (x : E), a * ‖x‖ ^ 2 ≤ ∑ i : ι, ‖inner 𝕜 (v i) x‖ ^ 2) {m : ℕ} (hm : Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = m) (i : Fin m) (hi : ↑i < Module.finrank 𝕜 E) : a ≤ ⋯.eigenvalues hm i

Gram spectrum from a lower frame bound. If a ‖x‖² ≤ ∑ᵢ ‖⟪vᵢ, x⟫‖² for every x, then every sorted eigenvalue of the Gram operator whose index is below finrank 𝕜 E is at least a.

theorem TauCeti.mul_norm_sq_le_sum_norm_inner_sq_of_le_eigenvalues_gramOperator {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] (v : ι → E) {a : ℝ} {m : ℕ} (hm : Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = m) (hdm : Module.finrank 𝕜 E ≤ m) (h : ∀ (i : Fin m), ↑i < Module.finrank 𝕜 E → a ≤ ⋯.eigenvalues hm i) (x : E) : a * ‖x‖ ^ 2 ≤ ∑ i : ι, ‖inner 𝕜 (v i) x‖ ^ 2

Lower frame bound from the Gram spectrum. If the family has at least finrank 𝕜 E members and the sorted Gram eigenvalues below index finrank 𝕜 E are at least a, then a ‖x‖² ≤ ∑ᵢ ‖⟪vᵢ, x⟫‖² for every x.

Orthonormal bases

@[simp]

theorem OrthonormalBasis.analysisMap_eq_repr {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : TauCeti.analysisMap 𝕜 ⇑b = ↑b.repr.toLinearEquiv

The analysis map of an orthonormal basis is its coordinate map b.repr.

@[simp]

theorem OrthonormalBasis.synthesisMap_eq_repr_symm {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : TauCeti.synthesisMap 𝕜 ⇑b = ↑b.repr.symm.toLinearEquiv

The synthesis map of an orthonormal basis is the inverse b.repr.symm of its coordinate map.

@[simp]

theorem OrthonormalBasis.frameOperator_eq_id {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : TauCeti.frameOperator 𝕜 ⇑b = LinearMap.id

The frame operator of an orthonormal basis is the identity.