OAI/Dynamics/StandardMap/Holonomy/DerivativeQuantitative.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.standardDerivativeProduct_quantitative line 12
  2. lemma OAI.StandardMapEntropy.standardInverseDerivativeProduct_quantitative line 74
  3. lemma OAI.StandardMapEntropy.contracting_line_comparison line 112
  4. lemma OAI.StandardMapEntropy.PlaneLyapunov.norm_le_of_energy_le line 129
  5. lemma OAI.StandardMapEntropy.unit_projective_image_bound line 144
  6. lemma OAI.StandardMapEntropy.unit_image_norm_difference line 159
  7. lemma OAI.StandardMapEntropy.log_difference_of_lower line 173
  8. lemma OAI.StandardMapEntropy.area_unit_log_image_difference line 191
  9. def OAI.StandardMapEntropy.unstableLogJacobian line 212
  10. lemma OAI.StandardMapEntropy.measurable_unstableLogJacobian line 214
  11. lemma OAI.StandardMapEntropy.unstableLogJacobian_difference line 219
  12. lemma OAI.StandardMapEntropy.sum_of_backward_contraction line 236
  13. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.step_zero line 254
  14. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_zero line 256
  15. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_cone line 261
  16. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_norm_eq_snd line 274
  17. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_snd_ne_zero line 277
  18. lemma OAI.StandardMapEntropy.NonlinearStable.scalar_log_quadratic_error line 287
  19. theorem OAI.StandardMapEntropy.NonlinearStable.Recurrence.finite_cone_log_distortion line 322
  20. def OAI.StandardMapEntropy.fineRemainderDerivative line 371
  21. lemma OAI.StandardMapEntropy.hasFDerivAt_fineRemainder line 374
  22. lemma OAI.StandardMapEntropy.fineRemainderDerivative_zero line 377
  23. lemma OAI.StandardMapEntropy.fineRemainderDerivative_lipschitz line 379
  24. lemma OAI.StandardMapEntropy.fineRemainderDerivative_bound line 385
  25. lemma OAI.StandardMapEntropy.fineRemainder_taylor line 392
  26. lemma OAI.StandardMapEntropy.fineRemainder_quadratic line 399
  27. lemma OAI.StandardMapEntropy.fineTrapped_orbit line 406
  28. theorem OAI.StandardMapEntropy.fineTrapped_log_distortion line 416