OAI/Dynamics/TriangleBilliards/FourierTails.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.Analysis.CR_components_eq line 45
2. lemma OAI.TriangularBilliards.Analysis.RotationalCR.mode_components line 58
3. lemma OAI.TriangularBilliards.Analysis.CircleAction.inner_of_modes line 91
4. lemma OAI.TriangularBilliards.Analysis.CircleAction.mode_inner_right line 96
5. lemma OAI.TriangularBilliards.Analysis.CircleAction.mode_inner_left line 100
6. lemma OAI.TriangularBilliards.Analysis.invariant_CR_recurrence line 109

   Source documentation

   The Fourier recurrence from exact invariance, justified on a dense regular CR core and then on all L2 tests. It never differentiates an infinite Fourier series term by term.

   lemma invariant_CR_recurrence (X Y : HilbertFlow H) (V : CircleAction H T)
       (hD : Dense {v : H | ∃ c d, RotationalCR X Y V v c d})
       {f : H} (hf : X.HasGenerator f 0) (a b : ℤ → H)
       (hg : ∀ j, RotationalCR X Y V (V.projection j f) (a j) (b j)) (m : ℤ) :
       a m + b (m+2) = 0 := by
   …

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

7. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.zero line 150
8. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.sum line 155
9. lemma OAI.TriangularBilliards.Analysis.CircleAction.bounded_modes_weaklyTendsto line 166
10. lemma OAI.TriangularBilliards.Analysis.parity_tail_endpoint line 181

    Source documentation

    The one-sided parity tail has the claimed L2 generator. The uniformly bounded terminal term disappears WEAKLY by escaping angular frequency.

    lemma parity_tail_endpoint (X Y : HilbertFlow H) (V : CircleAction H T)
        (hD : Dense {v : H | ∃ c d, RotationalCR X Y V v c d})
        {f : H} (hf : X.HasGenerator f 0) (a b : ℤ → H)
        (hg : ∀ j, RotationalCR X Y V (V.projection j f) (a j) (b j))
        {C : ℝ} (ha : ∀ j, ‖a j‖ ≤ C) (m : ℤ) :
        X.HasGenerator (V.parityTail m f) (b m) := by
    …

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

11. lemma OAI.TriangularBilliards.dense_rotationalCR_core line 226
12. lemma OAI.TriangularBilliards.bounded_invariant_tail_endpoint line 266

    Source documentation

    The actual triangular parity-tail endpoint. There is no unproved smooth-core density assumption remaining in this application.

    lemma bounded_invariant_tail_endpoint (Q : Triangle) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ {H : ℝ} {f : DoublePhase → ℂ}
          (_hm : StronglyMeasurable f) (hf : MemLp f 2 (doubleMeasure Q))
          (_hH : ∀ z, ‖f z‖ ≤ H)
          (_hfi : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) 0),
          ∃ a b : ℤ → DoubleL2 Q,
            (∀ j, RotationalCR (geodesicHilbertFlow Q) (transverseHilbertFlow Q)
              (angularCircleAction Q) ((angularCircleAction Q).projection j (hf.toLp f)) (a j) (b j)) ∧
            (∀ j, ‖a j‖ ≤ C*H ∧ ‖b j‖ ≤ C*H) ∧
            ∀ m, (geodesicHilbertFlow Q).HasGenerator
              ((angularCircleAction Q).parityTail m (hf.toLp f)) (b m) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.transverseHilbertFlow, OAI.TriangularBilliards.angularCircleAction