OAI/Analysis/IrrationalRotation/Spectral/GeneralPolar.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.GeneralPolar.norm_abs_apply line 16
  2. def OAI.Invariant233.GeneralPolar.closedRange line 27
  3. instance OAI.Invariant233.GeneralPolar.(instance at line 29) line 29
  4. def OAI.Invariant233.GeneralPolar.toClosedRange line 32
  5. lemma OAI.Invariant233.GeneralPolar.toClosedRange_dense line 36
  6. def OAI.Invariant233.GeneralPolar.rangeIsometryMap line 45
  7. lemma OAI.Invariant233.GeneralPolar.rangeIsometryMap_apply line 48
  8. lemma OAI.Invariant233.GeneralPolar.rangeIsometryMap_norm line 56
  9. def OAI.Invariant233.GeneralPolar.rangeIsometry line 66
  10. lemma OAI.Invariant233.GeneralPolar.rangeIsometryMap_mem line 70
  11. lemma OAI.Invariant233.GeneralPolar.rangeIsometryMap_adjoint_comp line 81
  12. lemma OAI.Invariant233.GeneralPolar.rangeIsometryMap_comp_adjoint line 87
  13. def OAI.Invariant233.GeneralPolar.partialIsometry line 108
  14. lemma OAI.Invariant233.GeneralPolar.partialIsometry_apply line 111
  15. lemma OAI.Invariant233.GeneralPolar.partialIsometry_initial line 119
  16. lemma OAI.Invariant233.GeneralPolar.partialIsometry_final line 131
  17. lemma OAI.Invariant233.GeneralPolar.partialIsometry_right_support line 148
  18. lemma OAI.Invariant233.GeneralPolar.eq_on_closedRange line 159
  19. lemma OAI.Invariant233.GeneralPolar.eq_of_right_support line 166
  20. lemma OAI.Invariant233.GeneralPolar.partialIsometry_commute line 177
  21. lemma OAI.Invariant233.GeneralPolar.closedRange_projection_mem line 195
  22. lemma OAI.Invariant233.GeneralPolar.partialIsometry_mem line 209
  23. lemma OAI.Invariant233.GeneralPolar.abs_mem line 221
  24. lemma OAI.Invariant233.GeneralPolar.ker_abs line 231
  25. lemma OAI.Invariant233.GeneralPolar.closedRange_abs line 236
  26. def OAI.Invariant233.GeneralPolar.polar line 242
  27. lemma OAI.Invariant233.GeneralPolar.polar_mul_abs line 244
  28. lemma OAI.Invariant233.GeneralPolar.polar_initial line 248
  29. lemma OAI.Invariant233.GeneralPolar.polar_final line 252
  30. lemma OAI.Invariant233.GeneralPolar.polar_mem line 256
  31. theorem OAI.Invariant233.GeneralPolar.trace_support_eq line 260