OAI/Dynamics/StandardMap/Holonomy/FineStableGeometry.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.fineStableGraph line 13
  2. def OAI.StandardMapEntropy.fineStableCurve line 16
  3. lemma OAI.StandardMapEntropy.fineStableCurve_zero line 19
  4. lemma OAI.StandardMapEntropy.fineStableCurve_orbit line 26
  5. lemma OAI.StandardMapEntropy.fineStableCoordinate line 42
  6. lemma OAI.StandardMapEntropy.fineStableCurve_contraction line 51
  7. lemma OAI.StandardMapEntropy.fineStableGraph_contDiffOn line 66
  8. lemma OAI.StandardMapEntropy.fineStableCurve_contDiffOn line 76
  9. theorem OAI.StandardMapEntropy.fineStableCurve_unique line 82
  10. lemma OAI.StandardMapEntropy.slow_sequence_ratio line 117
  11. lemma OAI.StandardMapEntropy.fineInverse_forward_radius_bound line 125
  12. lemma OAI.StandardMapEntropy.fineCoordinate_tracking_difference line 144
  13. lemma OAI.StandardMapEntropy.fineStableCoordinate_bound line 173
  14. theorem OAI.StandardMapEntropy.fineStablePlaque_overlap line 181
  15. lemma OAI.StandardMapEntropy.measurable_compact_continuity_block line 238
  16. abbrev OAI.StandardMapEntropy.LyapunovChartData line 284
  17. def OAI.StandardMapEntropy.lyapunovChartData line 285
  18. def OAI.StandardMapEntropy.orbitChartData line 287
  19. lemma OAI.StandardMapEntropy.measurable_lyapunovChartData line 290
  20. lemma OAI.StandardMapEntropy.measurable_orbitChartData line 293
  21. theorem OAI.StandardMapEntropy.compact_fineRegular_block line 298
  22. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.perronApprox line 335
  23. lemma OAI.StandardMapEntropy.NonlinearStable.perronApprox_eq_iterate line 340
  24. lemma OAI.StandardMapEntropy.NonlinearStable.perronApprox_error line 348
  25. lemma OAI.StandardMapEntropy.NonlinearStable.continuous_perronApprox line 364
  26. theorem OAI.StandardMapEntropy.NonlinearStable.continuous_solution_eval_on_strip line 380
  27. lemma OAI.StandardMapEntropy.continuous_complexProjection line 413
  28. lemma OAI.StandardMapEntropy.continuous_liftRemainder line 416
  29. lemma OAI.StandardMapEntropy.continuous_fineFrame_of_data line 421
  30. lemma OAI.StandardMapEntropy.continuous_fineInverse_of_data line 425
  31. theorem OAI.StandardMapEntropy.continuous_fineStableCurve_family line 431