OAI/Dynamics/TriangleBilliards/Geometry.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Elementary facts about complete specular trajectories.

  1. lemma OAI.TriangularBilliards.reflect_add line 12
  2. lemma OAI.TriangularBilliards.reflect_real_smul line 15
  3. lemma OAI.TriangularBilliards.reflect_involutive line 19
  4. lemma OAI.TriangularBilliards.reflect_norm line 24
  5. lemma OAI.TriangularBilliards.reflect_tangent line 27
  6. lemma OAI.TriangularBilliards.reflect_normal line 30
  7. lemma OAI.TriangularBilliards.FlightChain.exists_flight line 39
  8. lemma OAI.TriangularBilliards.FlightChain.flight_index_unique line 56
  9. lemma OAI.TriangularBilliards.FlightChain.at_of_flight line 69
  10. lemma OAI.TriangularBilliards.FlightChain.at_zero line 77
  11. lemma OAI.TriangularBilliards.FlightChain.initial_inside line 85
  12. lemma OAI.TriangularBilliards.FlightChain.position_at_interior line 90
  13. lemma OAI.TriangularBilliards.FlightChain.constant_direction_on_flight line 96
  14. lemma OAI.TriangularBilliards.FlightChain.unit_speed_on_flight line 101
  15. lemma OAI.TriangularBilliards.billiardFlow_zero line 112
  16. lemma OAI.TriangularBilliards.Triangle.isOpen_table line 120
  17. lemma OAI.TriangularBilliards.Triangle.measurableSet_table line 122
  18. lemma OAI.TriangularBilliards.Triangle.table_nonempty line 125
  19. lemma OAI.TriangularBilliards.Triangle.area_pos line 130
  20. lemma OAI.TriangularBilliards.Triangle.area_lt_top line 133
  21. lemma OAI.TriangularBilliards.Triangle.normalized_area_univ line 137
  22. lemma OAI.TriangularBilliards.Triangle.tangent_ne_zero line 142
  23. lemma OAI.TriangularBilliards.angularMeasure_univ line 148
  24. instance OAI.TriangularBilliards.angularMeasure_probability line 154
  25. lemma OAI.TriangularBilliards.phaseMeasure_univ line 157
  26. instance OAI.TriangularBilliards.phaseMeasure_probability line 161
  27. def OAI.TriangularBilliards.Triangle.basis line 167

    Source documentation

    Barycentric coordinates for the exact, nondegenerate table.

    def basis (Q : Triangle) : AffineBasis (Fin 3) ℝ ℂ where
…

    Mentions: OAI.TriangularBilliards.Triangle

  28. lemma OAI.TriangularBilliards.Triangle.table_iff_coords line 173
  29. lemma OAI.TriangularBilliards.Triangle.side_coord_zero_iff line 179
  30. lemma OAI.TriangularBilliards.Triangle.side_not_table line 189
  31. lemma OAI.TriangularBilliards.Triangle.side_index_unique line 196
  32. lemma OAI.TriangularBilliards.irrational_holonomy_ne_one line 206

    Source documentation

    The irrational-holonomy scalar for every irrational angle, with no Diophantine bound.

    lemma irrational_holonomy_ne_one {α : ℝ} (hα : Irrational (α / Real.pi))
    {j : ℤ} (hj : j ≠ 0) :
    Complex.exp (2 * (j : ℂ) * (α : ℂ) * Complex.I) ≠ 1 := by
…
  33. lemma OAI.TriangularBilliards.parallel_mode_zero line 217
  34. def OAI.TriangularBilliards.reflectIsometry line 225

    Source documentation

    The reflection is a genuine real-linear Euclidean isometry.

    def reflectIsometry (e : ℂ) (he : e ≠ 0) : ℂ ≃ₗᵢ[ℝ] ℂ where
…
  35. lemma OAI.TriangularBilliards.exit_time_unique line 234
  36. lemma OAI.TriangularBilliards.entry_time_unique line 243