OAI/Dynamics/TriangleBilliards/DerivativeAdjoints.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.directionalKernel_stronglyMeasurable line 30
2. lemma OAI.TriangularBilliards.directionalKernel_bounded line 39
3. lemma OAI.TriangularBilliards.directDirectional_adjoint line 51
4. lemma OAI.TriangularBilliards.reflectedDirectional_adjoint line 64
5. lemma OAI.TriangularBilliards.directGradS_apply_ae line 82
6. lemma OAI.TriangularBilliards.reflectedGradS_apply_ae line 90
7. lemma OAI.TriangularBilliards.Analysis.gradientApply_memLp line 105
8. lemma OAI.TriangularBilliards.Analysis.pairing_add_sum line 115
9. lemma OAI.TriangularBilliards.directGradS_memLp line 142
10. lemma OAI.TriangularBilliards.reflectedGradS_memLp line 148
11. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_adjoint line 157

    Source documentation

    Adjoint identity for the actual unfolded gradient kernel on the complete L² space. It holds in particular after pairing against a supported field, without taking any derivatives of that field.

    lemma reflectedSmoothingGradient_adjoint (Q : Triangle) {ε : ℝ} (hε : 0 < ε)
        {V : DirectionParity → ℂ} (hVm : StronglyMeasurable V) (hV : ∀ c, ‖V c‖ ≤ 1)
        (hVR : ∀ i c, reflect (Q.tangent i) (V c) = V (directionParityReflection Q i c))
        {f g : DoublePhase → ℂ} (hfm : StronglyMeasurable f) (hgm : StronglyMeasurable g)
        (hf : MemLp f 2 (doubleMeasure Q)) (hg : MemLp g 2 (doubleMeasure Q)) :
        (∫ z, reflectedSmoothingGradient Q ε f z (V (z.1.2,z.2)) * conj (g z) ∂doubleMeasure Q) =
          -(∫ z, f z * conj (reflectedSmoothingGradient Q ε g z (V (z.1.2,z.2))) ∂doubleMeasure Q) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DirectionParity, OAI.TriangularBilliards.reflect, OAI.TriangularBilliards.directionParityReflection, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.reflectedSmoothingGradient

12. lemma OAI.TriangularBilliards.directS_hasFDerivAt line 202
13. lemma OAI.TriangularBilliards.kernel_wall_derivative_transfer line 209
14. lemma OAI.TriangularBilliards.reflectedS_hasFDerivAt line 215
15. lemma OAI.TriangularBilliards.reflectedSmoothing_hasFDerivAt line 250
16. lemma OAI.TriangularBilliards.vertexCutoffFactor_derivative_bound line 266
17. lemma OAI.TriangularBilliards.vertexCutoff_derivative_bound line 287
18. lemma OAI.TriangularBilliards.exists_vertexCutoff_derivative_bound line 309
19. def OAI.TriangularBilliards.supportedSmoothingGradient line 319
20. lemma OAI.TriangularBilliards.supportedSmoothing_hasFDerivAt line 324
21. lemma OAI.TriangularBilliards.supportedSmoothingGradient_stronglyMeasurable line 333
22. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_norm_bound line 345
23. lemma OAI.TriangularBilliards.supportedSmoothingGradient_norm_bound line 352