OAI/Analysis/IrrationalRotation/Couplings/ProductCouplingCircle.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.OrderedProductCoupling.baseLaw_eq_restrict line 16
  2. lemma OAI.Invariant233.OrderedProductCoupling.circleEndpoint_measurable line 19
  3. lemma OAI.Invariant233.OrderedProductCoupling.realEndpoint_measurable line 23
  4. lemma OAI.Invariant233.OrderedProductCoupling.measurePreserving_circleQuotient line 29
  5. lemma OAI.Invariant233.OrderedProductCoupling.measurePreserving_circleEndpoint line 37
  6. lemma OAI.Invariant233.OrderedProductCoupling.measurePreserving_realEndpoint line 46
  7. lemma OAI.Invariant233.OrderedProductCoupling.circleEndpoint_realEndpoint line 59
  8. lemma OAI.Invariant233.OrderedProductCoupling.realEndpoint_circleEndpoint_of_mem line 64
  9. lemma OAI.Invariant233.OrderedProductCoupling.ae_realEndpoint_circleEndpoint line 69
  10. theorem OAI.Invariant233.OrderedProductCoupling.circle_density_transport line 78
  11. lemma OAI.Invariant233.OrderedProductCoupling.circleHybridEndpoint_measurable line 86
  12. lemma OAI.Invariant233.OrderedProductCoupling.circleLeftEndpoint_measurable line 90
  13. lemma OAI.Invariant233.OrderedProductCoupling.circleRightEndpoint_measurable line 93
  14. instance OAI.Invariant233.OrderedProductCoupling.circlePairLaw_probability line 96
  15. theorem OAI.Invariant233.OrderedProductCoupling.exists_circle_hybrid_density line 100
  16. theorem OAI.Invariant233.OrderedProductCoupling.leftEndpoint_ae_mem_unit line 122
  17. theorem OAI.Invariant233.OrderedProductCoupling.rightEndpoint_ae_mem_unit line 133
  18. theorem OAI.Invariant233.OrderedProductCoupling.ae_real_circle_endpoints line 144
  19. theorem OAI.Invariant233.OrderedProductCoupling.ae_circle_endpoints_ordered line 150
  20. theorem OAI.Invariant233.OrderedProductCoupling.circlePairLaw_fst line 157
  21. theorem OAI.Invariant233.OrderedProductCoupling.circlePairLaw_snd line 163
  22. theorem OAI.Invariant233.OrderedProductCoupling.circlePairLaw_ordered line 169