OAI/Dynamics/TriangleBilliards/Localization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularBilliards.Analysis.restrictL2 line 40
2. lemma OAI.TriangularBilliards.Analysis.restrictL2_coe line 75
3. lemma OAI.TriangularBilliards.Analysis.restrictL2_selfadjoint line 79
4. lemma OAI.TriangularBilliards.Analysis.restrictL2_fixed line 89
5. lemma OAI.TriangularBilliards.Analysis.restrictL2_commute line 98
6. lemma OAI.TriangularBilliards.Analysis.restrictL2_norm line 116
7. lemma OAI.TriangularBilliards.spatialRestriction_commute line 130
8. lemma OAI.TriangularBilliards.seam_localized_energy line 141

   Source documentation

   The localized energy bound on the actual smooth core. Every generator and Fourier projection here is that of the actual billiard double.

   lemma seam_localized_energy {Q : Triangle} {f : DoublePhase → ℂ}
       (hs : SeamCompatible Q f) (hm : Measurable f)
       (hd : ∀ v b, ContDiff ℝ ∞ (fun x => f ((x,v),b)))
       {C D : ℝ≥0}
       (hC : ∀ x v b, ‖fderiv ℝ (fun y => f ((y,v),b)) x‖ ≤ C)
       (hD : ∀ x v b, ‖fderiv ℝ (fderiv ℝ (fun y => f ((y,v),b))) x‖ ≤ D)
       (hf : MemLp f 2 (doubleMeasure Q))
       (E : Set ℂ) (hE : MeasurableSet E)
       (hX : ∀ᵐ z ∂doubleMeasure Q, z.1.1 ∉ E → xDerivative f z = 0) (j : ℤ) :
       let hx := xDerivative_memLp_of_gradient_bound Q hm
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.SeamCompatible, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.xDerivative, OAI.TriangularBilliards.xDerivative_memLp_of_gradient_bound

9. lemma OAI.TriangularBilliards.Triangle.clearance_sublevel line 214
10. lemma OAI.TriangularBilliards.Triangle.clearance_sublevel_measurable line 226
11. lemma OAI.TriangularBilliards.Triangle.clearance_area_bound line 230
12. def OAI.TriangularBilliards.unsafeSet line 245

    Source documentation

    The small-tip neighborhood on the actual oriented double.

    def unsafeSet (Q : Triangle) (R : ℝ) : Set DoublePhase :=
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase

13. lemma OAI.TriangularBilliards.unsafeSet_measurable line 248
14. lemma OAI.TriangularBilliards.unsafeSet_measure_bound line 251
15. lemma OAI.TriangularBilliards.Analysis.restrictL2_norm_of_bounded line 270
16. lemma OAI.TriangularBilliards.vertexCutoff_fderiv_zero_of_large line 293
17. lemma OAI.TriangularBilliards.supportedSmoothing_invariant_x_zero line 300
18. lemma OAI.TriangularBilliards.unsafeSet_real_measure_bound line 318
19. lemma OAI.TriangularBilliards.seam_tip_energy line 329

    Source documentation

    Generic localized gradient control on an actual smooth seam field, with its exact tip-neighborhood measure retained.

    lemma seam_tip_energy {Q : Triangle} {f : DoublePhase → ℂ}
        (hs : SeamCompatible Q f) (hm : Measurable f)
        (hd : ∀ v b, ContDiff ℝ ∞ (fun x => f ((x,v),b)))
        {C D : ℝ≥0}
        (hC : ∀ x v b, ‖fderiv ℝ (fun y => f ((y,v),b)) x‖ ≤ C)
        (hD : ∀ x v b, ‖fderiv ℝ (fderiv ℝ (fun y => f ((y,v),b))) x‖ ≤ D)
        (hf : MemLp f 2 (doubleMeasure Q)) (A : ℝ)
        (hX : ∀ᵐ z ∂doubleMeasure Q, z ∉ unsafeSet Q A → xDerivative f z = 0) (j : ℤ) :
        ∃ dx dy : Lp ℂ 2 (doubleMeasure Q),
          (geodesicHilbertFlow Q).HasGenerator ((angularCircleAction Q).projection j (hf.toLp _)) dx ∧
          (transverseHilbertFlow Q).HasGenerator ((angularCircleAction Q).projection j (hf.toLp _)) dy ∧
          ‖dx‖ ^ 2 ≤ 4 * (C : ℝ)^2 * (doubleMeasure Q (unsafeSet Q A)).toReal ∧
    …

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