OAI/Dynamics/TriangleBilliards/CollisionEscape.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularBilliards.crossMap_flight line 13
  2. lemma OAI.TriangularBilliards.crossMap_abs_le line 18
  3. lemma OAI.TriangularBilliards.wallReflection_fixed_vertex line 23
  4. lemma OAI.TriangularBilliards.Admissible.wall_ne_next line 35
  5. lemma OAI.TriangularBilliards.Admissible.dist_iterate_le_dist_time line 51
  6. lemma OAI.TriangularBilliards.Admissible.positions_converge_of_bounded_time line 60
  7. lemma OAI.TriangularBilliards.Admissible.limit_is_vertex line 72

    Source documentation

    If infinitely many collisions accumulated in finite distance, their common limit would have to be a vertex, not an arbitrary boundary point.

    lemma limit_is_vertex {Q : Triangle} (z : Admissible Q) {p : ℂ}
    (hp : Tendsto (fun n => (z.iterate n).pos) atTop (𝓝 p)) : ∃ k, p = Q.vertex k := by
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Admissible

  8. def OAI.TriangularBilliards.Admissible.momentum line 114

    Source documentation

    Absolute angular momentum about a fixed point.

    def momentum {Q : Triangle} (z : Admissible Q) (p : ℂ) : ℝ :=
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Admissible

  9. lemma OAI.TriangularBilliards.Admissible.momentum_next line 117
  10. lemma OAI.TriangularBilliards.Admissible.momentum_tendsto_zero line 127
  11. lemma OAI.TriangularBilliards.Admissible.eventually_wall_fixed_of_vertex_limit line 134
  12. lemma OAI.TriangularBilliards.Admissible.time_not_bddAbove line 151

    Source documentation

    Non-Zeno is proved, not added as an admissibility hypothesis: finite accumulation would approach a vertex, where conservation of absolute angular momentum forces this regular ray to aim through that vertex.

    lemma time_not_bddAbove {Q : Triangle} (z : Admissible Q) : ¬ BddAbove (range z.time) := by
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.Admissible

  13. lemma OAI.TriangularBilliards.Admissible.time_unbounded_above line 172
  14. lemma OAI.TriangularBilliards.reflect_neg line 181
  15. lemma OAI.TriangularBilliards.vertexExceptional_neg_iff line 184
  16. structure OAI.TriangularBilliards.TwoRays line 192

    Source documentation

    The two genuine recursively generated rays, joined at an interior state.

    structure TwoRays (Q : Triangle) (z : Phase) where
…

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

  17. def OAI.TriangularBilliards.regularRays line 201
  18. def OAI.TriangularBilliards.TwoRays.time line 215
  19. def OAI.TriangularBilliards.TwoRays.point line 220
  20. def OAI.TriangularBilliards.TwoRays.direction line 225
  21. def OAI.TriangularBilliards.TwoRays.wall line 229
  22. lemma OAI.TriangularBilliards.TwoRays.zero_before line 234
  23. lemma OAI.TriangularBilliards.TwoRays.zero_after line 240
  24. lemma OAI.TriangularBilliards.TwoRays.increasing line 245
  25. lemma OAI.TriangularBilliards.TwoRays.unbounded_above line 258
  26. lemma OAI.TriangularBilliards.TwoRays.unbounded_below line 262
  27. lemma OAI.TriangularBilliards.TwoRays.on_side line 269
  28. lemma OAI.TriangularBilliards.TwoRays.middle_point line 277
  29. lemma OAI.TriangularBilliards.TwoRays.start_point line 284
  30. lemma OAI.TriangularBilliards.TwoRays.flight line 291
  31. lemma OAI.TriangularBilliards.TwoRays.middle_flight line 325
  32. lemma OAI.TriangularBilliards.TwoRays.inside line 333
  33. lemma OAI.TriangularBilliards.TwoRays.specular line 369
  34. def OAI.TriangularBilliards.TwoRays.chain line 406

    Source documentation

    The full two-sided, non-Zeno, specular chain, assembled from actual exits.

    def chain : FlightChain Q z where
…

    Mentions: OAI.TriangularBilliards.FlightChain

  35. lemma OAI.TriangularBilliards.exists_chain_of_not_exceptional line 425
  36. lemma OAI.TriangularBilliards.ae_position_in_table line 429
  37. lemma OAI.TriangularBilliards.ae_exists_chain line 440

    Source documentation

    Complete regular trajectories exist for almost every initial state under exact normalized area-angular measure; all collisions and both infinite ends have been constructed above, with no completeness hypothesis.

    lemma ae_exists_chain (Q : Triangle) :
    ∀ᵐ z ∂phaseMeasure Q, Nonempty (FlightChain Q z) := by
…

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