OAI/Dynamics/StandardMap/Stable/LocalStable.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.NonlinearStable.unitClip line 12
  2. lemma OAI.StandardMapEntropy.NonlinearStable.abs_unitClip_le line 13
  3. lemma OAI.StandardMapEntropy.NonlinearStable.unitClip_eq line 16
  4. lemma OAI.StandardMapEntropy.NonlinearStable.unitClip_lipschitz line 19
  5. def OAI.StandardMapEntropy.NonlinearStable.planeClip line 22
  6. lemma OAI.StandardMapEntropy.NonlinearStable.norm_planeClip_le line 23
  7. lemma OAI.StandardMapEntropy.NonlinearStable.planeClip_eq line 25
  8. lemma OAI.StandardMapEntropy.NonlinearStable.planeClip_zero line 27
  9. lemma OAI.StandardMapEntropy.NonlinearStable.planeClip_lipschitz line 28
  10. structure OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence line 37
  11. def OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.step line 49
  12. def OAI.StandardMapEntropy.NonlinearStable.LocalRecurrence.extend line 51
  13. lemma OAI.StandardMapEntropy.NonlinearStable.extend_step_eq line 65
  14. lemma OAI.StandardMapEntropy.NonlinearStable.local_solution_bound line 69
  15. lemma OAI.StandardMapEntropy.NonlinearStable.local_solution_orbit line 72
  16. theorem OAI.StandardMapEntropy.NonlinearStable.local_stable_graph line 76
  17. def OAI.StandardMapEntropy.hyperbolicChartRate line 94
  18. def OAI.StandardMapEntropy.hyperbolicChartError line 95
  19. def OAI.StandardMapEntropy.hyperbolicChartScale line 96
  20. lemma OAI.StandardMapEntropy.hyperbolicChartRate_pos line 98
  21. lemma OAI.StandardMapEntropy.hyperbolicChartRate_lt_one line 99
  22. lemma OAI.StandardMapEntropy.hyperbolicChartError_pos line 102
  23. lemma OAI.StandardMapEntropy.hyperbolicChartScale_pos line 106
  24. lemma OAI.StandardMapEntropy.hyperbolicChartScale_le line 109
  25. def OAI.StandardMapEntropy.chartSize line 119
  26. def OAI.StandardMapEntropy.actualChartFrame line 121
  27. def OAI.StandardMapEntropy.actualChartInverse line 123
  28. def OAI.StandardMapEntropy.actualStableMultiplier line 125
  29. def OAI.StandardMapEntropy.actualUnstableMultiplier line 127
  30. lemma OAI.StandardMapEntropy.chartSize_pos line 129
  31. lemma OAI.StandardMapEntropy.chartSize_le_scale line 131
  32. lemma OAI.StandardMapEntropy.actualChartFrame_norm_le line 135
  33. lemma OAI.StandardMapEntropy.actualChartInverse_frame line 138
  34. lemma OAI.StandardMapEntropy.actualChartFrame_inverse line 142
  35. def OAI.StandardMapEntropy.RegularChartPoint line 147
  36. lemma OAI.StandardMapEntropy.ae_regularChartPoint line 158
  37. lemma OAI.StandardMapEntropy.ae_regularChartPoint_all_iterates line 167
  38. lemma OAI.StandardMapEntropy.slow_radius_ratio line 178
  39. lemma OAI.StandardMapEntropy.chartSize_ratio line 185
  40. lemma OAI.StandardMapEntropy.actualStableMultiplier_bound line 190
  41. lemma OAI.StandardMapEntropy.actualUnstableMultiplier_ne line 202
  42. lemma OAI.StandardMapEntropy.actualUnstableMultiplier_inverse_bound line 207
  43. lemma OAI.StandardMapEntropy.chart_nonlinearity_coefficient line 231
  44. def OAI.StandardMapEntropy.actualChartRemainder line 276
  45. lemma OAI.StandardMapEntropy.actualChartRemainder_zero line 279
  46. lemma OAI.StandardMapEntropy.actualChartRemainder_lipschitz line 281
  47. lemma OAI.StandardMapEntropy.actualChart_derivative_diagonal line 289
  48. lemma OAI.StandardMapEntropy.actualChart_step line 294
  49. lemma OAI.StandardMapEntropy.actualChart_lift_step line 307
  50. def OAI.StandardMapEntropy.chartLinearRate line 327
  51. def OAI.StandardMapEntropy.chartErrorRate line 328
  52. lemma OAI.StandardMapEntropy.chart_rates_contract line 329
  53. lemma OAI.StandardMapEntropy.regular_lift_next line 334
  54. def OAI.StandardMapEntropy.actualLocalRecurrence line 339
  55. lemma OAI.StandardMapEntropy.actualLocalRecurrence_lift_step line 351
  56. lemma OAI.StandardMapEntropy.actual_local_orbit_lift line 360
  57. theorem OAI.StandardMapEntropy.actual_stable_curve_of_regular line 370
  58. theorem OAI.StandardMapEntropy.ae_actual_stable_curve line 414
  59. def OAI.StandardMapEntropy.NonlinearStable.sndSequence line 436
  60. lemma OAI.StandardMapEntropy.NonlinearStable.sndSequence_apply line 439
  61. lemma OAI.StandardMapEntropy.NonlinearStable.linearRate_lt_one line 441
  62. lemma OAI.StandardMapEntropy.NonlinearStable.solution_snd_bound_of_forcing line 445
  63. lemma OAI.StandardMapEntropy.NonlinearStable.graph_slope_bound line 478
  64. lemma OAI.StandardMapEntropy.NonlinearStable.graph_bound_of_forcing line 488
  65. lemma OAI.StandardMapEntropy.NonlinearStable.local_graph_quadratic_bound line 498