OAI/Dynamics/StandardMap/Stable/SmoothRemainder.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.potential_lift_sub_bound line 12
  2. def OAI.StandardMapEntropy.derivativeVariationBound line 31
  3. lemma OAI.StandardMapEntropy.derivativeVariationBound_nonneg line 32
  4. lemma OAI.StandardMapEntropy.standardDerivative_lift_sub_bound line 36
  5. def OAI.StandardMapEntropy.liftRemainder line 61
  6. lemma OAI.StandardMapEntropy.liftRemainder_zero line 63
  7. lemma OAI.StandardMapEntropy.hasFDerivAt_liftRemainder line 66
  8. lemma OAI.StandardMapEntropy.liftRemainder_sub_bound line 73
  9. def OAI.StandardMapEntropy.chartRemainder line 85
  10. lemma OAI.StandardMapEntropy.chartRemainder_zero line 87
  11. lemma OAI.StandardMapEntropy.chartRemainder_sub_bound line 90
  12. abbrev OAI.StandardMapEntropy.NonlinearStable.Plane line 115
  13. abbrev OAI.StandardMapEntropy.NonlinearStable.Sequence line 116
  14. structure OAI.StandardMapEntropy.NonlinearStable.Recurrence line 118
  15. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.step line 130
  16. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.perronValue line 133
  17. lemma OAI.StandardMapEntropy.NonlinearStable.point_sub_bound line 137
  18. lemma OAI.StandardMapEntropy.NonlinearStable.fst_sub_bound line 139
  19. lemma OAI.StandardMapEntropy.NonlinearStable.snd_sub_bound line 141
  20. lemma OAI.StandardMapEntropy.NonlinearStable.remainder_sub_bound line 144
  21. lemma OAI.StandardMapEntropy.NonlinearStable.perronValue_sub_bound line 150
  22. lemma OAI.StandardMapEntropy.NonlinearStable.perronValue_zero line 193
  23. lemma OAI.StandardMapEntropy.NonlinearStable.perronValue_norm_bound line 196
  24. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.perron line 200
  25. lemma OAI.StandardMapEntropy.NonlinearStable.perron_apply line 204
  26. lemma OAI.StandardMapEntropy.NonlinearStable.perron_contracting line 207
  27. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.solution line 217
  28. lemma OAI.StandardMapEntropy.NonlinearStable.solution_fixed line 220
  29. lemma OAI.StandardMapEntropy.NonlinearStable.bound_of_max_contraction line 224
  30. lemma OAI.StandardMapEntropy.NonlinearStable.fixed_norm_bound line 231
  31. lemma OAI.StandardMapEntropy.NonlinearStable.solution_norm_bound line 239
  32. lemma OAI.StandardMapEntropy.NonlinearStable.solution_initial line 242
  33. lemma OAI.StandardMapEntropy.NonlinearStable.solution_orbit line 246
  34. lemma OAI.StandardMapEntropy.NonlinearStable.solution_lipschitz line 260
  35. def OAI.StandardMapEntropy.NonlinearStable.Sequence.tail line 282
  36. lemma OAI.StandardMapEntropy.NonlinearStable.tail_apply line 285
  37. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.tail line 287
  38. lemma OAI.StandardMapEntropy.NonlinearStable.orbit_fixed line 297
  39. lemma OAI.StandardMapEntropy.NonlinearStable.solution_unique line 311
  40. lemma OAI.StandardMapEntropy.NonlinearStable.solution_tail line 316
  41. lemma OAI.StandardMapEntropy.NonlinearStable.solution_cone line 324
  42. lemma OAI.StandardMapEntropy.NonlinearStable.step_fst_sub_bound line 331
  43. lemma OAI.StandardMapEntropy.NonlinearStable.solution_step_contraction line 346
  44. lemma OAI.StandardMapEntropy.NonlinearStable.solution_exponential_contraction line 353
  45. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.graph line 364
  46. lemma OAI.StandardMapEntropy.NonlinearStable.graph_lipschitz line 367
  47. lemma OAI.StandardMapEntropy.NonlinearStable.solution_zero line 374
  48. lemma OAI.StandardMapEntropy.NonlinearStable.graph_zero line 377
  49. theorem OAI.StandardMapEntropy.NonlinearStable.stable_graph line 380
  50. abbrev OAI.StandardMapEntropy.RealPlane line 401
  51. def OAI.StandardMapEntropy.complexToPair line 402
  52. def OAI.StandardMapEntropy.pairToComplex line 403
  53. lemma OAI.StandardMapEntropy.complexToPair_apply line 404
  54. lemma OAI.StandardMapEntropy.pairToComplex_apply line 405
  55. lemma OAI.StandardMapEntropy.complexToPair_pairToComplex line 406
  56. lemma OAI.StandardMapEntropy.pairToComplex_complexToPair line 407
  57. lemma OAI.StandardMapEntropy.complexToPair_norm_le line 408
  58. lemma OAI.StandardMapEntropy.pairToComplex_norm_le line 410
  59. lemma OAI.StandardMapEntropy.norm_complexToPair_le line 415
  60. lemma OAI.StandardMapEntropy.norm_pairToComplex_le line 419
  61. def OAI.StandardMapEntropy.flatFrame line 422
  62. def OAI.StandardMapEntropy.flatInverse line 424
  63. lemma OAI.StandardMapEntropy.flatInverse_frame line 427
  64. lemma OAI.StandardMapEntropy.flatFrame_inverse line 433
  65. lemma OAI.StandardMapEntropy.flatFrame_norm_le line 440
  66. lemma OAI.StandardMapEntropy.flatInverse_norm_le line 450
  67. lemma OAI.StandardMapEntropy.flat_diagonal line 458
  68. def OAI.StandardMapEntropy.flatRemainder line 468
  69. lemma OAI.StandardMapEntropy.flatRemainder_zero line 470
  70. lemma OAI.StandardMapEntropy.flatRemainder_sub_bound line 474