OAI/Geometry/RCD/Sobolev/HessianActionProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Hessian action obeys the product rule in a gradient direction

  1. theorem OAI.RegularPointCoordinates.localHessianAction_product line 18

    Source documentation

    The extra first-order terms cancel in the three-term Hessian formula. All products are genuine Sobolev products of bounded representatives.

    theorem localHessianAction_product {Ω : Set X}
    (f a u v fa fu fv au av : SobolevSpace μ hQ)
    (A B C D E F : ℝ≥0)
    (hu : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ u x|≤A)
    (hv : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ v x|≤B)
    (hfuB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ fu x|≤C)
    (hfvB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ fv x|≤D)
    (hauB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ au x|≤E)
    (havB : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ av x|≤F)
    (hfu : SobolevSpace.toLp μ hQ fu =ᵐ[μ.restrict Ω] localGamma μ hQ f u)
    (hfv : SobolevSpace.toLp μ hQ fv =ᵐ[μ.restrict Ω] localGamma μ hQ f v)
    (hau : SobolevSpace.toLp μ hQ au =ᵐ[μ.restrict Ω] localGamma μ hQ a u)
…

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