OAI/Dynamics/StandardMap/Stable/PerronStability.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.NonlinearStable.perron_defect_bound line 13
  2. lemma OAI.StandardMapEntropy.NonlinearStable.near_orbit_solution_bound line 43
  3. def OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.linearized line 55
  4. lemma OAI.StandardMapEntropy.NonlinearStable.linearized_step_smul line 68
  5. lemma OAI.StandardMapEntropy.NonlinearStable.linearized_solution_smul line 74
  6. lemma OAI.StandardMapEntropy.NonlinearStable.hasDerivAt_of_quadratic_bound line 86
  7. lemma OAI.StandardMapEntropy.quadratic_taylor_of_derivative_lipschitz line 113
  8. def OAI.StandardMapEntropy.flatRemainderDerivative line 131
  9. lemma OAI.StandardMapEntropy.hasFDerivAt_flatRemainder line 134
  10. lemma OAI.StandardMapEntropy.flatRemainderDerivative_zero line 138
  11. lemma OAI.StandardMapEntropy.flatRemainderDerivative_lipschitz line 142
  12. def OAI.StandardMapEntropy.actualChartRemainderDerivative line 167
  13. lemma OAI.StandardMapEntropy.hasFDerivAt_actualChartRemainder line 170
  14. lemma OAI.StandardMapEntropy.actualChartRemainderDerivative_zero line 173
  15. lemma OAI.StandardMapEntropy.actualChartRemainderDerivative_lipschitz line 175
  16. lemma OAI.StandardMapEntropy.actualChartRemainderDerivative_bound line 182
  17. lemma OAI.StandardMapEntropy.actualChartRemainder_taylor line 189
  18. lemma OAI.StandardMapEntropy.actualChartRemainder_quadratic line 196
  19. lemma OAI.StandardMapEntropy.NonlinearStable.linearized_difference_residual line 212
  20. lemma OAI.StandardMapEntropy.NonlinearStable.solution_quadratic_approximation line 222
  21. def OAI.StandardMapEntropy.NonlinearStable.graphLinearization line 243
  22. lemma OAI.StandardMapEntropy.NonlinearStable.solution_hasDerivAt line 249
  23. def OAI.StandardMapEntropy.NonlinearStable.sequenceEval line 264
  24. lemma OAI.StandardMapEntropy.NonlinearStable.sequenceEval_apply line 269
  25. lemma OAI.StandardMapEntropy.NonlinearStable.graph_hasDerivAt line 271
  26. lemma OAI.StandardMapEntropy.NonlinearStable.linearized_difference_of_fields line 282
  27. lemma OAI.StandardMapEntropy.NonlinearStable.linearized_solution_field_bound line 289
  28. lemma OAI.StandardMapEntropy.NonlinearStable.graphLinearization_lipschitz line 303
  29. lemma OAI.StandardMapEntropy.NonlinearStable.graph_deriv_lipschitzOn line 325
  30. lemma OAI.StandardMapEntropy.NonlinearStable.graph_contDiffOn line 344
  31. lemma OAI.StandardMapEntropy.NonlinearStable.graph_hasDerivAt_zero line 357
  32. def OAI.StandardMapEntropy.actualStableGraph line 376
  33. def OAI.StandardMapEntropy.actualStableCurve line 379
  34. lemma OAI.StandardMapEntropy.actualStableGraph_contDiffOn line 383
  35. lemma OAI.StandardMapEntropy.actualStableGraph_hasDerivAt_zero line 395
  36. lemma OAI.StandardMapEntropy.actualStableCurve_contDiffOn line 402
  37. lemma OAI.StandardMapEntropy.actualStableCurve_hasDerivAt_zero line 408
  38. lemma OAI.StandardMapEntropy.actualStableCurve_regular line 415
  39. lemma OAI.StandardMapEntropy.actualStableFrame_tangent line 433
  40. lemma OAI.StandardMapEntropy.actualStableCurve_orbit line 441
  41. lemma OAI.StandardMapEntropy.actualStableCurve_contraction line 453
  42. theorem OAI.StandardMapEntropy.ae_actual_stable_C1 line 468
  43. lemma OAI.StandardMapEntropy.standardReversal_involutive line 495
  44. lemma OAI.StandardMapEntropy.complexProjection_tangentReversal line 497
  45. lemma OAI.StandardMapEntropy.tangentReversal_inverseLift line 500
  46. lemma OAI.StandardMapEntropy.tangentReversal_inverse_lift_iterate line 503
  47. lemma OAI.StandardMapEntropy.inverse_lift_iterate_reversed line 508
  48. lemma OAI.StandardMapEntropy.tangentReversal_norm_le line 512
  49. lemma OAI.StandardMapEntropy.tangentReversal_ne_zero line 519
  50. lemma OAI.StandardMapEntropy.measurePreserving_reversal_spectralGapRegion line 524
  51. lemma OAI.StandardMapEntropy.ae_stableVector_reversal_unstable line 534
  52. lemma OAI.StandardMapEntropy.ae_reversal_tangent_transverse line 550
  53. def OAI.StandardMapEntropy.actualUnstableCurve line 571
  54. lemma OAI.StandardMapEntropy.actualUnstableCurve_contDiffOn line 575
  55. lemma OAI.StandardMapEntropy.actualUnstableCurve_hasDerivAt_zero line 579
  56. lemma OAI.StandardMapEntropy.actualUnstableCurve_regular line 587
  57. lemma OAI.StandardMapEntropy.actualUnstableCurve_contraction line 597
  58. theorem OAI.StandardMapEntropy.ae_actual_unstable_C1 line 607