OAI/Dynamics/StandardMap/Lyapunov/PlaneLyapunov.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.PlaneLyapunov.Growth line 15
2. lemma OAI.StandardMapEntropy.PlaneLyapunov.norm_pos line 18
3. lemma OAI.StandardMapEntropy.PlaneLyapunov.image_norm_pos line 21
4. lemma OAI.StandardMapEntropy.PlaneLyapunov.eventual_exp_lower line 29
5. def OAI.StandardMapEntropy.PlaneLyapunov.tailConstant line 38
6. lemma OAI.StandardMapEntropy.PlaneLyapunov.tailConstant_pos line 41
7. lemma OAI.StandardMapEntropy.PlaneLyapunov.stable_error_exp_bound line 46
8. lemma OAI.StandardMapEntropy.PlaneLyapunov.inverse_bound_by_exp line 82
9. lemma OAI.StandardMapEntropy.PlaneLyapunov.exists_stable_bound line 93
10. lemma OAI.StandardMapEntropy.PlaneLyapunov.all_growth_zero line 128
11. lemma OAI.StandardMapEntropy.PlaneLyapunov.stable_growth line 152
12. lemma OAI.StandardMapEntropy.PlaneLyapunov.growth_on_line line 204
13. lemma OAI.StandardMapEntropy.PlaneLyapunov.growth_off_line line 223
14. theorem OAI.StandardMapEntropy.PlaneLyapunov.positive_flag line 252