OAI/Analysis/IrrationalRotation/Operators/AffiliatedTransportSupplement.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.AffiliatedTransport.imageOn line 16
  2. def OAI.Invariant233.AffiliatedTransport.closedImageOn line 19
  3. instance OAI.Invariant233.AffiliatedTransport.(instance at line 22) line 22
  4. theorem OAI.Invariant233.AffiliatedTransport.mem_imageOn line 27
  5. theorem OAI.Invariant233.AffiliatedTransport.imageOn_le_closedImageOn line 31
  6. theorem OAI.Invariant233.AffiliatedTransport.image_mem_closedImageOn line 35
  7. theorem OAI.Invariant233.AffiliatedTransport.imageOn_invariant line 39
  8. theorem OAI.Invariant233.AffiliatedTransport.closedImageOn_invariant line 48
  9. theorem OAI.Invariant233.AffiliatedTransport.closedImageOn_invariant_of_commuting line 63
  10. theorem OAI.Invariant233.AffiliatedTransport.mem_orthogonal_closedImageOn line 71
  11. theorem OAI.Invariant233.AffiliatedTransport.inverse_imageOn_le_orthogonal line 80
  12. theorem OAI.Invariant233.AffiliatedTransport.inverse_closedImageOn_le_orthogonal line 97
  13. theorem OAI.Invariant233.AffiliatedTransport.orthogonal_invariant_of_inverse line 104
  14. theorem OAI.Invariant233.AffiliatedTransport.starProjection_commutes_of_reducing line 114
  15. theorem OAI.Invariant233.AffiliatedTransport.closedImageOn_map_eq line 125
  16. theorem OAI.Invariant233.AffiliatedTransport.closedImageOn_starProjection_commutes line 141
  17. theorem OAI.Invariant233.AffiliatedTransport.trace_eq_of_cutoff_estimates line 154