RegularRays.lean`

56 declarations, 0 contain sorry, 0 declared as axioms

Finite unfolding and the actual null vertex-aiming exception.

def OAI.TriangularBilliards.crossMap line 15
Source documentation
Oriented angular momentum about the origin against a fixed velocity.
```
def crossMap (v : ℂ) : ℂ →ₗ[ℝ] ℝ where
…
```
lemma OAI.TriangularBilliards.crossMap_unit line 22
lemma OAI.TriangularBilliards.crossMap_ker_ne_top line 28
def OAI.TriangularBilliards.aimingAt line 36
Source documentation
States whose straight starting line passes through p, in either direction.
```
def aimingAt (p : ℂ) : Set Phase := {z | crossMap z.2 (z.1 - p) = 0}
```
Mentions: OAI.TriangularBilliards.Phase, OAI.TriangularBilliards.crossMap
lemma OAI.TriangularBilliards.isClosed_aimingAt line 38
lemma OAI.TriangularBilliards.volume_aimingAt_slice line 43
lemma OAI.TriangularBilliards.phaseMeasure_aimingAt line 53
def OAI.TriangularBilliards.wallReflection line 65
Source documentation
Reflection of a point in the supporting line of a side.
```
def wallReflection (Q : Triangle) (i : Fin 3) (x : ℂ) : ℂ :=
…
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.unfoldedVertex line 69
Source documentation
Finite unfolding places every vertex in the countable reflection orbit.
```
def unfoldedVertex (Q : Triangle) (w : List (Fin 3)) (i : Fin 3) : ℂ :=
…
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.vertexExceptional line 72
lemma OAI.TriangularBilliards.measurableSet_vertexExceptional line 75
lemma OAI.TriangularBilliards.phaseMeasure_vertexExceptional line 81
Source documentation
A concrete, unconditional null exceptional set for all finite unfolding vertex hits, in both time directions and for this exact measure.
```
lemma phaseMeasure_vertexExceptional (Q : Triangle) :
    phaseMeasure Q (vertexExceptional Q) = 0 := by
…
```
Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.phaseMeasure, OAI.TriangularBilliards.vertexExceptional
def OAI.TriangularBilliards.Triangle.slope line 91
lemma OAI.TriangularBilliards.Triangle.coord_shift line 93
lemma OAI.TriangularBilliards.Triangle.sum_slope line 98
lemma OAI.TriangularBilliards.Triangle.slope_joint_injective line 106
lemma OAI.TriangularBilliards.Triangle.exists_slope_neg line 113

lemma OAI.TriangularBilliards.affine_first_exit line 126

Source documentation

Earliest exit for finitely many affine half-planes, including a starting point on an open side with an inward velocity. This is finite real geometry, not an assumed exit-time oracle.

lemma affine_first_exit {ι : Type uIota} [Fintype ι] (a b : ι → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hin : ∀ i, a i = 0 → 0 < b i)
    (hb : ∃ i, b i < 0) :
    ∃ T : ℝ, 0 < T ∧ (∀ t, 0 < t → t < T → ∀ i, 0 < a i + t * b i) ∧
      (∀ i, 0 ≤ a i + T * b i) ∧ (∃ i, a i + T * b i = 0 ∧ b i < 0) := by
…

def OAI.TriangularBilliards.Triangle.Inward line 167
Source documentation
An admissible velocity is strictly inward at every active half-plane.
```
def Inward (Q : Triangle) (x v : ℂ) : Prop :=
…
```
Mentions: OAI.TriangularBilliards.Triangle
lemma OAI.TriangularBilliards.Triangle.inward_of_table line 171
lemma OAI.TriangularBilliards.Triangle.exists_exit line 175
lemma OAI.TriangularBilliards.crossMap_self line 195
lemma OAI.TriangularBilliards.crossMap_reflect line 200
lemma OAI.TriangularBilliards.aimingAt_flight_iff line 209
lemma OAI.TriangularBilliards.vertexExceptional_flight_iff line 215
def OAI.TriangularBilliards.reflectedDirection line 220
Source documentation
Unit outgoing velocity, with exactly the specular law.
```
def reflectedDirection (Q : Triangle) (i : Fin 3) (v : Circle) : Circle :=
…
```
Mentions: OAI.TriangularBilliards.Triangle
lemma OAI.TriangularBilliards.wallReflection_involutive line 224
lemma OAI.TriangularBilliards.wallReflection_sub line 229
lemma OAI.TriangularBilliards.wallReflection_fixed_side line 236
lemma OAI.TriangularBilliards.aimingAt_reflection_iff line 246
lemma OAI.TriangularBilliards.vertexExceptional_reflection_iff line 253
lemma OAI.TriangularBilliards.not_vertex_of_not_exceptional line 270
lemma OAI.TriangularBilliards.Triangle.sum_coord_cyclic line 281
lemma OAI.TriangularBilliards.Triangle.side_of_coords line 292
lemma OAI.TriangularBilliards.Triangle.eq_vertex_of_two_coords_zero line 314
lemma OAI.TriangularBilliards.Triangle.boundary_open_side line 331
lemma OAI.TriangularBilliards.complex_decompose_tangent line 355
lemma OAI.TriangularBilliards.linear_reflect_neg line 364
lemma OAI.TriangularBilliards.Triangle.slope_tangent_zero line 373
lemma OAI.TriangularBilliards.Triangle.slope_reflect line 380
lemma OAI.TriangularBilliards.Triangle.inward_after_reflection line 385
structure OAI.TriangularBilliards.NextCollision line 398
Source documentation
A finite collision datum whose existence is proved from the actual half-plane geometry and the countable unfolded-vertex exception.
```
structure NextCollision (Q : Triangle) (x : ℂ) (v : Circle) where
…
```
Mentions: OAI.TriangularBilliards.Triangle
lemma OAI.TriangularBilliards.exists_next_collision line 407
structure OAI.TriangularBilliards.Admissible line 424
Source documentation
Actual states on a regular recursively extendible ray. Boundary initial states are allowed only with strict inward velocity.
```
structure Admissible (Q : Triangle) where
…
```
Mentions: OAI.TriangularBilliards.Triangle
def OAI.TriangularBilliards.Admissible.collision line 432
def OAI.TriangularBilliards.Admissible.next line 435
def OAI.TriangularBilliards.Admissible.iterate line 441
def OAI.TriangularBilliards.Admissible.time line 445
lemma OAI.TriangularBilliards.Admissible.time_zero line 448
lemma OAI.TriangularBilliards.Admissible.time_succ line 451
lemma OAI.TriangularBilliards.Admissible.time_strictMono line 455
lemma OAI.TriangularBilliards.Admissible.iterate_flight line 461
lemma OAI.TriangularBilliards.Admissible.iterate_inside line 467
lemma OAI.TriangularBilliards.Admissible.iterate_on_side line 474
lemma OAI.TriangularBilliards.Admissible.dist_iterate_succ line 478
lemma OAI.TriangularBilliards.Admissible.dist_iterate_le_time line 484