OAI/Dynamics/StandardMap/EndpointClasses.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.endpointLeft line 11
  2. def OAI.StandardMapEntropy.endpointRight line 12
  3. def OAI.StandardMapEntropy.leftRayClass line 13
  4. def OAI.StandardMapEntropy.rightRayClass line 14
  5. def OAI.StandardMapEntropy.twoRayClass line 15
  6. lemma OAI.StandardMapEntropy.measurable_endpointLeft line 16
  7. lemma OAI.StandardMapEntropy.measurable_endpointRight line 17
  8. lemma OAI.StandardMapEntropy.measurableSet_leftRayClass line 18
  9. lemma OAI.StandardMapEntropy.measurableSet_rightRayClass line 21
  10. lemma OAI.StandardMapEntropy.measurableSet_twoRayClass line 24
  11. lemma OAI.StandardMapEntropy.slowShape_dyadic line 28
  12. lemma OAI.StandardMapEntropy.leftRay_properties line 47
  13. lemma OAI.StandardMapEntropy.rightRay_properties line 59
  14. lemma OAI.StandardMapEntropy.twoRay_properties line 71