OAI/Dynamics/StandardMap/Bernoulli/ErgodicAverages.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundedSubadditive.ae_bounded_ergodic_mean line 14
  2. def OAI.HyperbolicCoding.hammingAverage line 35
  3. lemma OAI.HyperbolicCoding.hammingAverage_nonneg line 40
  4. lemma OAI.HyperbolicCoding.nat_eq_of_dist_lt_one line 50
  5. lemma OAI.HyperbolicCoding.compact_label_block line 64
  6. theorem OAI.HyperbolicCoding.full_set_asymptotic_names line 82
  7. lemma OAI.HyperbolicCoding.hammingAverage_le_one line 159
  8. lemma OAI.HyperbolicCoding.measurable_hammingAverage line 173
  9. theorem OAI.HyperbolicCoding.integral_hamming_asymptotic line 184
  10. def OAI.StandardMapEntropy.ReversibleRectangleBlock.carrierProbability line 216
  11. instance OAI.StandardMapEntropy.ReversibleRectangleBlock.carrierProbability_probability line 219
  12. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.carrierProbability_ac line 228
  13. lemma OAI.StandardMapEntropy.quasiMeasurePreserving_normalizedArea line 232
  14. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.carrier_nonsingular line 245
  15. lemma OAI.StandardMapEntropy.ReversibleGraphRectangle.component_for_power line 250
  16. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.name_coupling_cost line 289
  17. theorem OAI.HyperbolicCoding.ae_threshold_avoids_exponential line 323
  18. theorem OAI.HyperbolicCoding.ae_threshold_exponential_tail line 362
  19. def OAI.HyperbolicCoding.ExponentiallyAsymptotic line 390
  20. theorem OAI.HyperbolicCoding.ae_threshold_all_exponential_tails line 395
  21. def OAI.HyperbolicCoding.joinedBinary line 428
  22. lemma OAI.HyperbolicCoding.measurable_joinedBinary line 431
  23. theorem OAI.HyperbolicCoding.exists_good_binary_partitions line 436