OAI/Analysis/TracialSplitting/FaithfulRepresentations.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.stateGNSVector line 44
  2. lemma OAI.Pureness.stateGNSVector_norm line 46
  3. lemma OAI.Pureness.stateGNS_apply_vector line 55
  4. lemma OAI.Pureness.stateGNS_vector_value line 59
  5. theorem OAI.Pureness.exists_positiveState_norming line 74
  6. theorem OAI.Pureness.positive_eq_zero_of_states line 90
  7. theorem OAI.Pureness.stateGNS_separates line 96
  8. def OAI.Pureness.hilbertSumAction line 120
  9. lemma OAI.Pureness.hilbertSumAction_norm_le line 125
  10. def OAI.Pureness.hilbertSumOperator line 139
  11. lemma OAI.Pureness.hilbertSumOperator_apply line 146
  12. def OAI.Pureness.hilbertSumRepresentation line 149
  13. lemma OAI.Pureness.hilbertSumRepresentation_apply line 168
  14. lemma OAI.Pureness.hilbertSumRepresentation_eq_iff line 171
  15. def OAI.Pureness.PositiveStateIndex line 195
  16. abbrev OAI.Pureness.UniversalStateHilbert line 197
  17. def OAI.Pureness.universalStateGNS line 199
  18. lemma OAI.Pureness.universalStateGNS_apply line 203
  19. theorem OAI.Pureness.universalStateGNS_injective line 206
  20. def OAI.Pureness.universalStateHilbertNormedAddCommGroup line 229
  21. def OAI.Pureness.universalStateHilbertInnerProductSpace line 235
  22. theorem OAI.Pureness.universalStateHilbertCompleteSpace line 238
  23. def OAI.Pureness.StateHilbertSpace line 249
  24. instance OAI.Pureness.stateHilbertNormedAddCommGroup line 251
  25. instance OAI.Pureness.stateHilbertInnerProductSpace line 254
  26. instance OAI.Pureness.stateHilbertCompleteSpace line 257
  27. def OAI.Pureness.stateHilbertRepresentation line 260
  28. theorem OAI.Pureness.stateHilbertRepresentation_injective line 264