OAI/Dynamics/TriangleBilliards/Unfolding.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularBilliards.phaseWord line 11
2. lemma OAI.TriangularBilliards.measurePreserving_phaseWord line 14
3. lemma OAI.TriangularBilliards.wallPhase_involutive line 20
4. def OAI.TriangularBilliards.FlightChain.line line 29
5. lemma OAI.TriangularBilliards.FlightChain.line_zero line 32
6. lemma OAI.TriangularBilliards.FlightChain.line_succ line 41
7. lemma OAI.TriangularBilliards.FlightChain.line_pred line 63
8. lemma OAI.TriangularBilliards.FlightChain.line_unfold line 69
9. lemma OAI.TriangularBilliards.FlightChain.at_unfold line 82

   Source documentation

   Every fixed-time endpoint is the value of one of countably many genuine ambient measure-preserving Euclidean reflection/free-flight maps.

   lemma at_unfold {Q : Triangle} {z : Phase} (c : FlightChain Q z) (t : ℝ) :
       ∃ w : List (Fin 3), c.at t = phaseWord Q w (freeFlow t z) := by
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.FlightChain, OAI.TriangularBilliards.phaseWord, OAI.TriangularBilliards.freeFlow

10. lemma OAI.TriangularBilliards.phaseMeasure_eq_restrict line 94
11. lemma OAI.TriangularBilliards.phaseMeasure_absolutelyContinuous line 99
12. lemma OAI.TriangularBilliards.side_mem_frontier line 103
13. def OAI.TriangularBilliards.boundaryPhase line 112

    Source documentation

    All boundary-position phases form a measurable ambient-null set.

    def boundaryPhase (Q : Triangle) : Set Phase :=
    …

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

14. lemma OAI.TriangularBilliards.measurableSet_boundaryPhase line 115
15. lemma OAI.TriangularBilliards.ambientMeasure_boundaryPhase line 118
16. def OAI.TriangularBilliards.collisionExceptional line 124

    Source documentation

    A countable explicit null superset of all trajectories at a boundary at a prescribed time; it is defined without making trajectory choices.

    def collisionExceptional (Q : Triangle) (t : ℝ) : Set Phase :=
    …

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

17. lemma OAI.TriangularBilliards.measurableSet_collisionExceptional line 127
18. lemma OAI.TriangularBilliards.phaseMeasure_collisionExceptional line 132
19. lemma OAI.TriangularBilliards.FlightChain.mem_collisionExceptional line 140
20. def OAI.TriangularBilliards.regularAt line 152

    Source documentation

    Remove only the fixed-time collision set from the conull regular states.

    def regularAt (Q : Triangle) (t : ℝ) : Set Phase :=
    …

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

21. lemma OAI.TriangularBilliards.measurableSet_regularAt line 155
22. lemma OAI.TriangularBilliards.ae_regularAt line 158
23. lemma OAI.TriangularBilliards.regularAt_subset_table line 163
24. lemma OAI.TriangularBilliards.regularAt_noncollision line 167
25. lemma OAI.TriangularBilliards.flow_mem_table_of_regularAt line 171
26. lemma OAI.TriangularBilliards.flow_injective_regularAt line 180
27. lemma OAI.TriangularBilliards.billiardFlow_cocycle line 192

    Source documentation

    The flow law for every real pair, outside a proved null set.

    lemma billiardFlow_cocycle (Q : Triangle) (s t : ℝ) :
        billiardFlow Q (s + t) =ᵐ[phaseMeasure Q] (billiardFlow Q s ∘ billiardFlow Q t) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.billiardFlow, OAI.TriangularBilliards.phaseMeasure