OAI/Geometry/RCD/Sobolev/HessianCommutatorEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.local_hessian_commutator_energy line 17

   Source documentation

   The shifted Hessian of f and the ordinary Hessian of v control the commutator error. The coordinate Hessian cancels in the exact identity.

   theorem local_hessian_commutator_energy {Ω : Set X} {f v u : SobolevSpace μ hQ}
       (Gfv : LocalHessianPairing μ hQ Ω f v)
       (Gvf : LocalHessianPairing μ hQ Ω v f)
       (Gfu : LocalHessianPairing μ hQ Ω f u)
       (Gvu : LocalHessianPairing μ hQ Ω v u)
       (hF : MemLp (fun x => localHessianAction μ hQ f v u Gfv.mixed Gfu.mixed Gvu.mixed x -
         localGamma μ hQ v u x) 2 (μ.restrict Ω))
       (hV : MemLp (localHessianAction μ hQ v f u Gvf.mixed Gvu.mixed Gfu.mixed) 2 (μ.restrict Ω))
       {D E : ℝ}
       (hDF : (∫ x in Ω, (localHessianAction μ hQ f v u Gfv.mixed Gfu.mixed Gvu.mixed x -
         localGamma μ hQ v u x) ^ 2 ∂μ) ≤ D)
       (hDV : (∫ x in Ω, (localHessianAction μ hQ v f u Gvf.mixed Gvu.mixed Gfu.mixed x) ^ 2 ∂μ) ≤ E) :
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.localHessianAction, OAI.RegularPointCoordinates.localGamma