OAI/Dynamics/StandardMap/Lyapunov/TransverseLines.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.standardLyapunov_iterate line 12
  2. lemma OAI.StandardMapEntropy.ae_stableVector_product_covariant line 18
  3. lemma OAI.StandardMapEntropy.standardDerivativeProduct_inverse line 33
  4. lemma OAI.StandardMapEntropy.standardDerivativeProduct_norm_bound line 43
  5. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_norm_bound line 54
  6. lemma OAI.StandardMapEntropy.area_unit_log_abs_bound line 65
  7. lemma OAI.StandardMapEntropy.area_unit_rate_bound line 81
  8. def OAI.StandardMapEntropy.stableGrowthAverage line 94
  9. def OAI.StandardMapEntropy.stableBackwardAverage line 96
  10. lemma OAI.StandardMapEntropy.measurable_stableGrowthAverage line 99
  11. lemma OAI.StandardMapEntropy.measurable_stableBackwardAverage line 102
  12. lemma OAI.StandardMapEntropy.stableGrowthAverage_bound line 106
  13. lemma OAI.StandardMapEntropy.stableBackwardAverage_bound line 110
  14. lemma OAI.StandardMapEntropy.ae_stable_averages_cancel line 115
  15. lemma OAI.StandardMapEntropy.measurePreserving_coincidentLines line 138
  16. lemma OAI.StandardMapEntropy.ae_coincident_backward_growth line 145
  17. theorem OAI.StandardMapEntropy.measure_coincidentLines_zero line 155
  18. lemma OAI.StandardMapEntropy.ae_transverseLines line 213
  19. theorem OAI.StandardMapEntropy.ae_hyperbolic_splitting line 221
  20. def OAI.StandardMapEntropy.standardMap_measurableEquiv line 242
  21. lemma OAI.StandardMapEntropy.measurePreserving_inverseMap line 250
  22. lemma OAI.StandardMapEntropy.standardLyapunov_inverse line 253
  23. lemma OAI.StandardMapEntropy.standardLyapunov_inverse_iterate line 259
  24. lemma OAI.StandardMapEntropy.inverse_covariant_line line 265
  25. lemma OAI.StandardMapEntropy.ae_stableVector_inverse_covariant line 274
  26. lemma OAI.StandardMapEntropy.ae_unstableVector_inverse_covariant line 282
  27. lemma OAI.StandardMapEntropy.ae_unstableVector_product_covariant line 290
  28. lemma OAI.StandardMapEntropy.ae_stableVector_inverse_product_covariant line 308
  29. lemma OAI.StandardMapEntropy.ae_unstableVector_inverse_product_covariant line 326
  30. lemma OAI.StandardMapEntropy.invariant_unit_frame_wedge line 344
  31. lemma OAI.StandardMapEntropy.invariant_frame_angle_rate line 354
  32. theorem OAI.StandardMapEntropy.ae_angle_tempered line 379
  33. def OAI.StandardMapEntropy.PlaneLyapunov.energy line 416
  34. lemma OAI.StandardMapEntropy.PlaneLyapunov.summable_energy line 419
  35. lemma OAI.StandardMapEntropy.PlaneLyapunov.energy_nonneg line 445
  36. lemma OAI.StandardMapEntropy.PlaneLyapunov.energy_ge_one line 448
  37. lemma OAI.StandardMapEntropy.PlaneLyapunov.measurable_energy line 456
  38. lemma OAI.StandardMapEntropy.PlaneLyapunov.energy_shift line 466
  39. def OAI.StandardMapEntropy.stableEnergy line 494
  40. def OAI.StandardMapEntropy.unstableEnergy line 496
  41. def OAI.StandardMapEntropy.stableScale line 499
  42. def OAI.StandardMapEntropy.unstableScale line 500
  43. lemma OAI.StandardMapEntropy.measurable_stableEnergy line 502
  44. lemma OAI.StandardMapEntropy.measurable_unstableEnergy line 505
  45. lemma OAI.StandardMapEntropy.measurable_stableScale line 508
  46. lemma OAI.StandardMapEntropy.measurable_unstableScale line 510
  47. lemma OAI.StandardMapEntropy.stableScale_ge_one line 513
  48. lemma OAI.StandardMapEntropy.unstableScale_ge_one line 515
  49. lemma OAI.StandardMapEntropy.ae_stableEnergy_regular line 518
  50. lemma OAI.StandardMapEntropy.ae_unstableEnergy_regular line 536