OAI/Geometry/RCD/Sobolev/HessianPotentialSquare.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.localHessianAction_potential_square line 17

   Source documentation

   The quadratic perturbation has the expected rank-one second derivative.

   theorem localHessianAction_potential_square {Ω : Set X}
       (g u v gu gv uv : SobolevSpace μ hQ) (B E F : ℝ≥0)
       (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤B)
       (hguB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ gu x|≤E)
       (hgvB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ gv x|≤F)
       (hgu : SobolevSpace.toLp μ hQ gu =ᵐ[μ.restrict Ω] localGamma μ hQ g u)
       (hgv : SobolevSpace.toLp μ hQ gv =ᵐ[μ.restrict Ω] localGamma μ hQ g v) :
       localHessianAction μ hQ (SobolevSpace.product μ hQ g g B B) u v
         ((2 : ℝ) • SobolevSpace.product μ hQ g gu B E)
         ((2 : ℝ) • SobolevSpace.product μ hQ g gv B F) uv =ᵐ[μ.restrict Ω] fun x =>
         2*SobolevSpace.toLp μ hQ g x*localHessianAction μ hQ g u v gu gv uv x+
           2*localGamma μ hQ g u x*localGamma μ hQ g v x := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localHessianAction, OAI.RegularPointCoordinates.SobolevSpace.product