OAI/Analysis/JiangSu/Traces/TraceAlgebra.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UnitalTomsWinter.AlgebraicTrace line 10
  2. instance OAI.UnitalTomsWinter.(instance at line 14) line 14
  3. theorem OAI.UnitalTomsWinter.trace_compression line 17
  4. def OAI.UnitalTomsWinter.cornerSymmetry line 39
  5. theorem OAI.UnitalTomsWinter.cornerSymmetry_selfAdjoint line 41
  6. theorem OAI.UnitalTomsWinter.cornerSymmetry_square line 46
  7. theorem OAI.UnitalTomsWinter.cornerSymmetry_supported line 54
  8. theorem OAI.UnitalTomsWinter.trace_cornerSymmetry line 62
  9. theorem OAI.UnitalTomsWinter.normalized_isometry line 68
  10. theorem OAI.UnitalTomsWinter.isometry_range_projection line 78
  11. structure OAI.UnitalTomsWinter.TracialState line 95
  12. def OAI.UnitalTomsWinter.TracialState.algebraicTrace line 103
  13. def OAI.UnitalTomsWinter.TracialState.twoNorm line 107
  14. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_eq line 110
  15. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_nonneg line 114
  16. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_zero line 116
  17. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_one line 119
  18. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_add_le line 122
  19. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_smul line 127
  20. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_star line 131
  21. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_mul_left line 135
  22. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_mul_right line 147
  23. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_le_norm line 155
  24. def OAI.UnitalTomsWinter.TracialState.toPreGNSContinuous line 158
  25. theorem OAI.UnitalTomsWinter.TracialState.continuous_twoNorm line 163