OAI/Dynamics/TriangleBilliards/ClearanceSmoothing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.smoothing_direction_pairing line 44

   Source documentation

   Local transport commutation with a nonzero generator, obtained from unitary skew-adjointness and actual kernel adjoint identities.

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

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

2. lemma OAI.TriangularBilliards.smoothing_direction_local line 66
3. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_zero_near_tips line 140
4. lemma OAI.TriangularBilliards.smoothing_direction_of_supported line 158

   Source documentation

   Global commutation for inputs and their generators with a genuine vertex margin. The local identity extends by zero, not by a boundary claim.

   lemma smoothing_direction_of_supported (Q : Triangle) {ε R A : ℝ}
       (hε : 0 < ε) (hR : Q.safetyFactor * ε < R)
       (hsmall : 2 * R * Q.coordinateBound < 1) (hA : 2 * R + 2 * ε ≤ A)
       {f p : DoublePhase → ℂ} (hfm : StronglyMeasurable f) (hpm : StronglyMeasurable p)
       (hf : MemLp f 2 (doubleMeasure Q)) (hp : MemLp p 2 (doubleMeasure Q))
       (hfp : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) (hp.toLp p))
       {H J : ℝ} (hH : ∀ z, ‖f z‖ ≤ H) (hJ : ∀ z, ‖p z‖ ≤ J)
       (hfs : SpatiallyZero Q A f) (hps : SpatiallyZero Q A p) :
       (fun z => reflectedSmoothingGradient Q ε f z (z.1.2 : ℂ)) =ᵐ[doubleMeasure Q]
         reflectedSmoothing Q ε p := by
   …

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

5. lemma OAI.TriangularBilliards.supportedSmoothing_generator_commutes line 176
6. lemma OAI.TriangularBilliards.transverseVelocity_stronglyMeasurable line 205
7. def OAI.TriangularBilliards.reflectedSmoothingY line 213
8. lemma OAI.TriangularBilliards.reflectedSmoothingY_memLp line 216
9. lemma OAI.TriangularBilliards.reflectedSmoothingY_adjoint line 223
10. lemma OAI.TriangularBilliards.supportedSmoothing_yDerivative_eq_of_supported line 232
11. lemma OAI.TriangularBilliards.supportedSmoothing_transverse_generator line 247
12. lemma OAI.TriangularBilliards.seam_mixed_generators line 267
13. lemma OAI.TriangularBilliards.clearance_smoothing_pairing line 297

    Source documentation

    The segment pairing is obtained on the actual compactly supported mollifier domain. No commutation on a rough tail is asserted.

    lemma clearance_smoothing_pairing (Q : Triangle) {ε R A : ℝ}
        (hε : 0 < ε) (hR : Q.safetyFactor * ε < R)
        (hsmall : 2 * R * Q.coordinateBound < 1) (hA : 2 * R + 2 * ε ≤ A)
        {f p : DoublePhase → ℂ} (hfm : StronglyMeasurable f) (hpm : StronglyMeasurable p)
        (hf : MemLp f 2 (doubleMeasure Q)) (hp : MemLp p 2 (doubleMeasure Q))
        (hfp : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) (hp.toLp p))
        {H J : ℝ} (hH : ∀ z, ‖f z‖ ≤ H) (hJ : ∀ z, ‖p z‖ ≤ J)
        (hfs : SpatiallyZero Q A f) (hps : SpatiallyZero Q A p)
        {U B : DoubleL2 Q} (hUB : (geodesicHilbertFlow Q).HasGenerator U B) :
        inner ℂ B ((reflectedSmoothingY_memLp Q hε hfm hf).toLp _) =
          inner ℂ ((reflectedSmoothingY_memLp Q hε (Lp.stronglyMeasurable U) (Lp.memLp U)).toLp _) (hp.toLp p) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.SpatiallyZero, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.reflectedSmoothingY_memLp