OAI/Dynamics/StandardMap/Lyapunov/InverseLyapunov.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.standardReversal line 12
  2. def OAI.StandardMapEntropy.tangentReversal line 15
  3. lemma OAI.StandardMapEntropy.standardReversal_fst line 18
  4. lemma OAI.StandardMapEntropy.standardReversal_snd line 19
  5. lemma OAI.StandardMapEntropy.tangentReversal_re line 21
  6. lemma OAI.StandardMapEntropy.tangentReversal_im line 22
  7. lemma OAI.StandardMapEntropy.tangentReversal_involutive line 24
  8. lemma OAI.StandardMapEntropy.standardReversal_inverseMap line 27
  9. lemma OAI.StandardMapEntropy.standardReversal_inverse_iterate line 35
  10. lemma OAI.StandardMapEntropy.measurePreserving_standardReversal line 43
  11. lemma OAI.StandardMapEntropy.standardInverseDerivative_conjugate line 47
  12. def OAI.StandardMapEntropy.standardInverseDerivativeProduct line 58
  13. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_area line 63
  14. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_conjugate line 69
  15. lemma OAI.StandardMapEntropy.complexProjection_inverse_iterate line 84
  16. lemma OAI.StandardMapEntropy.hasFDerivAt_standardInverseLift_iterate line 92
  17. lemma OAI.StandardMapEntropy.tangentReversal_conjugate_norm_le line 102
  18. lemma OAI.StandardMapEntropy.inverse_derivative_log_difference_bound line 119
  19. lemma OAI.StandardMapEntropy.standardLyapunov_reversal_ae line 144
  20. lemma OAI.StandardMapEntropy.ae_standardInverseLyapunov_rate line 154
  21. lemma OAI.StandardMapEntropy.standardInverseDerivative_norm_bound line 173
  22. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_step_lower line 181
  23. theorem OAI.StandardMapEntropy.ae_inverse_hyperbolic_flag line 188
  24. abbrev OAI.StandardMapEntropy.PlaneLyapunov.UnitPlane line 209
  25. instance OAI.StandardMapEntropy.PlaneLyapunov.(instance at line 210) line 210
  26. def OAI.StandardMapEntropy.PlaneLyapunov.denseUnit line 212
  27. lemma OAI.StandardMapEntropy.PlaneLyapunov.exists_approx_slow line 214
  28. def OAI.StandardMapEntropy.PlaneLyapunov.approxSlow line 224
  29. lemma OAI.StandardMapEntropy.PlaneLyapunov.approxSlow_unit line 227
  30. lemma OAI.StandardMapEntropy.PlaneLyapunov.approxSlow_bound line 230
  31. lemma OAI.StandardMapEntropy.PlaneLyapunov.measurable_approxSlow line 233
  32. lemma OAI.StandardMapEntropy.PlaneLyapunov.unit_sq line 244
  33. lemma OAI.StandardMapEntropy.PlaneLyapunov.unit_projection_difference line 249
  34. lemma OAI.StandardMapEntropy.PlaneLyapunov.norm_tendsto_zero_of_negative_growth line 267
  35. lemma OAI.StandardMapEntropy.PlaneLyapunov.approxSlow_wedge_tendsto_zero line 281
  36. lemma OAI.StandardMapEntropy.PlaneLyapunov.approxSlow_projection_tendsto line 295
  37. def OAI.StandardMapEntropy.PlaneLyapunov.stableCandidate line 319
  38. lemma OAI.StandardMapEntropy.PlaneLyapunov.stableCandidate_ne_zero line 325
  39. lemma OAI.StandardMapEntropy.PlaneLyapunov.stableCandidate_wedge line 335
  40. def OAI.StandardMapEntropy.PlaneLyapunov.stableUnit line 349
  41. lemma OAI.StandardMapEntropy.PlaneLyapunov.norm_stableUnit line 353
  42. lemma OAI.StandardMapEntropy.PlaneLyapunov.measurable_stableCandidate line 358
  43. lemma OAI.StandardMapEntropy.PlaneLyapunov.measurable_stableUnit line 373
  44. theorem OAI.StandardMapEntropy.PlaneLyapunov.stableUnit_growth line 380
  45. lemma OAI.StandardMapEntropy.continuous_standardDerivativeProduct line 402
  46. lemma OAI.StandardMapEntropy.continuous_standardInverseDerivativeProduct line 409
  47. def OAI.StandardMapEntropy.stableVector line 416
  48. def OAI.StandardMapEntropy.unstableVector line 418
  49. lemma OAI.StandardMapEntropy.measurable_stableVector line 421
  50. lemma OAI.StandardMapEntropy.measurable_unstableVector line 423
  51. lemma OAI.StandardMapEntropy.norm_stableVector line 425
  52. lemma OAI.StandardMapEntropy.norm_unstableVector line 427
  53. lemma OAI.StandardMapEntropy.stableVector_ne_zero line 429
  54. lemma OAI.StandardMapEntropy.unstableVector_ne_zero line 431
  55. lemma OAI.StandardMapEntropy.ae_stableVector_growth line 434
  56. lemma OAI.StandardMapEntropy.ae_unstableVector_growth line 443
  57. lemma OAI.StandardMapEntropy.standardInverseDerivative_standardDerivative line 452
  58. lemma OAI.StandardMapEntropy.standardDerivative_standardInverseDerivative line 457
  59. lemma OAI.StandardMapEntropy.standardDerivativeProduct_shift line 462
  60. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_shift line 471
  61. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_forward line 480
  62. lemma OAI.StandardMapEntropy.contracting_wedge_zero line 486
  63. lemma OAI.StandardMapEntropy.ae_stableVector_covariant line 497
  64. lemma OAI.StandardMapEntropy.ae_unstableVector_covariant line 513
  65. lemma OAI.StandardMapEntropy.unit_collinear_eq_smul line 528
  66. lemma OAI.StandardMapEntropy.unit_collinear_dot_ne_zero line 532
  67. lemma OAI.StandardMapEntropy.covariant_collinear_iff line 539
  68. def OAI.StandardMapEntropy.coincidentLines line 553
  69. lemma OAI.StandardMapEntropy.measurableSet_coincidentLines line 556
  70. lemma OAI.StandardMapEntropy.preimage_coincidentLines_ae line 565