OAI/Analysis/KadisonKastler/TracialMatrixAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar values of finite matrix averages in a tracial algebra

  1. theorem OAI.KadisonKastler.tracial_matrixUnitAverage_eq_trace line 20

    Source documentation

    On the matrix algebra, finite signed averaging is exactly the scalar specified by the represented trace.

    theorem tracial_matrixUnitAverage_eq_trace (τ : TracialRepresentation M)
    {n : ℕ} [Nonempty (Fin n)] (E : MatrixUnitSystem (Fin n) (H →L[ℂ] H))
    (hE : E.algebra ≤ M.toStarSubalgebra) (x : Algebra M) (hx : x.val ∈ E.algebra) :
    matrixUnitAverage E x.val = τ.trace x • (1 : H →L[ℂ] H) := by
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitAverage