OAI/Dynamics/TriangleBilliards/WeakGenerators.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.HasGenerator.weak_limit line 46
2. lemma OAI.TriangularBilliards.Analysis.HilbertFlow.exists_generator_of_bounded_approx line 51
3. lemma OAI.TriangularBilliards.supported_smoothing_toLp_tendsto line 67
4. lemma OAI.TriangularBilliards.bounded_invariant_modes line 83

   Source documentation

   Bounded modes for the nonsingular billiard unitary groups. Only individual Fourier derivatives are bounded; this does not impose a bound on the sum of all mode derivatives.

   lemma bounded_invariant_modes (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) (j : ℤ),
         ∃ dx dy : Lp ℂ 2 (doubleMeasure Q),
           (geodesicHilbertFlow Q).HasGenerator ((angularCircleAction Q).projection j (hf.toLp f)) dx ∧
           (transverseHilbertFlow Q).HasGenerator ((angularCircleAction Q).projection j (hf.toLp f)) dy ∧
           ‖dx‖ ≤ C * H ∧ ‖dy‖ ≤ C * H := by
   …

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

5. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.map line 132
6. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.add line 135
7. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.sub line 140
8. lemma OAI.TriangularBilliards.Analysis.RotationalCR.weak_limit line 156
9. lemma OAI.TriangularBilliards.Analysis.RotationalCR.exists_of_bounded_approx line 171
10. lemma OAI.TriangularBilliards.Analysis.RotationalCR.components_unique line 183

    Source documentation

    In a single Fourier mode, the two CR components are exactly the two Fourier components of its geodesic generator.

    lemma components_unique {u a b dx : H} {j : ℤ}
        (h : RotationalCR X Y V u a b)
        (ha : V.projection (j+1) a = a) (hb : V.projection (j-1) b = b)
        (hx : X.HasGenerator u dx) :
        a = V.projection (j+1) dx ∧ b = V.projection (j-1) dx := by
    …

    Mentions: OAI.TriangularBilliards.Analysis.RotationalCR

11. lemma OAI.TriangularBilliards.supportedSmoothing_rotationalCR line 203
12. lemma OAI.TriangularBilliards.bounded_invariant_regularized_CR line 220
13. lemma OAI.TriangularBilliards.bounded_invariant_CR line 252