OAI/Dynamics/StandardMap/Lyapunov/Subadditive.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedSubadditive.excess line 14
  2. lemma OAI.BoundedSubadditive.excess_nonneg line 18
  3. lemma OAI.BoundedSubadditive.excess_succ_mono line 24
  4. lemma OAI.BoundedSubadditive.excess_mono line 31
  5. lemma OAI.BoundedSubadditive.sum_sub_le_excess line 35
  6. lemma OAI.BoundedSubadditive.excess_account line 47
  7. lemma OAI.BoundedSubadditive.measurable_excess line 67
  8. lemma OAI.BoundedSubadditive.integrable_excess line 73
  9. lemma OAI.BoundedSubadditive.integral_comp line 82
  10. lemma OAI.BoundedSubadditive.excess_measure_bound line 87
  11. lemma OAI.BoundedSubadditive.maximal_measure_bound line 117
  12. structure OAI.BoundedSubadditive.Cocycle line 136
  13. def OAI.BoundedSubadditive.Cocycle.average line 147
  14. def OAI.BoundedSubadditive.Cocycle.lowerRate line 148
  15. def OAI.BoundedSubadditive.Cocycle.upperRate line 149
  16. lemma OAI.BoundedSubadditive.Cocycle.average_bounds line 151
  17. lemma OAI.BoundedSubadditive.Cocycle.average_bdd_above line 157
  18. lemma OAI.BoundedSubadditive.Cocycle.average_bdd_below line 160
  19. lemma OAI.BoundedSubadditive.Cocycle.lowerRate_bounds line 163
  20. lemma OAI.BoundedSubadditive.Cocycle.lowerRate_le_upperRate line 171
  21. lemma OAI.BoundedSubadditive.Cocycle.measurable_average line 174
  22. lemma OAI.BoundedSubadditive.Cocycle.measurable_lowerRate line 177
  23. lemma OAI.BoundedSubadditive.Cocycle.measurable_upperRate line 180
  24. lemma OAI.BoundedSubadditive.Cocycle.average_shift_bound line 183
  25. lemma OAI.BoundedSubadditive.Cocycle.lowerRate_shift line 188
  26. lemma OAI.BoundedSubadditive.Cocycle.lowerRate_iterate line 211
  27. def OAI.BoundedSubadditive.Cocycle.badSet line 216
  28. def OAI.BoundedSubadditive.Cocycle.badObservation line 219
  29. lemma OAI.BoundedSubadditive.Cocycle.measurableSet_badSet line 222
  30. lemma OAI.BoundedSubadditive.Cocycle.measurable_badObservation line 229
  31. lemma OAI.BoundedSubadditive.Cocycle.badObservation_bounds line 232
  32. lemma OAI.BoundedSubadditive.Cocycle.exists_good_block line 237
  33. lemma OAI.BoundedSubadditive.Cocycle.badObservation_tendsto_zero line 247
  34. lemma OAI.BoundedSubadditive.Cocycle.birkhoff_bad_nonneg line 257
  35. lemma OAI.BoundedSubadditive.Cocycle.block_bound line 261
  36. lemma OAI.BoundedSubadditive.Cocycle.upperRate_le_of_bad_averages line 308
  37. lemma OAI.BoundedSubadditive.Cocycle.integrable_badObservation line 327
  38. lemma OAI.BoundedSubadditive.Cocycle.integral_badObservation_tendsto_zero line 331
  39. lemma OAI.BoundedSubadditive.Cocycle.ae_upperRate_le_add line 342
  40. theorem OAI.BoundedSubadditive.Cocycle.ae_tendsto_average line 366
  41. lemma OAI.BoundedSubadditive.Cocycle.integrable_lowerRate line 381
  42. lemma OAI.BoundedSubadditive.Cocycle.integrable_average line 387
  43. theorem OAI.BoundedSubadditive.Cocycle.tendsto_integral_average line 393
  44. lemma OAI.StandardMapEntropy.torusIter_nat_apply line 409
  45. lemma OAI.StandardMapEntropy.productDistance_one_shift_bound line 413
  46. def OAI.StandardMapEntropy.transferCocycle line 436
  47. def OAI.StandardMapEntropy.transferLyapunov line 447
  48. def OAI.StandardMapEntropy.TransferLimit line 450
  49. lemma OAI.StandardMapEntropy.lognorm_average_eq line 457
  50. lemma OAI.StandardMapEntropy.transferLyapunov_limit line 471
  51. theorem OAI.StandardMapEntropy.ae_transfer_limit line 485
  52. lemma OAI.StandardMapEntropy.integral_lowerRate_of_deficit line 489
  53. lemma OAI.StandardMapEntropy.positive_transferLyapunov_of_deficit line 504
  54. theorem OAI.StandardMapEntropy.positive_transfer_limit line 524