OAI/Analysis/IrrationalRotation/Model/ProductCoupling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Invariant233.OrderedProductCoupling.Parameters line 11
  2. abbrev OAI.Invariant233.OrderedProductCoupling.CoordinateSample line 27
  3. abbrev OAI.Invariant233.OrderedProductCoupling.Sample line 28
  4. abbrev OAI.Invariant233.OrderedProductCoupling.Endpoint line 29
  5. def OAI.Invariant233.OrderedProductCoupling.coordinateLaw line 31
  6. def OAI.Invariant233.OrderedProductCoupling.law line 34
  7. def OAI.Invariant233.OrderedProductCoupling.baseMeasure line 37
  8. def OAI.Invariant233.OrderedProductCoupling.leftEndpoint line 40
  9. def OAI.Invariant233.OrderedProductCoupling.rightEndpoint line 42
  10. def OAI.Invariant233.OrderedProductCoupling.hybridEndpoint line 44
  11. def OAI.Invariant233.OrderedProductCoupling.marginalDensity line 47
  12. def OAI.Invariant233.OrderedProductCoupling.energyBound line 51