OAI/Dynamics/TriangleBilliards/TransverseFlow.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.hasGenerator_of_hasDerivAt_zero line 31

   Source documentation

   A genuine strong derivative at zero determines the entire closed unitary generator; the group law transports it to every time.

   lemma hasGenerator_of_hasDerivAt_zero {u v : H}
       (h : HasDerivAt (fun t => W.act t u) v 0) : W.HasGenerator u v := by
   …

2. lemma OAI.TriangularBilliards.seam_geodesic_generator line 54

   Source documentation

   The spatial derivative of a smooth seam field is the actual strong Koopman generator, including trajectories with arbitrarily many reflections. The asserted generator is proved, not added as a hypothetical analytic input.

   lemma seam_geodesic_generator {Q : Triangle} {f : DoublePhase → ℂ}
       (hs : SeamCompatible Q f)
       (hd : ∀ v b, Differentiable ℝ (fun x => f ((x, v), b)))
       {C : ℝ≥0} (hC : ∀ x v b, ‖fderiv ℝ (fun y => f ((y,v),b)) x‖ ≤ C)
       (hf : MemLp f 2 (doubleMeasure Q))
       (hxf : MemLp (xDerivative f) 2 (doubleMeasure Q)) :
       (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) (hxf.toLp (xDerivative f)) := by
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.SeamCompatible, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.xDerivative, OAI.TriangularBilliards.geodesicHilbertFlow

3. lemma OAI.TriangularBilliards.parity_add_one_ne_zero_iff line 84
4. lemma OAI.TriangularBilliards.reflectedDirection_mul line 87
5. lemma OAI.TriangularBilliards.doubleRotate_seam line 96
6. lemma OAI.TriangularBilliards.SeamCompatible.rotate line 106
7. lemma OAI.TriangularBilliards.wallReflection_hasFDerivAt line 115
8. lemma OAI.TriangularBilliards.SeamCompatible.xDerivative line 125
9. lemma OAI.TriangularBilliards.xDerivative_contDiff line 140

   Source documentation

   Spatial smoothness does not require angular differentiability.

   lemma xDerivative_contDiff {f : DoublePhase → ℂ}
       (hf : ∀ v b, ContDiff ℝ ∞ (fun x => f ((x,v),b))) (v : Circle) (b : ZMod 2) :
       ContDiff ℝ ∞ (fun x => xDerivative f ((x,v),b)) := by
   …

   Mentions: OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.xDerivative

10. def OAI.TriangularBilliards.transverseVelocity line 147

    Source documentation

    The transverse velocity in the oriented sheet.

    def transverseVelocity (v : Circle) (b : ZMod 2) : ℂ :=
    …

11. def OAI.TriangularBilliards.yDerivative line 150
12. lemma OAI.TriangularBilliards.yDerivative_contDiff line 153
13. lemma OAI.TriangularBilliards.reflect_transverseVelocity line 159
14. lemma OAI.TriangularBilliards.SeamCompatible.yDerivative line 174
15. lemma OAI.TriangularBilliards.x_y_commute line 191
16. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.conjugate line 207
17. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.commuting_generators_inner line 218
18. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.commuting_generators_CR line 226
19. lemma OAI.TriangularBilliards.circle_exp_quarter_coe line 250
20. lemma OAI.TriangularBilliards.transverseVelocity_neg_quarter line 255
21. lemma OAI.TriangularBilliards.xDerivative_rotate_neg_quarter line 267
22. lemma OAI.TriangularBilliards.angular_toLp line 274
23. lemma OAI.TriangularBilliards.seam_transverse_generator line 281