OAI/Dynamics/StandardMap/Holonomy/ConeIntervalDistortion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.trapped_affine_derivative line 14
2. theorem OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.affine_interval_distortion line 38
3. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.pair_norm_eq_snd line 88
4. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.exists_orbit_escape line 94
5. lemma OAI.StandardMapEntropy.NonlinearStable.last_trapped_time line 113
6. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.escape_vertical_lower line 128
7. lemma OAI.StandardMapEntropy.NonlinearStable.terminal_size_comparison line 146
8. lemma OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.affine_interval_abs_distortion line 167
9. lemma OAI.StandardMapEntropy.NonlinearStable.relative_interval_ratio line 191
10. theorem OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.finite_holonomy_ratio line 200
11. lemma OAI.StandardMapEntropy.NonlinearStable.eventually_scaled_power_small line 229
12. theorem OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.holonomy_local_bound line 239
13. lemma OAI.StandardMapEntropy.fine_trueOrbit line 340
14. theorem OAI.StandardMapEntropy.fineTrapped_hasDerivAt_log_distortion line 349
15. lemma OAI.StandardMapEntropy.fineInverse_forward_bound line 391
16. lemma OAI.StandardMapEntropy.fineCoordinate_tracking_rate line 400
17. theorem OAI.StandardMapEntropy.fine_extended_step_bound line 421