OAI/Dynamics/StandardMap/Bernoulli/IntegerDynamics.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.integerIterate line 14
  2. lemma OAI.HyperbolicCoding.integerIterate_zero line 16
  3. lemma OAI.HyperbolicCoding.integerIterate_one line 18
  4. lemma OAI.HyperbolicCoding.integerIterate_add line 20
  5. lemma OAI.HyperbolicCoding.integerIterate_succ line 23
  6. lemma OAI.HyperbolicCoding.integerIterate_nat line 26
  7. lemma OAI.HyperbolicCoding.integerIterate_neg_nat line 28
  8. lemma OAI.HyperbolicCoding.integerIterate_nat_fun line 31
  9. lemma OAI.HyperbolicCoding.integerIterate_neg_nat_fun line 33
  10. lemma OAI.HyperbolicCoding.integerIterate_measurable line 35
  11. lemma OAI.HyperbolicCoding.integerIterate_measurePreserving line 41
  12. def OAI.HyperbolicCoding.orbitName line 49
  13. lemma OAI.HyperbolicCoding.measurable_orbitName line 51
  14. lemma OAI.HyperbolicCoding.orbitName_shift line 54
  15. def OAI.HyperbolicCoding.iterateEquiv line 68
  16. lemma OAI.HyperbolicCoding.iterateEquiv_apply line 75
  17. lemma OAI.HyperbolicCoding.iterateEquiv_measurePreserving line 79
  18. lemma OAI.HyperbolicCoding.integerIterate_iterateEquiv line 84
  19. def OAI.HyperbolicCoding.blockObservation line 89
  20. lemma OAI.HyperbolicCoding.measurable_blockObservation line 91
  21. lemma OAI.HyperbolicCoding.grouped_orbitName line 94
  22. theorem OAI.HyperbolicCoding.grouped_names_separate line 98
  23. lemma OAI.HyperbolicCoding.iterateEquiv_symm_apply line 119
  24. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.exists_partitions_tail_trivial line 133
  25. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.powerAtoms_with_rectangle line 175
  26. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.exists_totally_ergodic_rectangle line 204
  27. def OAI.HyperbolicCoding.GoodNames line 227
  28. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.doubleTail_constant_of_good_names line 240
  29. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.tail_trivial_of_good_names line 267
  30. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.exists_good_K_partitions line 292
  31. def OAI.HyperbolicCoding.LawClose line 323
  32. lemma OAI.HyperbolicCoding.LawClose.symm line 326
  33. lemma OAI.HyperbolicCoding.LawClose.triangle line 331
  34. lemma OAI.HyperbolicCoding.LawClose.map line 336
  35. lemma OAI.HyperbolicCoding.real_prod_apply line 342
  36. lemma OAI.HyperbolicCoding.integrable_real_section line 349
  37. lemma OAI.HyperbolicCoding.LawClose.prod_same_left line 358
  38. lemma OAI.HyperbolicCoding.LawClose.prod_same_right line 373
  39. lemma OAI.HyperbolicCoding.LawClose.prod line 378
  40. theorem OAI.HyperbolicCoding.decreasing_projection_limit line 393