OAI/Analysis/TracialCohomology/MatrixExtensions.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Matrix extensions for bounded Hochschild cohomology.

  1. lemma OAI.PopaQuantization.commutator_difference_bound line 28
  2. theorem OAI.PopaQuantization.exists_matrix_energy_decrease line 45
  3. lemma OAI.PopaMatrices.System.sum_product_index line 74
  4. def OAI.PopaMatrices.System.tensor line 79
  5. lemma OAI.PopaMatrices.System.tensor_entry line 108
  6. lemma OAI.PopaMatrices.System.tensor_sumExpect line 118
  7. lemma OAI.PopaMatrices.System.tensor_expect line 135
  8. lemma OAI.PopaMatrices.System.left_mul_coordinate line 152
  9. lemma OAI.PopaMatrices.System.coordinate_zero line 158
  10. lemma OAI.PopaMatrices.System.coordinate_sub line 162
  11. lemma OAI.PopaMatrices.System.coordinate_star line 167
  12. lemma OAI.PopaMatrices.System.coordinate_mul line 172
  13. lemma OAI.PopaMatrices.System.extract_coordinate line 189
  14. lemma OAI.PopaMatrices.System.coordinate_of_commutes line 195
  15. lemma OAI.PopaMatrices.System.coordinate_projection line 205
  16. theorem OAI.PopaMatrices.System.commutant_subprojection line 214
  17. def OAI.PopaMatrices.closedCommutant line 258
  18. instance OAI.PopaMatrices.closedCommutant_closed line 262
  19. lemma OAI.PopaMatrices.mem_closedCommutant line 268
  20. lemma OAI.PopaMatrices.closedCommutant_subset line 272
  21. lemma OAI.PopaMatrices.closedCommutant_factor line 307
  22. lemma OAI.PopaMatrices.closedCommutant_diffuse line 318
  23. def OAI.PopaMatrices.System.map line 341
  24. lemma OAI.PopaMatrices.System.map_entry line 349
  25. lemma OAI.PopaMatrices.System.map_expect line 352
  26. lemma OAI.PopaMatrices.preGNS_norm_eq_of_trace line 366
  27. theorem OAI.PopaMatrices.extend_energy_decrease line 377