Singular values for finite-dimensional linear maps

For a linear map T between finite-dimensional inner product spaces E and F, we define the singular values, which are the square roots of the eigenvalues of T.adjoint ∘ₗ T, arranged in descending order and repeated according to their multiplicity.

With our definition, there are countably infinitely many singular values, but only the first rank(T) singular values are nonzero.

The singular values are zero-indexed, so T.singularValues 0 is the first singular value. This means the positive singular values occur at 0 ≤ i < rank(T) and not 1 ≤ i ≤ rank(T).

Main definition

• LinearMap.singularValues: The infinite but finitely supported sequence of the singular values of a linear map.

Main statements

• LinearMap.support_singularValues: The first rank(T) many singular values are positive, and the rest are zero.

Implementation notes

Suppose T : E →ₗ[𝕜] F where dim(E) = n, dim(F) = m. In mathematical literature, the number of singular values varies, with popular choices including

• rank(T) singular values, all of which are positive.
• min(n,m) singular values, some of which might be zero.
• n singular values, some of which might be zero. This is the approach taken in [Axl24].
• Countably infinitely many singular values, with all but finitely many of them being zero.

We take the last approach for the following reasons:

• It avoid unnecessary dependent typing.
• You can easily convert this definition to the other three by composing with Fin.val, but converting between any two of the other definitions is more inconvenient because it involves multiple Fin types.
• If you prefer a definition where there are k singular values, you can treat the singular values after k as junk values. Not having to prove that i < k when getting the ith singular value has similar advantages to not having to prove that y ≠ 0 when calculating x / y.
• This API coincides with a potential future API for approximation numbers, which are a generalization of singular values to continuous linear maps between possibly-infinite-dimensional normed vector spaces.

TODO

• Generalize singular values to the approximation numbers for maps between possibly-infinite-dimensional normed vector spaces. This will likely have a similar type signature to the current singular values definition, except it will take in a ContinuousLinearMap and will not be finitely supported.

References

• Sheldon Axler, Linear Algebra Done Right

Tags

singular values

noncomputable def LinearMap.singularValues {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : ℕ →₀ ℝ

If T : E →ₗ[𝕜] F is a linear map between finite dimensional inner product spaces, then T.singularValues is the infinite sequence where the first dim(E) elements are the square roots of eigenvalues of T.adjoint ∘ₗ T (which are guaranteed to be nonnegative real numbers), arranged in descending order and repeated according to their multiplicity, and the rest of the elements in the infinite sequence are zero. Please see the module docstring of Mathlib/Analysis/InnerProductSpace/SingularValues.lean for an explanation of this design decision.

The singular values are zero-indexed, so T.singularValues 0 refers to the first singular value. This means the positive singular values occur at 0 ≤ i < rank(T) and not 1 ≤ i ≤ rank(T).

Equations

• T.singularValues = Finsupp.embDomain Fin.valEmbedding (Finsupp.ofSupportFinite (fun (i : Fin (Module.finrank 𝕜 E)) => √(⋯.eigenvalues ⋯ i)) ⋯)

theorem LinearMap.singularValues_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) (i : ℕ) : 0 ≤ T.singularValues i

theorem LinearMap.singularValues_pos_iff_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) (i : ℕ) : 0 < T.singularValues i ↔ T.singularValues i ≠ 0

theorem LinearMap.singularValues_fin {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n) : T.singularValues ↑i = √(⋯.eigenvalues hn i)

Connection between LinearMap.singularValues and LinearMap.IsSymmetric.eigenvalues. Together with LinearMap.singularValues_of_finrank_le, this characterizes the singular values.

Because of the square root, you probably need to use T.isPositive_adjoint_comp_self.nonneg_eigenvalues to make effective use of this theorem.

theorem LinearMap.singularValues_of_lt {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) {i : ℕ} (hi : i < n) : T.singularValues i = √(⋯.eigenvalues hn ⟨i, hi⟩)

theorem LinearMap.singularValues_of_finrank_le {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {i : ℕ} (hi : Module.finrank 𝕜 E ≤ i) : T.singularValues i = 0

theorem LinearMap.sq_singularValues_fin {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n) : T.singularValues ↑i ^ 2 = ⋯.eigenvalues hn i

theorem LinearMap.sq_singularValues_of_lt {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) {i : ℕ} (hi : i < n) : T.singularValues i ^ 2 = ⋯.eigenvalues hn ⟨i, hi⟩

theorem LinearMap.hasEigenvalue_adjoint_comp_self_sq_singularValues {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : n < Module.finrank 𝕜 E) : Module.End.HasEigenvalue (adjoint T ∘ₗ T) (↑(T.singularValues n) ^ 2)

theorem LinearMap.singularValues_antitone {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : Antitone ⇑T.singularValues

theorem LinearMap.injective_iff_forall_lt_finrank_singularValues_pos {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : Function.Injective ⇑T ↔ ∀ i < Module.finrank 𝕜 E, 0 < T.singularValues i

7.68(a) from [Axl24]. Note that we have countably infinitely many singular values whereas there are only dim(domain(T)) singular values in [Axl24], so we modify the statement to account for this.

theorem LinearMap.card_support_singularValues {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : T.singularValues.support.card = Module.finrank 𝕜 ↥T.range

7.68(b) from [Axl24]. See also LinearMap.support_singularValues for a stronger statement.

theorem LinearMap.isLowerSet_support_singularValues {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : IsLowerSet ↑T.singularValues.support

@[simp]

theorem LinearMap.support_singularValues {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : T.singularValues.support = Finset.range (Module.finrank 𝕜 ↥T.range)

theorem LinearMap.singularValues_pos_iff_lt_finrank_range {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} : 0 < T.singularValues n ↔ n < Module.finrank 𝕜 ↥T.range

theorem LinearMap.singularValues_finrank_range_self {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : T.singularValues (Module.finrank 𝕜 ↥T.range) = 0

theorem LinearMap.singularValues_eq_zero_iff_le_finrank_range {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} : T.singularValues n = 0 ↔ Module.finrank 𝕜 ↥T.range ≤ n

@[simp]

theorem LinearMap.singularValues_zero {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] : singularValues 0 = 0

@[simp]

theorem LinearMap.singularValues_eq_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) : T.singularValues = 0 ↔ T = 0