HessianPotentialProduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Hessian product rule in its potential argument

theorem OAI.RegularPointCoordinates.localHessianAction_potential_product line 18

Source documentation

The Hessian of a product has the two expected gradient cross terms. Every entry is the actual three-term Sobolev action.

theorem localHessianAction_potential_product {Ω : Set X}
    (f g u v fu fv gu gv uv : SobolevSpace μ hQ)
    (A B C D E F : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x|≤A)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤B)
    (hfuB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ fu x|≤C)
    (hfvB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ fv x|≤D)
    (hguB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ gu x|≤E)
    (hgvB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ gv x|≤F)
    (hfu : SobolevSpace.toLp μ hQ fu =ᵐ[μ.restrict Ω] localGamma μ hQ f u)
    (hfv : SobolevSpace.toLp μ hQ fv =ᵐ[μ.restrict Ω] localGamma μ hQ f v)
    (hgu : SobolevSpace.toLp μ hQ gu =ᵐ[μ.restrict Ω] localGamma μ hQ g u)
…

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