OAI/Dynamics/TriangleBilliards/AngularMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularBilliards.angleMeasure line 15

   Source documentation

   Angular Haar probability in additive angle coordinates, used to verify invariance of the explicit angular measure.

   def angleMeasure : Measure (AddCircle (2 * Real.pi)) :=
   …

2. lemma OAI.TriangularBilliards.measurePreserving_toCircle line 18
3. lemma OAI.TriangularBilliards.measurePreserving_circle_mul line 32
4. lemma OAI.TriangularBilliards.measurePreserving_circle_inv line 49
5. lemma OAI.TriangularBilliards.reflectedDirection_eq line 63
6. lemma OAI.TriangularBilliards.measurePreserving_reflectedDirection line 69
7. lemma OAI.TriangularBilliards.measurePreserving_wallReflection line 76
8. def OAI.TriangularBilliards.ambientMeasure line 87

   Source documentation

   Ambient Liouville measure, before restriction and normalization.

   def ambientMeasure : Measure Phase := volume.prod angularMeasure

   Mentions: OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.angularMeasure

9. def OAI.TriangularBilliards.wallPhase line 90

   Source documentation

   Reflection at a whole supporting line, on the ambient phase space.

   def wallPhase (Q : Triangle) (i : Fin 3) (z : Phase) : Phase :=
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase

10. lemma OAI.TriangularBilliards.measurePreserving_wallPhase line 93
11. def OAI.TriangularBilliards.freeFlow line 98

    Source documentation

    The free-flight shear on the whole plane, without any boundary.

    def freeFlow (t : ℝ) (z : Phase) : Phase := (z.1 + t • (z.2 : ℂ), z.2)

    Mentions: OAI.TriangularBilliards.Phase

12. lemma OAI.TriangularBilliards.measurePreserving_freeFlow line 100