OAI/Analysis/BoundedHochschild/Frames.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal frames of partial isometries and maximal frame construction.

  1. def OAI.HochschildComparison.PartialIso.ofProjection line 21
  2. lemma OAI.HochschildComparison.PartialIso.ofProjection_coe line 24
  3. lemma OAI.HochschildComparison.PartialIso.ofProjection_initial line 27
  4. lemma OAI.HochschildComparison.PartialIso.ofProjection_final line 30
  5. lemma OAI.HochschildComparison.PartialIso.initial_ne_zero line 34
  6. lemma OAI.HochschildComparison.PartialIso.restrict_square line 40
  7. def OAI.HochschildComparison.PartialIso.restrict line 47
  8. lemma OAI.HochschildComparison.PartialIso.restrict_coe line 50
  9. lemma OAI.HochschildComparison.PartialIso.restrict_initial line 52
  10. lemma OAI.HochschildComparison.PartialIso.restrict_le line 54
  11. lemma OAI.HochschildComparison.projection_orthogonal_mono line 59
  12. structure OAI.HochschildComparison.Frame line 69
  13. lemma OAI.HochschildComparison.Frame.ext line 77
  14. def OAI.HochschildComparison.Frame.base line 81
  15. def OAI.HochschildComparison.Frame.support line 82
  16. lemma OAI.HochschildComparison.Frame.base_proj line 83
  17. lemma OAI.HochschildComparison.Frame.final_zero line 84
  18. lemma OAI.HochschildComparison.Frame.initial_eq line 89
  19. lemma OAI.HochschildComparison.Frame.support_proj line 90
  20. lemma OAI.HochschildComparison.Frame.final_le_support line 103
  21. lemma OAI.HochschildComparison.Frame.base_le_support line 112
  22. lemma OAI.HochschildComparison.Frame.support_le line 114
  23. instance OAI.HochschildComparison.Frame.(instance at line 120) line 120
  24. lemma OAI.HochschildComparison.Frame.zero_part line 121
  25. lemma OAI.HochschildComparison.Frame.zero_base line 122
  26. lemma OAI.HochschildComparison.Frame.zero_support line 123
  27. instance OAI.HochschildComparison.Frame.(instance at line 124) line 124
  28. instance OAI.HochschildComparison.Frame.(instance at line 125) line 125
  29. lemma OAI.HochschildComparison.Frame.zero_le line 129
  30. lemma OAI.HochschildComparison.Frame.base_mono line 130
  31. lemma OAI.HochschildComparison.Frame.eq_of_le_of_base_eq line 131
  32. lemma OAI.HochschildComparison.Frame.cross_final_zero line 139
  33. lemma OAI.HochschildComparison.Frame.cross_initial_zero line 143
  34. lemma OAI.HochschildComparison.Frame.support_orthogonal_symm line 148
  35. def OAI.HochschildComparison.Frame.orthogonalSum line 153
  36. lemma OAI.HochschildComparison.Frame.orthogonalSum_support line 163
  37. lemma OAI.HochschildComparison.Frame.orthogonalSum_base line 166
  38. lemma OAI.HochschildComparison.Frame.le_orthogonalSum line 170
  39. lemma OAI.HochschildComparison.Frame.exists_local line 190
  40. lemma OAI.HochschildComparison.Frame.le_of_comparable_trace_le line 269
  41. lemma OAI.HochschildComparison.Frame.chain_upper line 278
  42. theorem OAI.HochschildComparison.Frame.exists_full line 336