OAI/Analysis/BoundedHochschild/PartialIsometries.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Partial isometries and comparison of equal-trace projections.

  1. structure OAI.HochschildComparison.PartialIso line 34
  2. instance OAI.HochschildComparison.PartialIso.(instance at line 39) line 39
  3. lemma OAI.HochschildComparison.PartialIso.ext line 40
  4. def OAI.HochschildComparison.PartialIso.initial line 43
  5. def OAI.HochschildComparison.PartialIso.final line 44
  6. lemma OAI.HochschildComparison.PartialIso.mul_initial line 45
  7. lemma OAI.HochschildComparison.PartialIso.final_mul line 47
  8. lemma OAI.HochschildComparison.PartialIso.initial_proj line 48
  9. lemma OAI.HochschildComparison.PartialIso.final_proj line 54
  10. lemma OAI.HochschildComparison.PartialIso.norm_le_one line 60
  11. instance OAI.HochschildComparison.PartialIso.(instance at line 68) line 68
  12. lemma OAI.HochschildComparison.PartialIso.le_def line 69
  13. instance OAI.HochschildComparison.PartialIso.(instance at line 73) line 73
  14. lemma OAI.HochschildComparison.PartialIso.initial_mono line 90
  15. lemma OAI.HochschildComparison.PartialIso.mul_initial_of_le line 92
  16. lemma OAI.HochschildComparison.PartialIso.star_mul_of_le line 93
  17. lemma OAI.HochschildComparison.PartialIso.star_mul_of_ge line 100
  18. lemma OAI.HochschildComparison.PartialIso.final_mono line 103
  19. lemma OAI.HochschildComparison.PartialIso.diff_square line 110
  20. instance OAI.HochschildComparison.PartialIso.(instance at line 117) line 117
  21. lemma OAI.HochschildComparison.PartialIso.coe_zero line 119
  22. lemma OAI.HochschildComparison.PartialIso.initial_zero line 121
  23. lemma OAI.HochschildComparison.PartialIso.final_zero line 123
  24. lemma OAI.HochschildComparison.PartialIso.zero_le line 124
  25. lemma OAI.HochschildComparison.PartialIso.star_mul_eq_zero_of_final_orthogonal line 130
  26. lemma OAI.HochschildComparison.PartialIso.mul_star_eq_zero_of_initial_orthogonal line 141
  27. lemma OAI.HochschildComparison.PartialIso.orthogonal_initial_symm line 152
  28. lemma OAI.HochschildComparison.PartialIso.orthogonal_final_symm line 156
  29. def OAI.HochschildComparison.PartialIso.orthogonalSum line 161
  30. lemma OAI.HochschildComparison.PartialIso.orthogonalSum_initial line 173
  31. lemma OAI.HochschildComparison.PartialIso.orthogonalSum_final line 178
  32. lemma OAI.HochschildComparison.PartialIso.le_orthogonalSum line 185
  33. lemma OAI.HochschildComparison.PartialIso.eq_of_le_of_initial_eq line 218
  34. lemma OAI.HochschildComparison.PartialIso.le_of_comparable_trace_le line 226
  35. lemma OAI.HochschildComparison.PartialIso.diff_gns_sq line 235
  36. lemma OAI.HochschildComparison.PartialIso.monotone_gns_cauchy line 241
  37. lemma OAI.HochschildComparison.PartialIso.exists_monotone_limit line 259
  38. lemma OAI.HochschildComparison.PartialIso.chain_upper line 305
  39. lemma OAI.HochschildComparison.exists_nonzero_corner line 356
  40. lemma OAI.HochschildComparison.partialIso_of_nonzero_corner line 395
  41. lemma OAI.HochschildComparison.projection_orthogonal_of_le_sub line 431
  42. theorem OAI.HochschildComparison.exists_partialIso_of_equal_trace line 444