OAI/Dynamics/StandardMap/Bernoulli/TailNameSaturation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.tailName line 13
  2. lemma OAI.HyperbolicCoding.measurable_tailName line 16
  3. def OAI.HyperbolicCoding.TailEvent line 21
  4. theorem OAI.HyperbolicCoding.tailEvent_saturation line 25
  5. lemma OAI.HyperbolicCoding.ExponentiallyAsymptotic.iterate line 47
  6. lemma OAI.StandardMapEntropy.fineStableCurve_exponentiallyAsymptotic line 67
  7. lemma OAI.StandardMapEntropy.fineUnstableCurve_exponentiallyAsymptotic line 80
  8. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.row_exponential line 97
  9. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.column_exponential line 105
  10. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.exists_partitions_doubleTail_constant line 113
  11. lemma OAI.StandardMapEntropy.Entropy.exists_prefix_approx line 161
  12. lemma OAI.StandardMapEntropy.Entropy.exists_cond_prefix_lt line 225
  13. def OAI.HyperbolicCoding.TailObservable line 254
  14. lemma OAI.HyperbolicCoding.TailObservable.word line 258
  15. lemma OAI.HyperbolicCoding.tailEvent_bool line 281
  16. lemma OAI.StandardMapEntropy.Entropy.cond_word_future_eq line 307
  17. lemma OAI.StandardMapEntropy.Entropy.entropy_increment_eq line 317
  18. lemma OAI.StandardMapEntropy.Entropy.entropy_increment_antitone line 329
  19. lemma OAI.StandardMapEntropy.Entropy.entropy_increment_nonneg line 339
  20. lemma OAI.StandardMapEntropy.Entropy.entropy_increment_tendsto line 345
  21. lemma OAI.StandardMapEntropy.Entropy.rate_le_entropy_increment line 361
  22. lemma OAI.StandardMapEntropy.Entropy.rate_mul_le_cond_future line 368
  23. lemma OAI.StandardMapEntropy.Entropy.cond_triangle line 395
  24. lemma OAI.StandardMapEntropy.Entropy.cond_word_window_bound line 406
  25. lemma OAI.StandardMapEntropy.Entropy.rate_mul_le_cond_tail line 419
  26. theorem OAI.StandardMapEntropy.Entropy.tailObservable_rate_zero line 438