OAI/Dynamics/StandardMap/Towers/FiniteCouplingRealization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.realize_finite_coupling_finite line 16
  2. lemma OAI.HyperbolicCoding.integral_cost_of_realization line 38
  3. lemma OAI.HyperbolicCoding.finite_symbolCost_integral line 47
  4. theorem OAI.HyperbolicCoding.exists_independent_finite_phase line 71
  5. lemma OAI.HyperbolicCoding.finite_phase_factor line 105
  6. def OAI.HyperbolicCoding.disjointIndex line 126
  7. lemma OAI.HyperbolicCoding.disjointIndex_some line 132
  8. lemma OAI.HyperbolicCoding.disjointIndex_none line 149
  9. lemma OAI.HyperbolicCoding.measurable_disjointIndex line 160
  10. def OAI.HyperbolicCoding.disjointPaste line 178
  11. lemma OAI.HyperbolicCoding.disjointPaste_on line 185
  12. lemma OAI.HyperbolicCoding.disjointPaste_off line 192
  13. lemma OAI.HyperbolicCoding.measurable_disjointPaste line 198
  14. def OAI.HyperbolicCoding.entryLevel line 220
  15. lemma OAI.HyperbolicCoding.measurableSet_entryLevel line 223
  16. lemma OAI.HyperbolicCoding.entryLevel_disjoint line 233
  17. lemma OAI.HyperbolicCoding.mem_entryLevel_iterate line 242
  18. lemma OAI.HyperbolicCoding.mem_entryLevel_back line 250
  19. lemma OAI.HyperbolicCoding.ae_exists_entry line 266
  20. def OAI.HyperbolicCoding.entryTowerBase line 289
  21. lemma OAI.HyperbolicCoding.measurableSet_entryTowerBase line 292
  22. lemma OAI.HyperbolicCoding.entryTower_disjoint line 296
  23. lemma OAI.HyperbolicCoding.entryTower_covers line 319
  24. lemma OAI.HyperbolicCoding.measurableSet_iterate_image line 349
  25. lemma OAI.HyperbolicCoding.entryTower_error line 354
  26. lemma OAI.HyperbolicCoding.exists_small_positive_marker line 374
  27. theorem OAI.HyperbolicCoding.exists_rohlin_tower line 382
  28. def OAI.HyperbolicCoding.paintTower line 408
  29. lemma OAI.HyperbolicCoding.measurable_paintTower line 414
  30. lemma OAI.HyperbolicCoding.paintTower_level line 422
  31. lemma OAI.HyperbolicCoding.paintTower_word line 431
  32. lemma OAI.HyperbolicCoding.paintTower_off line 439
  33. lemma OAI.HyperbolicCoding.measure_iterate_image line 444
  34. theorem OAI.HyperbolicCoding.paintTower_repaint line 461