OAI/Analysis/IrrationalRotation/Product/OneCoordinateCrossing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.OneCoordinateCoupling.ofReal_total line 11
  2. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_ge_one line 22
  3. lemma OAI.Invariant233.OneCoordinateCoupling.intervalLaw_Ici_eq_one line 28
  4. lemma OAI.Invariant233.OneCoordinateCoupling.intervalLaw_Iio_eq_one line 35
  5. lemma OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_component_lower line 50
  6. lemma OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_component_lower line 65
  7. theorem OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_crossing_lower line 80
  8. theorem OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_crossing_lower line 105
  9. lemma OAI.Invariant233.OneCoordinateCoupling.intervalDensity_ge_one_of_mem line 136
  10. theorem OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_event_lower line 151
  11. theorem OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_event_lower line 173
  12. theorem OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_crossing line 195
  13. theorem OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_crossing line 216
  14. theorem OAI.Invariant233.OneCoordinateCoupling.pairLaw_fst_ae_mem_unit line 237
  15. theorem OAI.Invariant233.OneCoordinateCoupling.pairLaw_snd_ae_mem_unit line 242
  16. theorem OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_ae_all_crossings line 247
  17. theorem OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_ae_all_crossings line 255