OAI/Dynamics/StandardMap/TorusDynamics.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.torusStep line 11
  2. lemma OAI.StandardMapEntropy.torusStep_apply line 16
  3. lemma OAI.StandardMapEntropy.torusStep_symm_apply line 17
  4. lemma OAI.StandardMapEntropy.continuous_torusStep line 19
  5. lemma OAI.StandardMapEntropy.continuous_torusStep_symm line 21
  6. lemma OAI.StandardMapEntropy.measurePreserving_recurrenceCoordinates line 23
  7. lemma OAI.StandardMapEntropy.measurePreserving_torusStep line 28
  8. def OAI.StandardMapEntropy.torusStep_measurableEquiv line 35
  9. lemma OAI.StandardMapEntropy.measurePreserving_torusStep_symm line 39
  10. def OAI.StandardMapEntropy.torusIter line 41
  11. lemma OAI.StandardMapEntropy.torusIter_add line 42
  12. lemma OAI.StandardMapEntropy.torusIter_zero line 45
  13. lemma OAI.StandardMapEntropy.continuous_torusIter line 46
  14. lemma OAI.StandardMapEntropy.measurePreserving_torusIter line 53
  15. lemma OAI.StandardMapEntropy.coe_phi line 60
  16. lemma OAI.StandardMapEntropy.liftProjection_step line 63
  17. lemma OAI.StandardMapEntropy.liftProjection_step_symm line 70
  18. lemma OAI.StandardMapEntropy.liftProjection_iter line 74
  19. lemma OAI.StandardMapEntropy.liftProjection_surjective line 83