OAI/Analysis/KadisonKastler/FaithfulTraceGNS.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The concrete GNS representation of a faithful tracial state

  1. def OAI.KadisonKastler.FaithfulTracialState.toPositiveLinearMap line 16
  2. abbrev OAI.KadisonKastler.TraceStateHilbert line 28
  3. def OAI.KadisonKastler.traceStateVector line 30
  4. def OAI.KadisonKastler.traceStateRepresentation line 33
  5. theorem OAI.KadisonKastler.norm_traceStateVector line 37
  6. theorem OAI.KadisonKastler.traceStateVector_sub line 42
  7. theorem OAI.KadisonKastler.traceStateRepresentation_vector line 46
  8. theorem OAI.KadisonKastler.traceStateVector_dense line 53
  9. theorem OAI.KadisonKastler.traceStateRepresentation_injective line 58
  10. theorem OAI.KadisonKastler.norm_traceStateRepresentation line 74
  11. def OAI.KadisonKastler.traceStateRight line 80

    Source documentation

    Right multiplication, supplied by the same tracial GNS construction.

    def traceStateRight (τ : FaithfulTracialState A) (a : A) :
    TraceStateHilbert τ →L[ℂ] TraceStateHilbert τ :=
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceStateHilbert

  12. theorem OAI.KadisonKastler.traceStateRight_vector line 84
  13. theorem OAI.KadisonKastler.traceState_left_right_commute line 89