OAI/Dynamics/StandardMap/Lyapunov/HyperbolicSet.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.MainContinuationObligation line 12
  2. def OAI.StandardMapEntropy.hyperbolicRegion line 31
  3. lemma OAI.StandardMapEntropy.measurableSet_hyperbolicRegion line 34
  4. lemma OAI.StandardMapEntropy.preimage_hyperbolicRegion line 38
  5. lemma OAI.StandardMapEntropy.normalizedArea_probability line 43
  6. lemma OAI.StandardMapEntropy.normalizedArea_absolutelyContinuous line 50
  7. lemma OAI.StandardMapEntropy.normalizedArea_ae_mem line 53
  8. lemma OAI.StandardMapEntropy.normalizedArea_integrable line 57
  9. lemma OAI.StandardMapEntropy.measurePreserving_normalizedArea line 61
  10. theorem OAI.StandardMapEntropy.hyperbolic_probability_of_deficit line 68
  11. lemma OAI.StandardMapEntropy.measurePreserving_torusSwap line 100
  12. lemma OAI.StandardMapEntropy.torusIter_neg_nat_apply line 103
  13. lemma OAI.StandardMapEntropy.transfer_lowerRate_inverse_iterate line 108
  14. lemma OAI.StandardMapEntropy.transfer_average_reverse line 120
  15. lemma OAI.StandardMapEntropy.transfer_lowerRate_swap_ae line 127
  16. lemma OAI.StandardMapEntropy.transferLyapunov_swap_ae line 184
  17. lemma OAI.StandardMapEntropy.ae_transfer_inverse_rate line 189