OAI/Dynamics/TriangleBilliards/SeamEnergy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.seam_CR_norms line 28

   Source documentation

   Global equal Cauchy--Riemann norms on the genuine smooth seam core. The integration-by-parts step is supplied by the actual measure-preserving geodesic/transverse generators and the proved pointwise Schwarz identity.

   lemma seam_CR_norms {Q : Triangle} {f : DoublePhase → ℂ}
       (hs : SeamCompatible Q f)
       (hd : ∀ v b, ContDiff ℝ ∞ (fun x => f ((x,v),b)))
       {C Cx Cy : ℝ≥0}
       (hC : ∀ x v b, ‖fderiv ℝ (fun y => f ((y,v),b)) x‖ ≤ C)
       (hCx : ∀ x v b, ‖fderiv ℝ (fun y => xDerivative f ((y,v),b)) x‖ ≤ Cx)
       (hCy : ∀ x v b, ‖fderiv ℝ (fun y => yDerivative f ((y,v),b)) x‖ ≤ Cy)
       (hf : MemLp f 2 (doubleMeasure Q))
       (hxf : MemLp (xDerivative f) 2 (doubleMeasure Q))
       (hyf : MemLp (yDerivative f) 2 (doubleMeasure Q))
       (hxyf : MemLp (xDerivative (yDerivative f)) 2 (doubleMeasure Q)) :
       ‖hxf.toLp (xDerivative f) + Complex.I • hyf.toLp (yDerivative f)‖ =
   …

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

2. lemma OAI.TriangularBilliards.raw_eq_one_of_norm_le line 62
3. lemma OAI.TriangularBilliards.raw_eq_zero_of_one_le_norm line 67
4. def OAI.TriangularBilliards.vertexCutoffFactor line 75

   Source documentation

   An explicit vertex cutoff, zero up to radius R and one outside radius 2R. Its transition annuli are those used in the localized energy bound.

   def vertexCutoffFactor (Q : Triangle) (R : ℝ) (i : Fin 3) (x : ℂ) : ℝ :=
   …

   Mentions: OAI.TriangularBilliards.Triangle

5. def OAI.TriangularBilliards.vertexCutoff line 78
6. lemma OAI.TriangularBilliards.vertexCutoffFactor_mem_Icc line 81
7. lemma OAI.TriangularBilliards.vertexCutoff_mem_Icc line 85
8. lemma OAI.TriangularBilliards.vertexCutoffFactor_zero line 92
9. lemma OAI.TriangularBilliards.vertexCutoffFactor_one line 101
10. lemma OAI.TriangularBilliards.vertexCutoff_zero line 110
11. lemma OAI.TriangularBilliards.vertexCutoff_one line 121
12. lemma OAI.TriangularBilliards.vertexCutoffFactor_contDiff line 130
13. lemma OAI.TriangularBilliards.vertexCutoff_contDiff line 136
14. lemma OAI.TriangularBilliards.reflected_vertex_dist line 139
15. lemma OAI.TriangularBilliards.side_opposite_dist_lower line 152
16. lemma OAI.TriangularBilliards.vertexCutoff_seam_germ line 163

    Source documentation

    Scale condition only on geometric constants of the fixed nondegenerate triangle. It imposes no Diophantine angle condition.

    lemma vertexCutoff_seam_germ (Q : Triangle) {R : ℝ} (hR : 0 < R)
        (hsmall : 2 * R * Q.coordinateBound < 1) (i : Fin 3) {x : ℂ} (hx : x ∈ Q.side i) :
        ∀ᶠ y in 𝓝 x, vertexCutoff Q R (wallReflection Q i y) = vertexCutoff Q R y := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.vertexCutoff, OAI.TriangularBilliards.wallReflection

17. def OAI.TriangularBilliards.supportedSmoothing line 198

    Source documentation

    The supported smoothing used for bounded-mode regularity.

    def supportedSmoothing (Q : Triangle) (ε R : ℝ) (f : DoublePhase → ℂ) : DoublePhase → ℂ :=
    …

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

18. lemma OAI.TriangularBilliards.supportedSmoothing_zero line 201
19. lemma OAI.TriangularBilliards.supportedSmoothing_seam line 206
20. lemma OAI.TriangularBilliards.bounded_spatialSlice_integrable line 226
21. lemma OAI.TriangularBilliards.supportedSmoothing_contDiff line 234
22. lemma OAI.TriangularBilliards.supportedSmoothing_stronglyMeasurable line 242
23. lemma OAI.TriangularBilliards.directS_norm_bound line 248
24. lemma OAI.TriangularBilliards.reflectedSmoothing_norm_bound line 261
25. lemma OAI.TriangularBilliards.supportedSmoothing_norm_bound line 275