OAI/Dynamics/TriangleBilliards/HilbertFlow.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Strongly continuous unitary dynamics and the closed generator graph. All hypotheses here are structural flow properties; the billiard instance is constructed from its geometric flow, not postulated.

  1. structure OAI.TriangularBilliards.Analysis.HilbertFlow line 32
  2. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.act_zero line 42
  3. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.act_neg line 44
  4. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.inner_act line 47
  5. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.continuous_joint line 50
  6. def OAI.TriangularBilliards.Analysis.HilbertFlow.conjugate line 58

    Source documentation

    Conjugating by a second genuine unitary flow preserves all structural properties. For billiards the second flow is angular rotation.

    def conjugate (V : HilbertFlow H) (θ : ℝ) : HilbertFlow H where
…

    Mentions: OAI.TriangularBilliards.Analysis.HilbertFlow

  7. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.conjugate_joint line 69
  8. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.intervalIntegrable line 79
  9. def OAI.TriangularBilliards.Analysis.HilbertFlow.timeIntegral line 85

    Source documentation

    Integration in time, as a genuine bounded linear operator. No operator-norm continuity of the unitary group is presupposed.

    def timeIntegral (a b : ℝ) : H →L[ℂ] H :=
…
  10. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.timeIntegral_apply line 102
  11. def OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator line 107

    Source documentation

    The generator domain encoded by the exact orbit integral identity. This formulation makes weak closedness an immediate linear-test fact.

    def HasGenerator (u v : H) : Prop :=
…
  12. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.hasDerivAt line 110
  13. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.hasGenerator_of_hasDerivAt line 123
  14. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.generator_unique line 129
  15. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.generator_skew line 134
  16. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.generatorGraph_closed line 143
  17. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.generatorGraph_convex line 154
  18. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.timeIntegral_translate line 166
  19. def OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage line 176

    Source documentation

    The finite negative-time average.

    def negativeAverage (T : ℝ) : H →L[ℂ] H := (T⁻¹ : ℝ) • W.timeIntegral (-T) 0
…
  20. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_eq line 179
  21. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_norm_le line 187
  22. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.timeIntegral_hasDerivAt_right line 199
  23. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.timeIntegral_hasDerivAt_translate line 204
  24. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_generator line 219
  25. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_generator_norm line 242
  26. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_invariant line 251
  27. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.negativeAverage_dist_invariant line 258