OAI/Analysis/KadisonKastler/TracialSequenceState.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The canonical trace on a bounded product

The trace is the scalar ultralimit of the coordinate traces. The varying family covers both the constant-factor and finite-matrix products used here.

  1. theorem OAI.KadisonKastler.exists_tracialSequenceValue line 23
  2. def OAI.KadisonKastler.tracialSequenceValue line 35
  3. theorem OAI.KadisonKastler.norm_tracialSequenceValue line 38
  4. theorem OAI.KadisonKastler.tendsto_tracialSequenceValue line 42
  5. def OAI.KadisonKastler.tracialSequenceLinear line 47
  6. def OAI.KadisonKastler.tracialSequenceContinuous line 58
  7. theorem OAI.KadisonKastler.tracialSequenceContinuous_apply line 63
  8. theorem OAI.KadisonKastler.tracialSequenceValue_one line 68
  9. theorem OAI.KadisonKastler.tracialSequenceValue_tracial line 74
  10. theorem OAI.KadisonKastler.tracialSequenceValue_positive line 81
  11. theorem OAI.KadisonKastler.tracialSequenceValue_positive_im line 88