OAI/Geometry/RCD/Sobolev/HessianActionIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrability and the exact integral of the Hessian action

  1. theorem OAI.RegularPointCoordinates.localHessianAction_integrable line 16
  2. theorem OAI.RegularPointCoordinates.integral_localHessianAction line 23
  3. theorem OAI.RegularPointCoordinates.LocalHessianPairing.integral_action_core line 37

    Source documentation

    The pointwise three-term action agrees with the continuous Hessian functional on the constructed dense test core.

    theorem LocalHessianPairing.integral_action_core {Ω : Set X} {f a : SobolevSpace μ hQ}
    (G : LocalHessianPairing μ hQ Ω f a) (φ : G.core) :
    (∫ x, localHessianAction μ hQ f a φ.val.val G.mixed
      (G.gammaF φ).val (G.gammaA φ).val x ∂μ) = G.hessian φ.val := by
…

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