OAI/Analysis/FiniteFactor/OperatorTracialRepresentation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.FiniteFactor.TracialRepresentation line 13

    Source documentation

    A concrete finite tracial von Neumann algebra in a faithful vector-trace representation. These are operator-algebra data, without approximation assumptions.

    structure TracialRepresentation (M : VonNeumannAlgebra H) where
…
  2. abbrev OAI.FiniteFactor.TracialRepresentation.Algebra line 23
  3. def OAI.FiniteFactor.TracialRepresentation.trace line 25
  4. def OAI.FiniteFactor.TracialRepresentation.norm₂ line 26
  5. theorem OAI.FiniteFactor.TracialRepresentation.trace_one line 28
  6. theorem OAI.FiniteFactor.TracialRepresentation.trace_mul_comm line 31
  7. theorem OAI.FiniteFactor.TracialRepresentation.trace_star_mul line 34
  8. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_star line 41
  9. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_zero line 52
  10. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_sub line 53
  11. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_add_le line 56
  12. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_smul line 59
  13. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_mul_le line 62
  14. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_mul_le_right line 65
  15. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_le_norm line 70
  16. theorem OAI.FiniteFactor.TracialRepresentation.norm_trace_le_norm₂ line 74
  17. theorem OAI.FiniteFactor.TracialRepresentation.norm₂_eq_zero_iff line 77