OAI/Dynamics/StandardMap/Lyapunov/DerivativeGrowth.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.tangentCoordinates_re line 13
  2. lemma OAI.StandardMapEntropy.tangentCoordinates_im line 14
  3. lemma OAI.StandardMapEntropy.tangentCoordinates_involutive line 15
  4. lemma OAI.StandardMapEntropy.tangentCoordinates_wedge line 19
  5. lemma OAI.StandardMapEntropy.tangentCoordinates_norm_le line 24
  6. lemma OAI.StandardMapEntropy.standardDerivative_re line 36
  7. lemma OAI.StandardMapEntropy.standardDerivative_im line 41
  8. lemma OAI.StandardMapEntropy.standardDerivative_area line 47
  9. lemma OAI.StandardMapEntropy.standardInverseDerivative_area line 53
  10. lemma OAI.StandardMapEntropy.standardDerivativeProduct_area line 59
  11. lemma OAI.StandardMapEntropy.standardDerivative_norm_ge_one line 65
  12. lemma OAI.StandardMapEntropy.standardInverseDerivative_norm_ge_one line 67
  13. lemma OAI.StandardMapEntropy.standardDerivativeProduct_norm_ge_one line 70
  14. lemma OAI.StandardMapEntropy.complexProjection_standardLift line 74
  15. lemma OAI.StandardMapEntropy.complexProjection_standardInverseLift line 77
  16. lemma OAI.StandardMapEntropy.standardLift_inverse line 82
  17. lemma OAI.StandardMapEntropy.standardInverseLift_inverse line 85
  18. lemma OAI.StandardMapEntropy.continuous_transferStepInv line 89
  19. lemma OAI.StandardMapEntropy.continuous_standardDerivative line 99
  20. lemma OAI.StandardMapEntropy.continuous_inverseMap line 104
  21. lemma OAI.StandardMapEntropy.continuous_standardInverseDerivative line 108
  22. lemma OAI.StandardMapEntropy.integrable_log_standardDerivative line 113
  23. lemma OAI.StandardMapEntropy.integrable_log_standardInverseDerivative line 118
  24. lemma OAI.StandardMapEntropy.recurrenceCoordinates_iterate line 124
  25. lemma OAI.StandardMapEntropy.standardDerivativeProduct_conjugate line 133
  26. lemma OAI.StandardMapEntropy.conjugate_norm_le line 155
  27. lemma OAI.StandardMapEntropy.conjugate_norm_lower line 164
  28. lemma OAI.StandardMapEntropy.derivative_log_difference_bound line 172
  29. lemma OAI.StandardMapEntropy.contDiff_standardLift line 194
  30. lemma OAI.StandardMapEntropy.contDiff_standardInverseLift line 202
  31. lemma OAI.StandardMapEntropy.complexPair_re line 210
  32. lemma OAI.StandardMapEntropy.complexPair_im line 211
  33. lemma OAI.StandardMapEntropy.hasFDerivAt_standardLift line 213
  34. lemma OAI.StandardMapEntropy.hasFDerivAt_standardInverseLift line 226
  35. theorem OAI.StandardMapEntropy.actual_derivative_certificate line 240
  36. lemma OAI.StandardMapEntropy.complexProjection_iterate line 254
  37. lemma OAI.StandardMapEntropy.hasFDerivAt_standardLift_iterate line 261
  38. lemma OAI.StandardMapEntropy.derivative_rate_of_transfer_rate line 270
  39. def OAI.StandardMapEntropy.standardLyapunov line 288
  40. lemma OAI.StandardMapEntropy.measurable_recurrenceCoordinates line 291
  41. lemma OAI.StandardMapEntropy.measurable_standardLyapunov line 294
  42. lemma OAI.StandardMapEntropy.integrable_standardLyapunov line 298
  43. lemma OAI.StandardMapEntropy.standardLyapunov_nonneg line 303
  44. lemma OAI.StandardMapEntropy.standardLyapunov_invariant line 306
  45. lemma OAI.StandardMapEntropy.ae_standardLyapunov_rate line 312
  46. lemma OAI.StandardMapEntropy.positive_standardLyapunov_of_deficit line 321
  47. lemma OAI.StandardMapEntropy.standardDerivative_norm_bound line 337
  48. lemma OAI.StandardMapEntropy.standardDerivativeProduct_step_lower line 345