OAI/Analysis/BoundedHochschild/MatrixDilation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Matrix dilations, tracial matrix algebras and bounded linear maps.

  1. abbrev OAI.HochschildMatrixDilation.Mat line 17
  2. def OAI.HochschildMatrixDilation.diag line 19
  3. def OAI.HochschildMatrixDilation.offdiag line 21
  4. lemma OAI.HochschildMatrixDilation.diag_zero_zero line 23
  5. lemma OAI.HochschildMatrixDilation.diag_one_one line 25
  6. lemma OAI.HochschildMatrixDilation.diag_add line 27
  7. lemma OAI.HochschildMatrixDilation.diag_smul line 29
  8. lemma OAI.HochschildMatrixDilation.diag_mul line 31
  9. lemma OAI.HochschildMatrixDilation.star_diag line 34
  10. lemma OAI.HochschildMatrixDilation.star_offdiag line 37
  11. lemma OAI.HochschildMatrixDilation.offdiag_mul line 40
  12. def OAI.HochschildMatrixDilation.diagHom line 46
  13. lemma OAI.HochschildMatrixDilation.norm_diag_le line 59
  14. lemma OAI.HochschildMatrixDilation.offdiag_selfAdjoint line 63
  15. lemma OAI.HochschildMatrixDilation.offdiag_norm_le_one line 67
  16. def OAI.HochschildMatrixDilation.flipUnitary line 79
  17. def OAI.HochschildMatrixDilation.dilation line 84
  18. lemma OAI.HochschildMatrixDilation.dilation_sub_diag line 94
  19. lemma OAI.HochschildMatrixDilation.diagEntry_nonneg line 102
  20. def OAI.HochschildMatrixDilation.matrixTraceLinear line 110
  21. def OAI.HochschildMatrixDilation.matrixTrace line 118
  22. lemma OAI.HochschildMatrixDilation.matrixTrace_apply line 123
  23. lemma OAI.HochschildMatrixDilation.matrixTrace_diag line 126
  24. lemma OAI.HochschildMatrixDilation.matrixTrace_one line 129
  25. lemma OAI.HochschildMatrixDilation.matrixTrace_tracial line 133
  26. lemma OAI.HochschildMatrixDilation.matrixTrace_norm_sq line 140
  27. lemma OAI.HochschildMatrixDilation.matrixTrace_faithful line 151
  28. def OAI.HochschildMatrixDilation.matrixMap line 181
  29. lemma OAI.HochschildMatrixDilation.matrixMap_apply line 192
  30. lemma OAI.HochschildMatrixDilation.matrixMap_diag line 196
  31. lemma OAI.HochschildMatrixDilation.dilation_defect_nonneg line 200
  32. lemma OAI.HochschildMatrixDilation.dilation_error_sq line 209