OAI/Dynamics/StandardMap/Lyapunov/MeasurableFrame.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.measurable_complex_mk line 12
  2. lemma OAI.StandardMapEntropy.measurable_wedge line 16
  3. lemma OAI.StandardMapEntropy.measurable_rankOne line 21
  4. lemma OAI.StandardMapEntropy.planeCoframe_columns line 25
  5. lemma OAI.StandardMapEntropy.measurable_lyapunovFrame line 34
  6. lemma OAI.StandardMapEntropy.measurable_lyapunovCoframe line 41
  7. def OAI.StandardMapEntropy.TemperedControl.orbit line 73
  8. lemma OAI.StandardMapEntropy.TemperedControl.orbit_zero line 74
  9. lemma OAI.StandardMapEntropy.TemperedControl.orbit_one line 75
  10. lemma OAI.StandardMapEntropy.TemperedControl.orbit_neg_one line 76
  11. lemma OAI.StandardMapEntropy.TemperedControl.orbit_add line 77
  12. lemma OAI.StandardMapEntropy.TemperedControl.orbit_nat line 79
  13. lemma OAI.StandardMapEntropy.TemperedControl.orbit_neg_nat line 81
  14. lemma OAI.StandardMapEntropy.TemperedControl.measurable_orbit line 83
  15. lemma OAI.StandardMapEntropy.TemperedControl.summable_damped_of_log_rate line 90
  16. def OAI.StandardMapEntropy.TemperedControl.weight line 107
  17. def OAI.StandardMapEntropy.TemperedControl.control line 108
  18. def OAI.StandardMapEntropy.TemperedControl.radius line 110
  19. lemma OAI.StandardMapEntropy.TemperedControl.summable_control line 113
  20. lemma OAI.StandardMapEntropy.TemperedControl.control_nonneg line 125
  21. lemma OAI.StandardMapEntropy.TemperedControl.control_ge line 127
  22. lemma OAI.StandardMapEntropy.TemperedControl.weight_shift_bound line 132
  23. lemma OAI.StandardMapEntropy.TemperedControl.summable_control_orbit line 141
  24. lemma OAI.StandardMapEntropy.TemperedControl.control_orbit_le line 156
  25. lemma OAI.StandardMapEntropy.TemperedControl.radius_pos line 176
  26. lemma OAI.StandardMapEntropy.TemperedControl.radius_le_one line 180
  27. lemma OAI.StandardMapEntropy.TemperedControl.radius_mul_control_le line 184
  28. lemma OAI.StandardMapEntropy.TemperedControl.radius_orbit_lower line 195
  29. lemma OAI.StandardMapEntropy.TemperedControl.measurable_control line 206
  30. lemma OAI.StandardMapEntropy.TemperedControl.measurable_radius line 208
  31. def OAI.StandardMapEntropy.diagonalPlane line 220
  32. lemma OAI.StandardMapEntropy.diagonalPlane_apply line 222
  33. lemma OAI.StandardMapEntropy.planeFrame_normal_form line 226
  34. lemma OAI.StandardMapEntropy.collinear_image_norm line 244
  35. lemma OAI.StandardMapEntropy.energy_contraction line 249
  36. def OAI.StandardMapEntropy.stableMultiplier line 263
  37. def OAI.StandardMapEntropy.unstableMultiplier line 266
  38. lemma OAI.StandardMapEntropy.ae_lyapunov_normal_form line 270
  39. lemma OAI.StandardMapEntropy.ae_stableMultiplier_bound line 286
  40. lemma OAI.StandardMapEntropy.covariant_inverse_norm_product line 305
  41. lemma OAI.StandardMapEntropy.ae_unstableMultiplier_bound line 314
  42. lemma OAI.StandardMapEntropy.standardMap_measurableEquiv_apply line 357
  43. lemma OAI.StandardMapEntropy.standardMap_measurableEquiv_symm_apply line 359
  44. lemma OAI.StandardMapEntropy.log_max_one_rate line 362
  45. def OAI.StandardMapEntropy.chartControl line 377
  46. def OAI.StandardMapEntropy.chartRadius line 378
  47. lemma OAI.StandardMapEntropy.chartControl_ge_one line 380
  48. lemma OAI.StandardMapEntropy.measurable_chartControl line 381
  49. lemma OAI.StandardMapEntropy.measurable_chartRadius line 383
  50. lemma OAI.StandardMapEntropy.chartRadius_pos line 385
  51. lemma OAI.StandardMapEntropy.chartRadius_le_one line 387
  52. lemma OAI.StandardMapEntropy.ae_chartControl_summable line 390
  53. theorem OAI.StandardMapEntropy.ae_chartRadius_control line 399