OAI/Dynamics/StandardMap/Coding/FullEntropyCopySequence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.FiniteRateSupremum line 15
  2. lemma OAI.HyperbolicCoding.FiniteRateSupremum.upper line 21
  3. lemma OAI.HyperbolicCoding.iid_lawClose_prefix line 32
  4. def OAI.HyperbolicCoding.GoodIIDStage line 48
  5. lemma OAI.HyperbolicCoding.goodIIDStage_initial line 56
  6. lemma OAI.HyperbolicCoding.goodIIDStage_next line 69
  7. theorem OAI.HyperbolicCoding.full_entropy_copy_sequence line 92
  8. lemma OAI.HyperbolicCoding.iidShift_integerIterate line 140
  9. lemma OAI.HyperbolicCoding.iid_orbitName line 149
  10. lemma OAI.HyperbolicCoding.finite_integer_window line 153
  11. lemma OAI.HyperbolicCoding.orbit_restrict_map_eq_window line 164
  12. lemma OAI.HyperbolicCoding.lawClose_orbit_restrict_of_word line 185
  13. lemma OAI.HyperbolicCoding.restricted_box_lawClose line 198
  14. theorem OAI.HyperbolicCoding.iid_law_of_growing_forward_words line 223
  15. lemma OAI.HyperbolicCoding.word_law_of_iid_factor line 272
  16. lemma OAI.HyperbolicCoding.rate_of_iid_factor line 285
  17. lemma OAI.HyperbolicCoding.geometric_repainting_summable line 309
  18. theorem OAI.HyperbolicCoding.full_entropy_iid_factor line 326
  19. lemma OAI.StandardMapEntropy.Entropy.shannon_weighted_le line 359
  20. lemma OAI.StandardMapEntropy.Entropy.obs_weighted_le line 381
  21. lemma OAI.StandardMapEntropy.Entropy.rate_weighted_le line 388
  22. lemma OAI.StandardMapEntropy.area_weight_normalized line 405
  23. lemma OAI.StandardMapEntropy.restricted_finite_rate_upper line 417
  24. theorem OAI.HyperbolicCoding.exists_finiteRateSupremum line 447