OAI/Dynamics/TriangleBilliards/LongTrajectories.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.FlightChain.dist_point_succ line 45
2. lemma OAI.TriangularBilliards.FlightChain.dist_point_le line 51
3. lemma OAI.TriangularBilliards.FlightChain.position_dist_le line 63
4. lemma OAI.TriangularBilliards.billiard_position_lipschitz line 105
5. lemma OAI.TriangularBilliards.Triangle.clearance_flow_lipschitz line 118
6. def OAI.TriangularBilliards.goodMesh line 131

   Source documentation

   A finite measurable subset of the good set. Sampling one extra endpoint keeps all sample times simple multiples of the mesh width.

   def goodMesh (Q : Triangle) (L ε T : ℝ) : Set DoublePhase :=
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase

7. lemma OAI.TriangularBilliards.goodMesh_measurable line 135
8. lemma OAI.TriangularBilliards.goodMesh_clearance line 144
9. lemma OAI.TriangularBilliards.badMesh_measure_bound line 169
10. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_mem_convex line 203
11. lemma OAI.TriangularBilliards.Analysis.isClosed_ae_mem line 226

    Source documentation

    Measurable functions with values almost everywhere in prescribed closed convex fibers form a closed convex subset of the actual L² space.

    lemma isClosed_ae_mem (C : A → Set ℂ) (hc : ∀ z, IsClosed (C z)) :
        IsClosed {u : Lp ℂ 2 μ | ∀ᵐ z ∂μ, u z ∈ C z} := by
    …

12. lemma OAI.TriangularBilliards.Analysis.convex_ae_mem line 234
13. lemma OAI.TriangularBilliards.Analysis.isClosed_ae_bounded line 243
14. lemma OAI.TriangularBilliards.Analysis.convex_ae_bounded line 248
15. lemma OAI.TriangularBilliards.Analysis.isClosed_ae_zero_on line 253
16. lemma OAI.TriangularBilliards.Analysis.convex_ae_zero_on line 264
17. lemma OAI.TriangularBilliards.Analysis.restrictL2_ae_bounded line 281
18. lemma OAI.TriangularBilliards.Analysis.restrictL2_sub_self line 290