OAI/Dynamics/TriangleBilliards/Koopman.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space analysis of actual measurable measure-preserving flows. The continuity hypothesis below is only slice-wise almost everywhere and therefore applies to billiards at each fixed time, despite wall collisions.

  1. lemma OAI.TriangularBilliards.Analysis.norm_sq_L2 line 29
  2. def OAI.TriangularBilliards.Analysis.koopman line 39
  3. lemma OAI.TriangularBilliards.Analysis.coe_koopman line 43
  4. lemma OAI.TriangularBilliards.Analysis.koopman_bounded_continuous line 47
  5. lemma OAI.TriangularBilliards.Analysis.continuous_koopman_bounded line 53
  6. lemma OAI.TriangularBilliards.Analysis.continuous_koopman line 93
  7. lemma OAI.TriangularBilliards.Analysis.continuous_koopman_time line 105