OAI/Analysis/BoundedHochschild/PartialUnitaries.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Partial unitaries, ordered limits and trace estimates.

  1. abbrev OAI.HochschildComparison.PartialUnitary line 35
  2. instance OAI.HochschildComparison.PartialUnitary.(instance at line 38) line 38
  3. instance OAI.HochschildComparison.PartialUnitary.(instance at line 39) line 39
  4. lemma OAI.HochschildComparison.PartialUnitary.ext line 43
  5. abbrev OAI.HochschildComparison.PartialUnitary.support line 45
  6. lemma OAI.HochschildComparison.PartialUnitary.support_proj line 46
  7. lemma OAI.HochschildComparison.PartialUnitary.norm_le_one line 47
  8. lemma OAI.HochschildComparison.PartialUnitary.star_mul_self_eq_support line 48
  9. lemma OAI.HochschildComparison.PartialUnitary.mul_star_self_eq_support line 49
  10. lemma OAI.HochschildComparison.PartialUnitary.mul_support line 50
  11. lemma OAI.HochschildComparison.PartialUnitary.support_mul line 51
  12. lemma OAI.HochschildComparison.PartialUnitary.star_support line 54
  13. lemma OAI.HochschildComparison.PartialUnitary.support_star line 56
  14. instance OAI.HochschildComparison.PartialUnitary.(instance at line 58) line 58
  15. lemma OAI.HochschildComparison.PartialUnitary.coe_zero line 59
  16. lemma OAI.HochschildComparison.PartialUnitary.support_zero line 60
  17. lemma OAI.HochschildComparison.PartialUnitary.zero_le line 63
  18. lemma OAI.HochschildComparison.PartialUnitary.orthogonal_symm line 71
  19. lemma OAI.HochschildComparison.PartialUnitary.mul_eq_zero line 73
  20. def OAI.HochschildComparison.PartialUnitary.orthogonalSum line 79
  21. lemma OAI.HochschildComparison.PartialUnitary.coe_orthogonalSum line 82
  22. lemma OAI.HochschildComparison.PartialUnitary.support_orthogonalSum line 84
  23. lemma OAI.HochschildComparison.PartialUnitary.le_orthogonalSum line 89
  24. def OAI.HochschildComparison.PartialUnitary.power line 97
  25. lemma OAI.HochschildComparison.PartialUnitary.norm_power_le_one line 99
  26. lemma OAI.HochschildComparison.PartialUnitary.support_power line 103
  27. lemma OAI.HochschildComparison.PartialUnitary.power_support line 108
  28. lemma OAI.HochschildComparison.PartialUnitary.add_pow_succ_of_orthogonal line 114
  29. lemma OAI.HochschildComparison.PartialUnitary.power_orthogonalSum line 123
  30. lemma OAI.HochschildComparison.PartialUnitary.power_tendsto line 138
  31. lemma OAI.HochschildComparison.PartialUnitary.exists_monotone_limit line 171
  32. lemma OAI.HochschildComparison.PartialUnitary.chain_limit line 187
  33. lemma OAI.HochschildComparison.PartialUnitary.maximal_of_sequentially_closed line 227
  34. lemma OAI.HochschildPatching.norm_trace_mul_le_gns line 254
  35. lemma OAI.HochschildPatching.projection_gns_sq line 261
  36. lemma OAI.HochschildPatching.small_compression_trace_bound line 267