OAI/Dynamics/StandardMap/Bernoulli/RohlinSinaiFinite.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.zero_entropy_opposite_factor line 16
  2. theorem OAI.HyperbolicCoding.TailObservable.reverse line 79
  3. lemma OAI.HyperbolicCoding.TailEvent.congr line 96
  4. lemma OAI.HyperbolicCoding.TailEvent.nullMeasurable line 101
  5. lemma OAI.HyperbolicCoding.TailEvent.univ line 106
  6. lemma OAI.HyperbolicCoding.TailEvent.compl line 110
  7. lemma OAI.HyperbolicCoding.TailEvent.iInter line 117
  8. lemma OAI.HyperbolicCoding.TailEvent.inter line 126
  9. lemma OAI.HyperbolicCoding.TailEvent.preimage line 135
  10. lemma OAI.HyperbolicCoding.TailEvent.inverse_preimage line 151
  11. lemma OAI.HyperbolicCoding.TailEvent.reverse line 165
  12. def OAI.HyperbolicCoding.IsTailAtom line 197
  13. theorem OAI.HyperbolicCoding.exists_tailAtom_of_local_constancy line 200
  14. theorem OAI.HyperbolicCoding.tail_trivial_of_atom line 236
  15. lemma OAI.HyperbolicCoding.law_distance_le_disagreement line 279
  16. lemma OAI.HyperbolicCoding.tail_disagreement_tendsto_zero line 292
  17. theorem OAI.HyperbolicCoding.product_remote_tail_independence line 329
  18. lemma OAI.HyperbolicCoding.map_withDensity_comp line 384
  19. theorem OAI.HyperbolicCoding.exists_exact_density_lift line 392
  20. theorem OAI.HyperbolicCoding.tailAtom_of_rectangle line 450