Singular values of a continuous linear map

Mathlib.Analysis.InnerProductSpace.SingularValues defines the singular values of a linear map between finite-dimensional inner product spaces, as a Finsupp sequence LinearMap.singularValues : ℕ →₀ ℝ. Between finite-dimensional spaces every linear map is continuous, so the two notions agree; but the operator-theoretic consumers — approximation numbers, Ky Fan norms, Eckart--Young — all work with ContinuousLinearMap, and without an accessor at that level every public statement about them has to spell T.toLinearMap.singularValues n, leaking the coercion into the statement and into every downstream proof.

This module supplies the accessor and the small part of the API that the operator-theoretic layer actually uses. Everything is definitionally the LinearMap notion, so ContinuousLinearMap.toLinearMap_singularValues moves freely between the two and no result is duplicated: the lemmas below are one-line delegations kept only so that consumers never have to unfold the accessor.

Naming

The name stays plural, matching LinearMap.singularValues. The signature-polish backlog suggested a singular singularValue "unless the existing Mathlib function is irrevocably plural" — it is: the Mathlib object is the whole ℕ →₀ ℝ sequence, not an individual value, and T.singularValues n is function application to it. A singular accessor would have to be a second definition wrapping the first, which is exactly the duplication this module exists to avoid.

Main declarations

• ContinuousLinearMap.singularValues: the singular-value sequence of a continuous linear map.
• ContinuousLinearMap.toLinearMap_singularValues: the bridge to LinearMap.singularValues, simp-normalizing towards the continuous form.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Extraction class: new, written per the signature-polish backlog, which asked for "a singular-value accessor on ContinuousLinearMap rather than T.toLinearMap.singularValues in public statements".
• Spectra influence: none — this module imports only Mathlib.

noncomputable def ContinuousLinearMap.singularValues {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) : ℕ →₀ ℝ

The singular values of a continuous linear map between finite-dimensional inner product spaces: the sequence whose first finrank 𝕜 E entries are the square roots of the eigenvalues of T⋆ T in decreasing order, repeated according to multiplicity, and zero thereafter.

Zero-indexed: T.singularValues 0 is the largest singular value, and the positive singular values occupy 0 ≤ i < finrank 𝕜 T.range. This matches LinearMap.singularValues, of which this is definitionally a restatement, and it is why the approximation numbers of ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/Basic.lean are indexed the same way.

Equations

• T.singularValues = (↑T).singularValues

@[simp]

theorem ContinuousLinearMap.toLinearMap_singularValues {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) : (↑T).singularValues = T.singularValues

The singular values of a continuous linear map are those of the underlying linear map. Oriented towards the continuous form, so that simp removes the coercion from statements rather than introducing it.

theorem ContinuousLinearMap.singularValues_nonneg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) (i : ℕ) : 0 ≤ T.singularValues i

Singular values are nonnegative.

theorem ContinuousLinearMap.singularValues_antitone {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) : Antitone ⇑T.singularValues

Singular values are listed in decreasing order.

theorem ContinuousLinearMap.singularValues_of_finrank_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) {i : ℕ} (hi : Module.finrank 𝕜 E ≤ i) : T.singularValues i = 0

Singular values past the dimension of the source vanish.

@[simp]

theorem ContinuousLinearMap.singularValues_zero {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] : singularValues 0 = 0

The zero map has all singular values zero.

@[simp]

theorem ContinuousLinearMap.singularValues_eq_zero_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {T : E →L[𝕜] F} : T.singularValues = 0 ↔ T = 0

Conversely, vanishing singular values force the map to be zero -- the definiteness that makes any gauge built from them a norm rather than a seminorm.

theorem ContinuousLinearMap.singularValues_pos_iff_lt_finrank_range {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {T : E →L[𝕜] F} {n : ℕ} : 0 < T.singularValues n ↔ n < Module.finrank 𝕜 ↥(↑T).range

A singular value is positive exactly below the rank.