OAI/Analysis/TracialSplitting/GNSRepresentations.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NuclearTrace.norm_preGNS_star line 25
  2. lemma OAI.NuclearTrace.right_preGNS_norm line 31
  3. def OAI.NuclearTrace.rightPreGNS line 44
  4. lemma OAI.NuclearTrace.rightPreGNS_apply line 48
  5. def OAI.NuclearTrace.rightGNSMap line 51
  6. lemma OAI.NuclearTrace.rightGNSMap_coe line 53
  7. lemma OAI.NuclearTrace.rightGNSMap_mul line 57
  8. lemma OAI.NuclearTrace.rightGNSMap_star line 65
  9. def OAI.NuclearTrace.rightGNS line 76
  10. lemma OAI.NuclearTrace.rightGNS_coe line 102
  11. lemma OAI.NuclearTrace.left_right_commute line 106
  12. def OAI.Pureness.commutingStarTensorHom line 125
  13. lemma OAI.Pureness.commutingStarTensorHom_tmul line 142
  14. def OAI.NuclearTrace.vectorFunctional line 158
  15. lemma OAI.NuclearTrace.vectorFunctional_apply line 168
  16. def OAI.NuclearTrace.leftRightTensor line 179
  17. lemma OAI.NuclearTrace.leftRightTensor_vector line 182
  18. theorem OAI.NuclearTrace.nuclear_diagonal_state line 189