OAI/Analysis/TracialCohomology/CornerComparison.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Corner comparison for bounded Hochschild cohomology.

  1. theorem OAI.PopaCorners.connecting_corner line 28
  2. theorem OAI.PopaCorners.corner_polar line 72
  3. theorem OAI.PopaCorners.nonzero_partial_isometry line 98
  4. structure OAI.PopaCorners.CornerIso line 119
  5. instance OAI.PopaCorners.CornerIso.(instance at line 128) line 128
  6. theorem OAI.PopaCorners.CornerIso.ext line 131
  7. def OAI.PopaCorners.CornerIso.initial line 134
  8. def OAI.PopaCorners.CornerIso.final line 135
  9. lemma OAI.PopaCorners.CornerIso.initial_proj line 138
  10. lemma OAI.PopaCorners.CornerIso.final_proj line 140
  11. lemma OAI.PopaCorners.CornerIso.mul_initial line 148
  12. lemma OAI.PopaCorners.CornerIso.final_mul line 150
  13. lemma OAI.PopaCorners.CornerIso.norm_le_one line 154
  14. instance OAI.PopaCorners.CornerIso.(instance at line 159) line 159
  15. lemma OAI.PopaCorners.CornerIso.le_def line 175
  16. lemma OAI.PopaCorners.CornerIso.initial_mono line 178
  17. lemma OAI.PopaCorners.CornerIso.mul_initial_of_le line 179
  18. lemma OAI.PopaCorners.CornerIso.star_mul_of_le line 182
  19. lemma OAI.PopaCorners.CornerIso.star_mul_of_ge line 191
  20. lemma OAI.PopaCorners.CornerIso.sub_star_mul line 196
  21. lemma OAI.PopaCorners.CornerIso.final_mono line 202
  22. def OAI.PopaCorners.CornerIso.rank line 209
  23. lemma OAI.PopaCorners.CornerIso.rank_mono line 211
  24. lemma OAI.PopaCorners.CornerIso.gns_sub_sq line 215
  25. lemma OAI.PopaCorners.CornerIso.le_of_comparable_rank_le line 220
  26. lemma OAI.PopaCorners.CornerIso.monotone_cauchy line 232
  27. lemma OAI.PopaCorners.CornerIso.projection_mul_zero_of_le_sub line 251
  28. lemma OAI.PopaCorners.CornerIso.add_orthogonal line 262
  29. lemma OAI.PopaCorners.CornerIso.rank_tendsto line 329
  30. theorem OAI.PopaCorners.CornerIso.monotone_limit line 341
  31. theorem OAI.PopaCorners.CornerIso.chain_upper line 390
  32. def OAI.PopaCorners.CornerIso.zero line 424
  33. lemma OAI.PopaCorners.CornerIso.exists_maximal line 430
  34. theorem OAI.PopaCorners.CornerIso.maximal_fills line 441
  35. theorem OAI.PopaCorners.CornerIso.exists_full_initial line 463
  36. theorem OAI.PopaCorners.CornerIso.equivalent_of_trace_eq line 481