OAI/Dynamics/TriangleBilliards/DoubleFlow.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The actual oriented double of the billiard, in its full-measure pair of interior charts. The second coordinate records the parity of reflections; it is not an independent randomization of the dynamics.

  1. abbrev OAI.TriangularBilliards.DoublePhase line 20
  2. def OAI.TriangularBilliards.parityMeasure line 22
  3. instance OAI.TriangularBilliards.parityMeasure_probability line 24
  4. def OAI.TriangularBilliards.doubleMeasure line 29
  5. instance OAI.TriangularBilliards.doubleMeasure_probability line 31
  6. lemma OAI.TriangularBilliards.measurePreserving_parity_add line 35
  7. def OAI.TriangularBilliards.collisionIndex line 43
  8. lemma OAI.TriangularBilliards.collisionIndex_spec line 47
  9. lemma OAI.TriangularBilliards.collisionIndex_eq line 56
  10. lemma OAI.TriangularBilliards.measurable_collisionIndex line 60
  11. lemma OAI.TriangularBilliards.collisionIndex_zero line 69
  12. def OAI.TriangularBilliards.doubleFlow line 76

    Source documentation

    Unit-speed geodesic flow of the oriented double in the two interior charts.

    def doubleFlow (Q : Triangle) (t : ℝ) (z : DoublePhase) : DoublePhase :=
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase

  13. lemma OAI.TriangularBilliards.measurable_doubleFlow line 79
  14. lemma OAI.TriangularBilliards.measurable_doubleFlow_time line 88
  15. lemma OAI.TriangularBilliards.measurePreserving_doubleFlow line 92
  16. lemma OAI.TriangularBilliards.doubleFlow_zero line 99
  17. lemma OAI.TriangularBilliards.collisionIndex_rebase line 102
  18. lemma OAI.TriangularBilliards.doubleFlow_add_of_noncollision line 118
  19. lemma OAI.TriangularBilliards.doubleFlow_cocycle line 130
  20. def OAI.TriangularBilliards.doubleRotate line 140

    Source documentation

    Rotation in the oriented tangent circle; the negative copy has the opposite physical rotation, exactly as in a conjugate Euclidean chart.

    def doubleRotate (a : Circle) (z : DoublePhase) : DoublePhase :=
…

    Mentions: OAI.TriangularBilliards.DoublePhase

  21. lemma OAI.TriangularBilliards.measurable_doubleRotate line 143
  22. lemma OAI.TriangularBilliards.measurePreserving_doubleRotate line 147
  23. lemma OAI.TriangularBilliards.doubleRotate_one line 161
  24. lemma OAI.TriangularBilliards.doubleRotate_mul line 164
  25. lemma OAI.TriangularBilliards.doubleFlow_on_flight line 168
  26. lemma OAI.TriangularBilliards.continuousAt_doubleFlow_of_noncollision line 175
  27. lemma OAI.TriangularBilliards.ae_continuousAt_doubleFlow line 192