OAI/Dynamics/StandardMap/Holonomy/FiniteOrbitDecay.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.stable_cone_backward line 13
  2. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.stable_orbit_bound line 39
  3. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.unstable_orbit_bound line 48
  4. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_tail line 58
  5. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_two_ended line 66
  6. lemma OAI.StandardMapEntropy.NonlinearStable.geometric_partial_bound line 78
  7. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_sum_norm line 84
  8. lemma OAI.StandardMapEntropy.NonlinearStable.scalar_log_relative_error line 113
  9. theorem OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.linearized_log_distortion line 146
  10. def OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trueOrbit line 187
  11. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trueOrbit_eq_extend line 191
  12. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trueOrbit_hasDerivAt line 198
  13. lemma OAI.StandardMapEntropy.NonlinearStable.continuous_injective_abs_sub_le line 238
  14. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.transverse_injective line 249
  15. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.transverse_between line 257
  16. theorem OAI.StandardMapEntropy.NonlinearStable.Recurrence.transverse_interval_trapped line 265
  17. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trueOrbit_continuous line 293
  18. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trapped_transverse_derivative line 301
  19. lemma OAI.StandardMapEntropy.NonlinearStable.exp_bounds_of_log_error line 324
  20. theorem OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.transverse_interval_distortion line 334
  21. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_pair_cone line 378
  22. lemma OAI.StandardMapEntropy.NonlinearStable.affine_cone line 389
  23. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.affine_transverse_injective line 398
  24. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.affine_interval_trapped line 409
  25. theorem OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.linearized_cone_log_distortion line 433
  26. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trueOrbit_affine_hasDerivAt line 473