OAI/Dynamics/StandardMap/Lyapunov/BoundedTempering.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedSubadditive.observationCocycle line 14
  2. lemma OAI.BoundedSubadditive.ae_exists_bounded_average_limit line 28
  3. theorem OAI.BoundedSubadditive.ae_nonnegative_coboundary_tempered line 57
  4. def OAI.StandardMapEntropy.spectralGapRegion line 106
  5. lemma OAI.StandardMapEntropy.measurableSet_spectralGapRegion line 108
  6. lemma OAI.StandardMapEntropy.preimage_spectralGapRegion line 111
  7. lemma OAI.StandardMapEntropy.preimage_inverse_spectralGapRegion line 115
  8. lemma OAI.StandardMapEntropy.measurePreserving_spectralGapRegion line 119
  9. lemma OAI.StandardMapEntropy.measurePreserving_inverse_spectralGapRegion line 124
  10. lemma OAI.StandardMapEntropy.unit_image_bounds line 130
  11. lemma OAI.StandardMapEntropy.positive_energy_ratio_bounds line 139
  12. lemma OAI.StandardMapEntropy.log_ratio_bound line 158
  13. lemma OAI.StandardMapEntropy.ae_both_coboundary_tempered line 166
  14. def OAI.StandardMapEntropy.energyRatioBound line 179
  15. lemma OAI.StandardMapEntropy.energyRatioBound_ge_one line 181
  16. lemma OAI.StandardMapEntropy.ae_stableEnergy_log_increment line 186
  17. lemma OAI.StandardMapEntropy.ae_unstableEnergy_log_increment line 207
  18. lemma OAI.StandardMapEntropy.log_stableScale line 228
  19. lemma OAI.StandardMapEntropy.log_unstableScale line 231
  20. theorem OAI.StandardMapEntropy.ae_lyapunovScale_tempered line 235
  21. def OAI.StandardMapEntropy.planeFrame line 277
  22. lemma OAI.StandardMapEntropy.planeFrame_apply line 281
  23. def OAI.StandardMapEntropy.planeCoframe line 286
  24. lemma OAI.StandardMapEntropy.planeCoframe_apply line 292
  25. lemma OAI.StandardMapEntropy.planeCoframe_frame line 295
  26. lemma OAI.StandardMapEntropy.planeFrame_coframe line 306
  27. lemma OAI.StandardMapEntropy.planeFrame_norm_le line 317
  28. lemma OAI.StandardMapEntropy.planeCoframe_norm_le line 337
  29. def OAI.StandardMapEntropy.lyapunovFrame line 367
  30. def OAI.StandardMapEntropy.lyapunovCoframe line 369
  31. lemma OAI.StandardMapEntropy.lyapunovFrame_norm_le line 372
  32. lemma OAI.StandardMapEntropy.lyapunovCoframe_frame line 376
  33. lemma OAI.StandardMapEntropy.lyapunovFrame_coframe line 381
  34. lemma OAI.StandardMapEntropy.planeCoframe_norm_ge_one line 387
  35. lemma OAI.StandardMapEntropy.planeCoframe_log_bound line 397
  36. lemma OAI.StandardMapEntropy.coframe_tempered line 409
  37. theorem OAI.StandardMapEntropy.ae_lyapunovCoframe_tempered line 426