OAI/Dynamics/StandardMap/Bernoulli/ErgodicL1.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.orbitAverage line 13
  2. lemma OAI.HyperbolicCoding.orbitAverage_integrable line 17
  3. lemma OAI.HyperbolicCoding.orbitAverage_sub line 22
  4. lemma OAI.HyperbolicCoding.orbitAverage_abs_le line 27
  5. lemma OAI.HyperbolicCoding.integral_orbitAverage line 33
  6. lemma OAI.HyperbolicCoding.orbitAverage_L1_contraction line 44
  7. theorem OAI.HyperbolicCoding.ergodic_L1_unit line 54
  8. theorem OAI.HyperbolicCoding.ergodic_L1_bounded line 83
  9. lemma OAI.HyperbolicCoding.ergodic_L1_error_bound line 125
  10. theorem OAI.HyperbolicCoding.ergodic_L1 line 151
  11. def OAI.HyperbolicCoding.cesaroLawMass line 184
  12. lemma OAI.HyperbolicCoding.iterateLawMass_density line 187
  13. lemma OAI.HyperbolicCoding.cesaroLawMass_density line 203
  14. theorem OAI.HyperbolicCoding.cesaro_ac_uniform line 215
  15. lemma OAI.HyperbolicCoding.remotePair_translate line 242
  16. lemma OAI.HyperbolicCoding.remoteProduct_drop line 257
  17. lemma OAI.HyperbolicCoding.RemoteIndependent.translate line 266
  18. lemma OAI.HyperbolicCoding.cesaroLawMass_close line 290
  19. theorem OAI.HyperbolicCoding.weakBernoulli_of_ac_remote line 306
  20. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.weakBernoulli_of_good_names line 344
  21. theorem OAI.StandardMapEntropy.ReversibleGraphRectangle.exists_weakBernoulli_partitions line 380
  22. theorem OAI.StandardMapEntropy.actual_weakBernoulli_component line 393
  23. lemma OAI.HyperbolicCoding.tailName_commute line 419
  24. theorem OAI.HyperbolicCoding.WeakBernoulliProcess.translate line 424
  25. theorem OAI.StandardMapEntropy.actual_cyclic_weakBernoulli_component line 453
  26. theorem OAI.StandardMapEntropy.eventually_actual_cyclic_weakBernoulli_component line 525