OAI/Analysis/RotationWeights/Transport.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CircleTransport.Op line 32
  2. lemma OAI.CircleTransport.commute_projection_of_reducing line 34
  3. lemma OAI.CircleTransport.invariant_closure line 51
  4. lemma OAI.CircleTransport.commutes_star_centralizer line 59
  5. lemma OAI.CircleTransport.projection_mem_centralizer line 66
  6. lemma OAI.CircleTransport.polar_mem_centralizer line 72
  7. lemma OAI.CircleTransport.exists_cutoff_intersection line 78
  8. def OAI.CircleTransport.transportedRange line 99
  9. instance OAI.CircleTransport.(instance at line 102) line 102
  10. lemma OAI.CircleTransport.transportedRange_invariant line 106
  11. lemma OAI.CircleTransport.transportedRange_mem_centralizer line 115
  12. lemma OAI.CircleTransport.transportedRange_ne_bot line 126
  13. lemma OAI.CircleTransport.transportedRange_ne_top line 138
  14. lemma OAI.CircleTransport.projection_ne_zero_of_ne_bot line 159
  15. lemma OAI.CircleTransport.projection_ne_one_of_ne_top line 168
  16. lemma OAI.CircleTransport.invariant_projection line 178
  17. theorem OAI.CircleTransport.affiliated_transport line 184
  18. def OAI.CircleTransport.fractionMap line 235
  19. lemma OAI.CircleTransport.fractionMap_apply line 239
  20. lemma OAI.CircleTransport.fractionMap_injective line 244
  21. lemma OAI.CircleTransport.fractionMap_range line 247
  22. lemma OAI.CircleTransport.fractionMap_symmetric line 255
  23. lemma OAI.CircleTransport.fraction_domain_map line 272
  24. lemma OAI.CircleTransport.fractionMap_intertwine line 277
  25. theorem OAI.CircleTransport.bounded_fraction_transport line 289