Theorems · Definition · linear algebra

LinearMap.singularValues

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

Defined in

Mathlib.Analysis.InnerProductSpace.SingularValues

Cited by

20 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensionalNormedAddCommGroupInnerProductSpaceFiniteDimensional