HessianActionLocality.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local representative independence of the Hessian action

theorem OAI.RegularPointCoordinates.localHessianAction_congr line 16

theorem OAI.RegularPointCoordinates.localHessianAction_square_self line 33

Source documentation

The square identity uses any local Gram representatives, including the entries of the common finite-family Bochner construction.

theorem localHessianAction_square_self {Ω : Set X}
    (g G P : SobolevSpace μ hQ) (A B : ℝ≥0)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x|≤A)
    (hG : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ G x|≤B)
    (hGr : SobolevSpace.toLp μ hQ G =ᵐ[μ.restrict Ω] localGamma μ hQ g g)
    (hPr : SobolevSpace.toLp μ hQ P =ᵐ[μ.restrict Ω]
      localGamma μ hQ (SobolevSpace.product μ hQ g g A A) g) :
    localHessianAction μ hQ (SobolevSpace.product μ hQ g g A A) g g P P G
      =ᵐ[μ.restrict Ω] fun x =>
        2*SobolevSpace.toLp μ hQ g x*localHessianAction μ hQ g g g G G G x+
          2*(localGamma μ hQ g g x)^2 := by
…

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