OAI/Analysis/KadisonSimilarity/Tracial/MatrixTracialInputTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spectral rounding for finite matrices in an actual normal representation.

  1. theorem OAI.KadisonSimilarity.matrix_spectralProjectionRoundingInput_of_concrete_range line 15

    Source documentation

    Any faithful normal realization supplies all finite-matrix rounding inputs, for every positive functional on the matrix algebra.

    theorem matrix_spectralProjectionRoundingInput_of_concrete_range
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hσ : Function.Injective σ)
    (P : VonNeumannAlgebra H) (hrange : σ.range = P.toStarSubalgebra)
    (n : ℕ) [NeZero n] (τ : CStarMatrix (Fin n) (Fin n) A →ₚ[ℂ] ℂ) :
    SpectralProjectionRoundingInput τ :=
…

    Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput