OAI/Dynamics/StandardMap/Entropy/FineCharts.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.fineScale line 12
  2. def OAI.StandardMapEntropy.fineSize line 13
  3. def OAI.StandardMapEntropy.fineFrame line 14
  4. def OAI.StandardMapEntropy.fineInverse line 16
  5. def OAI.StandardMapEntropy.fineStableMultiplier line 18
  6. def OAI.StandardMapEntropy.fineUnstableMultiplier line 20
  7. lemma OAI.StandardMapEntropy.fineScale_pos line 22
  8. lemma OAI.StandardMapEntropy.fineSize_pos line 25
  9. lemma OAI.StandardMapEntropy.fineSize_le_scale line 27
  10. lemma OAI.StandardMapEntropy.fineFrame_norm_le line 29
  11. lemma OAI.StandardMapEntropy.fineInverse_frame line 32
  12. lemma OAI.StandardMapEntropy.fineFrame_inverse line 36
  13. def OAI.StandardMapEntropy.FineRegular line 41
  14. lemma OAI.StandardMapEntropy.ae_fineRegular line 49
  15. lemma OAI.StandardMapEntropy.ae_fineRegular_all_iterates line 57
  16. lemma OAI.StandardMapEntropy.fineSize_ratio line 66
  17. lemma OAI.StandardMapEntropy.fineStableMultiplier_bound line 70
  18. lemma OAI.StandardMapEntropy.fineUnstableMultiplier_ne line 77
  19. lemma OAI.StandardMapEntropy.fineUnstableMultiplier_inverse_bound line 81
  20. def OAI.StandardMapEntropy.codingScale line 100
  21. def OAI.StandardMapEntropy.codingRadius line 101
  22. lemma OAI.StandardMapEntropy.codingScale_pos line 103
  23. lemma OAI.StandardMapEntropy.codingScale_le line 106
  24. lemma OAI.StandardMapEntropy.codingScale_global line 113
  25. lemma OAI.StandardMapEntropy.codingRadius_pos line 121
  26. lemma OAI.StandardMapEntropy.codingRadius_small line 123
  27. lemma OAI.StandardMapEntropy.codingRadius_le_one line 133
  28. lemma OAI.StandardMapEntropy.measurable_codingRadius line 137
  29. def OAI.StandardMapEntropy.codingLevel line 139
  30. lemma OAI.StandardMapEntropy.measurable_codingLevel line 141
  31. lemma OAI.StandardMapEntropy.codingLevel_size line 143
  32. lemma OAI.StandardMapEntropy.codingRadius_ratio line 146
  33. lemma OAI.StandardMapEntropy.codingLevel_step line 166
  34. lemma OAI.StandardMapEntropy.fineInverse_codingRadius line 173
  35. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.linearRate_pos line 200
  36. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.unstable_size_lower line 202
  37. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.unstable_size_ge_one line 205
  38. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.unstable_expansion line 208
  39. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.step_snd_lower line 217
  40. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.unstable_cone_step line 227
  41. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit line 251
  42. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_continuous line 254
  43. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_unstable_cone line 261
  44. def OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox line 272
  45. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_closed line 274
  46. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_fiber_diameter line 278
  47. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_fiber_volume line 297
  48. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_fiber_empty line 305
  49. theorem OAI.StandardMapEntropy.NonlinearStable.Recurrence.trappedBox_volume line 312
  50. lemma OAI.StandardMapEntropy.fine_nonlinearity_coefficient line 340
  51. def OAI.StandardMapEntropy.fineRemainder line 380
  52. lemma OAI.StandardMapEntropy.fineRemainder_zero line 383
  53. lemma OAI.StandardMapEntropy.fineRemainder_lipschitz line 385
  54. lemma OAI.StandardMapEntropy.fine_derivative_diagonal line 391
  55. lemma OAI.StandardMapEntropy.fine_step line 395
  56. lemma OAI.StandardMapEntropy.fine_lift_step line 405
  57. def OAI.StandardMapEntropy.fineLinearRate line 424
  58. def OAI.StandardMapEntropy.fineErrorRate line 425
  59. lemma OAI.StandardMapEntropy.fine_regular_lift_next line 426
  60. def OAI.StandardMapEntropy.fineLocalRecurrence line 430
  61. def OAI.StandardMapEntropy.fineCoordinate line 442
  62. lemma OAI.StandardMapEntropy.fineCoordinate_initial line 445
  63. lemma OAI.StandardMapEntropy.fineCoordinate_step line 450
  64. def OAI.StandardMapEntropy.fineTrapped line 464
  65. lemma OAI.StandardMapEntropy.fineTrapped_subset line 467
  66. theorem OAI.StandardMapEntropy.fineTrapped_volume line 483
  67. lemma OAI.StandardMapEntropy.fine_parameters_for_rate line 491
  68. theorem OAI.StandardMapEntropy.ae_sharp_fine_volume line 499