OAI/Dynamics/StandardMap/Towers/PhaseAveraging.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicCoding.map_restrict_image_equiv line 16
  2. lemma OAI.HyperbolicCoding.map_restrict_finite_iUnion line 23
  3. theorem OAI.HyperbolicCoding.exists_phase_averaging line 29
  4. def OAI.HyperbolicCoding.phaseBlockStart line 66
  5. lemma OAI.HyperbolicCoding.phaseBlockStart_add_lt line 68
  6. lemma OAI.HyperbolicCoding.phaseBlockStart_lt line 76
  7. lemma OAI.HyperbolicCoding.phaseBlockStart_injective line 80
  8. def OAI.HyperbolicCoding.phaseBlockBase line 91
  9. lemma OAI.HyperbolicCoding.measurableSet_phaseBlockBase line 94
  10. lemma OAI.HyperbolicCoding.phaseBlockBase_level line 99
  11. lemma OAI.HyperbolicCoding.phaseBlockBase_disjoint line 109
  12. def OAI.HyperbolicCoding.middleTower line 148
  13. lemma OAI.HyperbolicCoding.measurableSet_middleTower line 152
  14. lemma OAI.HyperbolicCoding.middleTower_disjoint line 157
  15. lemma OAI.HyperbolicCoding.middleTower_measure line 167
  16. theorem OAI.HyperbolicCoding.exists_unbiased_block_base line 176
  17. theorem OAI.HyperbolicCoding.normalized_restriction_lawClose line 221
  18. lemma OAI.HyperbolicCoding.normalized_restriction_observation_close line 258
  19. lemma OAI.HyperbolicCoding.normalize_scaled_observation line 264
  20. lemma OAI.HyperbolicCoding.tower_measure line 289
  21. theorem OAI.HyperbolicCoding.exists_unbiased_rohlin_tower line 296
  22. lemma OAI.HyperbolicCoding.paintTower_repaint_integral line 390
  23. theorem OAI.HyperbolicCoding.realize_tower_coupling line 412
  24. lemma OAI.HyperbolicCoding.tower_decoder_error line 447