OAI/Dynamics/TriangleBilliards/CovariantGenerators.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularBilliards.angularCircleAction line 34

    Source documentation

    The actual oriented tangent-circle representation on the double.

    def angularCircleAction (Q : Triangle) : CircleAction (DoubleL2 Q) (2 * Real.pi) where
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2

  2. lemma OAI.TriangularBilliards.angularCircleAction_coe line 70
  3. instance OAI.TriangularBilliards.circlePeriodPositive line 75
  4. def OAI.TriangularBilliards.angularProjection line 79

    Source documentation

    These are actual Fourier projections of the double, not externally specified coefficient operators.

    def angularProjection (Q : Triangle) (j : ℤ) : DoubleL2 Q →L[ℂ] DoubleL2 Q :=
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2

  5. lemma OAI.TriangularBilliards.angular_projection_complete line 82
  6. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.add line 94
  7. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.smul line 101
  8. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.integral line 106
  9. lemma OAI.TriangularBilliards.rotated_velocity_decompose line 124
  10. lemma OAI.TriangularBilliards.rotated_transverse_decompose line 135
  11. lemma OAI.TriangularBilliards.xDerivative_rotate line 147
  12. lemma OAI.TriangularBilliards.yDerivative_rotate line 155
  13. lemma OAI.TriangularBilliards.circleAction_toLp line 169
  14. lemma OAI.TriangularBilliards.rotate_x_memLp line 176
  15. lemma OAI.TriangularBilliards.rotate_y_memLp line 187
  16. lemma OAI.TriangularBilliards.seam_rotated_generators line 198
  17. def OAI.TriangularBilliards.Analysis.RotationalCR line 268

    Source documentation

    Covariant first-derivative data, stated as actual generator graphs. The smooth seam producer below supplies these graphs for billiard fields.

    def RotationalCR (X Y : HilbertFlow H) (V : CircleAction H T) (u a b : H) : Prop :=
…

    Mentions: OAI.TriangularBilliards.Analysis.HilbertFlow, OAI.TriangularBilliards.Analysis.CircleAction

  18. lemma OAI.TriangularBilliards.Analysis.RotationalCR.generators line 278
  19. lemma OAI.TriangularBilliards.Analysis.RotationalCR.projection line 283