Theorems · Theorem · linear algebra

LinearMap.singularValues_fin

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : 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.

Defined in

Mathlib.Analysis.InnerProductSpace.SingularValues

Cited by

4 results in Mathlib

Foundations

Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensionalNormedAddCommGroupInnerProductSpaceFiniteDimensional