OAI/Dynamics/TriangleBilliards/SmoothingGenerators.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.supportedSmoothing_xDerivative line 30
2. lemma OAI.TriangularBilliards.supportedSmoothing_fderiv_bound line 37
3. lemma OAI.TriangularBilliards.supportedSmoothing_memLp line 52
4. lemma OAI.TriangularBilliards.supportedSmoothing_xDerivative_memLp line 59
5. lemma OAI.TriangularBilliards.supportedSmoothing_generator line 78
6. lemma OAI.TriangularBilliards.supportedSmoothing_eq_of_supported line 97
7. lemma OAI.TriangularBilliards.supportedSmoothing_derivative_eq_of_supported line 107
8. lemma OAI.TriangularBilliards.reflectedSmoothing_direction_memLp line 122
9. lemma OAI.TriangularBilliards.reflectedSmoothing_supported_generator line 130
10. lemma OAI.TriangularBilliards.integral_pairing_toLp line 152
11. lemma OAI.TriangularBilliards.invariant_smoothing_direction_pairing_zero line 162

    Source documentation

    Exact local kernel-transport commutation for a bounded invariant field, expressed against arbitrary bounded fields with a sufficient vertex margin.

    lemma invariant_smoothing_direction_pairing_zero (Q : Triangle) {ε R A : ℝ}
        (hε : 0 < ε) (hR : Q.safetyFactor * ε < R)
        (hsmall : 2 * R * Q.coordinateBound < 1) (hA : 2 * R + ε ≤ A)
        {f g : DoublePhase → ℂ} (hfm : StronglyMeasurable f) (hgm : StronglyMeasurable g)
        (hf : MemLp f 2 (doubleMeasure Q)) (hg : MemLp g 2 (doubleMeasure Q))
        (hfi : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) 0)
        {H : ℝ} (hH : ∀ z, ‖g z‖ ≤ H) (hgs : SpatiallyZero Q A g) :
        (∫ z, reflectedSmoothingGradient Q ε f z (z.1.2 : ℂ) * conj (g z) ∂doubleMeasure Q) = 0 := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.SpatiallyZero, OAI.TriangularBilliards.reflectedSmoothingGradient

12. lemma OAI.TriangularBilliards.reflectedSmoothing_direction_norm_bound line 185
13. lemma OAI.TriangularBilliards.reflectedSmoothing_direction_stronglyMeasurable line 193
14. lemma OAI.TriangularBilliards.invariant_smoothing_direction_zero line 203

    Source documentation

    The actual local X-commutation equation for a bounded invariant field. No local distributional transport statement is used as an extra hypothesis.

    lemma invariant_smoothing_direction_zero (Q : Triangle) {ε R A : ℝ}
        (hε : 0 < ε) (hR : Q.safetyFactor * ε < R)
        (hsmall : 2 * R * Q.coordinateBound < 1) (hA : 2 * R + ε ≤ A)
        {f : DoublePhase → ℂ} (hfm : StronglyMeasurable f)
        (hf : MemLp f 2 (doubleMeasure Q))
        (hfi : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) 0)
        {H : ℝ} (hH : ∀ z, ‖f z‖ ≤ H) :
        ∀ᵐ z ∂doubleMeasure Q, A ≤ Q.clearance z.1.1 →
          reflectedSmoothingGradient Q ε f z (z.1.2 : ℂ) = 0 := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.reflectedSmoothingGradient

15. lemma OAI.TriangularBilliards.Analysis.pairing_add_sum_symmetric line 258
16. lemma OAI.TriangularBilliards.spatialKernel_stronglyMeasurable line 284
17. lemma OAI.TriangularBilliards.directS_adjoint line 289
18. lemma OAI.TriangularBilliards.reflectedS_adjoint line 301
19. lemma OAI.TriangularBilliards.directS_memLp line 315
20. lemma OAI.TriangularBilliards.reflectedS_memLp line 320
21. lemma OAI.TriangularBilliards.reflectedSmoothing_adjoint line 325