OAI/Analysis/TracialCohomology/Expectations.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Expectations for bounded Hochschild cohomology.

  1. lemma OAI.PopaMatrices.System.diagonal_projection line 25
  2. lemma OAI.PopaMatrices.System.entry_absorb_left line 30
  3. lemma OAI.PopaMatrices.System.entry_absorb_right line 34
  4. lemma OAI.PopaMatrices.System.entry_norm_le line 38
  5. def OAI.PopaMatrices.System.commutant line 45
  6. lemma OAI.PopaMatrices.System.mem_commutant line 59
  7. def OAI.PopaMatrices.System.coordinate line 61
  8. lemma OAI.PopaMatrices.System.coordinate_commutes line 64
  9. lemma OAI.PopaMatrices.System.coordinate_mem line 74
  10. lemma OAI.PopaMatrices.System.reconstruct line 78
  11. lemma OAI.PopaMatrices.System.central_in_commutant_is_central line 91
  12. def OAI.PopaMatrices.System.sumExpect line 100
  13. lemma OAI.PopaMatrices.System.sumExpect_commutes line 103
  14. lemma OAI.PopaMatrices.System.sumExpect_of_commutes line 112
  15. lemma OAI.PopaMatrices.System.sumExpect_star line 126
  16. def OAI.PopaMatrices.System.expect line 129
  17. lemma OAI.PopaMatrices.System.expect_mem line 132
  18. lemma OAI.PopaMatrices.System.expect_fix line 137
  19. lemma OAI.PopaMatrices.System.expect_idempotent line 142
  20. lemma OAI.PopaMatrices.System.expect_one line 146
  21. lemma OAI.PopaMatrices.System.expect_add line 149
  22. lemma OAI.PopaMatrices.System.expect_smul line 153
  23. lemma OAI.PopaMatrices.System.expect_star line 158
  24. lemma OAI.PopaMatrices.System.expect_bimodule line 162
  25. lemma OAI.PopaMatrices.System.trace_sumExpect line 176
  26. lemma OAI.PopaMatrices.System.trace_expect line 189
  27. lemma OAI.PopaMatrices.System.expect_zero line 207
  28. lemma OAI.PopaMatrices.System.expect_sub line 209
  29. lemma OAI.PopaMatrices.System.expect_pairing line 214
  30. lemma OAI.PopaMatrices.System.expect_orthogonal line 220
  31. lemma OAI.PopaMatrices.System.expect_pythagoras line 226
  32. lemma OAI.PopaMatrices.System.expect_norm_le line 232
  33. lemma OAI.PopaMatrices.System.commutator_norm_le_residual line 237
  34. lemma OAI.PopaMatrices.System.energy_drop line 250