OAI/Dynamics/StandardMap/Components/BirkhoffAtoms.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedSubadditive.ContinuousBirkhoffCode.measurableSet_atom line 15
  2. lemma OAI.BoundedSubadditive.ContinuousBirkhoffCode.invariant_atom line 19
  3. lemma OAI.BoundedSubadditive.ContinuousBirkhoffCode.integral_on_subset_atom line 26
  4. theorem OAI.BoundedSubadditive.ContinuousBirkhoffCode.ergodic_atom line 40
  5. def OAI.StandardMapEntropy.ReversibleGraphRectangle.torusPoint line 108
  6. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.stable_representation line 109
  7. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.unstable_representation line 115
  8. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.torus_nonsingular line 121
  9. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.spectrum_positive line 123
  10. theorem OAI.StandardMapEntropy.actual_rectangle_hopf_atom line 132
  11. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.row_asymptotic line 198
  12. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.column_asymptotic line 207
  13. lemma OAI.StandardMapEntropy.asymptotic_iterate line 217
  14. theorem OAI.StandardMapEntropy.exists_powerBirkhoffCodes line 225
  15. theorem OAI.StandardMapEntropy.actual_rectangle_all_powers_atom line 233
  16. def OAI.AEPeriod.setoid line 284
  17. abbrev OAI.AEPeriod.Class line 288
  18. def OAI.AEPeriod.ofSet line 289
  19. lemma OAI.AEPeriod.ofSet_eq_iff line 290
  20. def OAI.AEPeriod.act line 293
  21. lemma OAI.AEPeriod.act_ofSet line 296
  22. lemma OAI.AEPeriod.iterate_act line 298
  23. lemma OAI.AEPeriod.periodic_iff line 306
  24. lemma OAI.AEPeriod.period_pos line 311
  25. lemma OAI.AEPeriod.period_dvd line 316
  26. lemma OAI.AEPeriod.period_preimage line 320
  27. lemma OAI.AEPeriod.preimage_mod line 324
  28. lemma OAI.AEPeriod.preimage_ne line 330
  29. lemma OAI.BoundedSubadditive.ergodic_restrict_of_normalized line 351
  30. lemma OAI.BoundedSubadditive.ergodic_restrict_subset_of_inter line 356
  31. lemma OAI.BoundedSubadditive.ergodic_restrict_disjoint_or_eq line 366
  32. lemma OAI.BoundedSubadditive.measurePreserving_restrict_of_ae line 375
  33. lemma OAI.BoundedSubadditive.ergodic_restrict_congr line 380
  34. lemma OAI.BoundedSubadditive.preimage_iterate_symm_eq line 384
  35. lemma OAI.BoundedSubadditive.translate_invariant line 391
  36. lemma OAI.BoundedSubadditive.measurePreserving_translate line 399
  37. lemma OAI.BoundedSubadditive.ergodic_translate line 410
  38. structure OAI.BoundedSubadditive.CyclicAtom line 426
  39. lemma OAI.BoundedSubadditive.inverse_preimage_ae line 438
  40. theorem OAI.BoundedSubadditive.finite_cycle_of_ergodic_atom line 448