OAI/Dynamics/StandardMap/Coupling/RelativeFiniteRealization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.finite_map_eq_of_mass line 15
  2. lemma OAI.HyperbolicCoding.mass_eq_of_map_eq line 26
  3. lemma OAI.HyperbolicCoding.relative_finite_realization line 34
  4. lemma OAI.HyperbolicCoding.map_restrict_factor line 53
  5. lemma OAI.HyperbolicCoding.factor_iterate line 59
  6. lemma OAI.HyperbolicCoding.factor_word line 67
  7. lemma OAI.HyperbolicCoding.factor_tower_level line 74
  8. lemma OAI.HyperbolicCoding.relative_tower_base_copy line 102
  9. lemma OAI.HyperbolicCoding.equal_base_level_laws line 139
  10. lemma OAI.HyperbolicCoding.lawClose_of_common_restriction line 181
  11. lemma OAI.HyperbolicCoding.tower_disjoint_mono line 211
  12. lemma OAI.HyperbolicCoding.equal_base_interior_laws line 220
  13. lemma OAI.HyperbolicCoding.tower_interior_compl_bound line 241
  14. theorem OAI.HyperbolicCoding.relative_measurable_graph_approx line 280
  15. lemma OAI.HyperbolicCoding.finite_sigma_set_approx line 336
  16. theorem OAI.HyperbolicCoding.finite_factor_approx line 367
  17. lemma OAI.HyperbolicCoding.joinedBinary_comap_monotone line 415
  18. lemma OAI.HyperbolicCoding.joinedBinary_generates line 425
  19. theorem OAI.HyperbolicCoding.joinedBinary_approximates line 452