OAI/Analysis/RotationWeights/Polar.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CirclePolar.Op line 31
  2. def OAI.CirclePolar.absOp line 33
  3. lemma OAI.CirclePolar.absOp_selfAdjoint line 35
  4. lemma OAI.CirclePolar.absOp_square line 38
  5. lemma OAI.CirclePolar.norm_absOp line 41
  6. def OAI.CirclePolar.closedRange line 50
  7. instance OAI.CirclePolar.(instance at line 52) line 52
  8. def OAI.CirclePolar.intoRange line 55
  9. lemma OAI.CirclePolar.intoRange_dense line 59
  10. def OAI.CirclePolar.polarCore line 66
  11. lemma OAI.CirclePolar.polarCore_abs line 69
  12. lemma OAI.CirclePolar.polarCore_norm line 76
  13. def OAI.CirclePolar.polar line 84
  14. lemma OAI.CirclePolar.polar_abs line 87
  15. lemma OAI.CirclePolar.polar_norm line 94
  16. def OAI.CirclePolar.polarCoreIsometry line 100
  17. lemma OAI.CirclePolar.polar_star_mul line 104
  18. lemma OAI.CirclePolar.ker_absOp line 117
  19. lemma OAI.CirclePolar.closedRange_absOp line 122
  20. lemma OAI.CirclePolar.polar_eq_zero_iff line 128
  21. lemma OAI.CirclePolar.commute_absOp line 133
  22. lemma OAI.CirclePolar.commute_polar line 137
  23. lemma OAI.CirclePolar.polar_norm_le line 172
  24. lemma OAI.CirclePolar.polar_opNorm_le line 176
  25. lemma OAI.CirclePolar.polar_range line 180
  26. lemma OAI.CirclePolar.polar_range_le line 199
  27. lemma OAI.CirclePolar.polar_adjoint_annihilates line 207
  28. lemma OAI.CirclePolar.disjoint_norm_bound line 219
  29. lemma OAI.CirclePolar.exists_intersection_of_norm_lt line 258