LocalHessianAction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The local Hessian action and the exact two-center commutator identity

Gigli (2018), Theorem 3.3.8, equation (3.3.19), identifies the three-term gradient formula with Hessian evaluation on gradient vector fields. The cancellation below only uses the actual local Sobolev pairings.

def OAI.RegularPointCoordinates.localHessianAction line 23
Source documentation
The three-term gradient formula for Hess f(grad v, grad u), when the three local gradient pairings have Sobolev representatives.
```
def localHessianAction (f v u fv fu vu : SobolevSpace μ hQ) : X → ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.local_hessian_commutator line 29

Source documentation

The second derivatives of the coordinate function cancel exactly. No differentiability of a pointwise metric is used.

theorem local_hessian_commutator {Ω : 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) :
    (fun x => localGamma μ hQ v Gfu.mixed x - localGamma μ hQ f Gvu.mixed x) =ᵐ[μ.restrict Ω]
      fun x => localHessianAction μ hQ f v u Gfv.mixed Gfu.mixed Gvu.mixed x -
        localHessianAction μ hQ v f u Gvf.mixed Gvu.mixed Gfu.mixed x := by
…

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