OAI/Analysis/KadisonKastler/MatrixTrace.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The normalized faithful trace on finite matrices

The normalized sum of the diagonal traces is positive and faithful by expanding the diagonal entries of a matrix star square.

  1. def OAI.KadisonKastler.matrixTraceLinearMap line 25
  2. theorem OAI.KadisonKastler.matrixTraceLinearMap_apply line 33
  3. theorem OAI.KadisonKastler.matrixTraceLinearMap_star_mul line 38
  4. theorem OAI.KadisonKastler.matrixTraceLinearMap_star_mul_re line 45
  5. theorem OAI.KadisonKastler.matrixTraceLinearMap_positive line 52
  6. theorem OAI.KadisonKastler.matrixTraceLinearMap_positive_im line 58
  7. theorem OAI.KadisonKastler.matrixTraceLinearMap_tracial line 64
  8. theorem OAI.KadisonKastler.matrixTraceLinearMap_one line 78
  9. theorem OAI.KadisonKastler.matrixTraceLinearMap_faithful line 84
  10. def OAI.KadisonKastler.matrixTrace line 101

    Source documentation

    The canonical normalized faithful tracial state on finite square matrices.

    def matrixTrace (τ : FaithfulTracialState B) : FaithfulTracialState (CStarMatrix ι ι B) where
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState

  11. theorem OAI.KadisonKastler.matrixTrace_apply line 109
  12. def OAI.KadisonKastler.coordinateMatrixUnits line 114

    Source documentation

    The canonical matrix units, with the identity of B in the selected entry.

    def coordinateMatrixUnits : Generator.MatrixUnitSystem ι (CStarMatrix ι ι B) where
…

    Mentions: OAI.Generator.MatrixUnitSystem

  13. theorem OAI.KadisonKastler.coordinateMatrixUnits_projection line 132
  14. theorem OAI.KadisonKastler.matrixTrace_coordinate_diagonal line 136
  15. theorem OAI.KadisonKastler.finiteAverage_coordinate_diagonal line 142