OAI/Dynamics/StandardMap/TorusObservations.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.cosine_periodic line 11

    Also declared: ComparatorChallenges/StandardMapComponents.lean:29 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:47 (same declaration text).

  2. def OAI.StandardMapEntropy.cosine line 16

    Also declared: ComparatorChallenges/StandardMapComponents.lean:34 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:52 (same declaration text).

  3. lemma OAI.StandardMapEntropy.cosine_coe line 17
  4. lemma OAI.StandardMapEntropy.continuous_cosine line 19
  5. def OAI.StandardMapEntropy.torusPotential line 24

    Also declared: ComparatorChallenges/StandardMapComponents.lean:36 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:54 (same declaration text).

  6. lemma OAI.StandardMapEntropy.torusPotential_coe line 25
  7. lemma OAI.StandardMapEntropy.continuous_torusPotential line 26
  8. def OAI.StandardMapEntropy.torusSegmentCoefficient line 28
  9. def OAI.StandardMapEntropy.torusSegmentTransfer line 30
  10. def OAI.StandardMapEntropy.torusShortfall line 32
  11. lemma OAI.StandardMapEntropy.torusSegmentCoefficient_lift line 34
  12. lemma OAI.StandardMapEntropy.torusSegmentTransfer_lift line 39
  13. lemma OAI.StandardMapEntropy.torusShortfall_lift line 45
  14. lemma OAI.StandardMapEntropy.continuous_torusSegmentCoefficient line 48
  15. lemma OAI.StandardMapEntropy.continuous_torusSegmentTransfer line 51
  16. lemma OAI.StandardMapEntropy.torusSegmentTransfer_norm_bounds line 55
  17. lemma OAI.StandardMapEntropy.continuous_torusShortfall line 60
  18. lemma OAI.StandardMapEntropy.torusShortfall_mem line 66
  19. lemma OAI.StandardMapEntropy.torusShortfall_shift line 71
  20. lemma OAI.StandardMapEntropy.shortfall_observation_transport line 80
  21. lemma OAI.StandardMapEntropy.continuous_shortfall_observation line 106