OAI/Geometry/RCD/Coordinates/HessianCoordinateForm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite bilinear representatives of the actual Hessian action

  1. theorem OAI.RegularPointCoordinates.gamma_bilinear_right_rep line 17
  2. def OAI.RegularPointCoordinates.hessianCoordinateForm line 49
  3. theorem OAI.RegularPointCoordinates.hessianCoordinateForm_rep line 58

    Source documentation

    Finite bilinear representatives preserve the full three-term action.

    theorem hessianCoordinateForm_rep (f : SobolevSpace μ hQ)
    (U G : Euclidean m →L[ℝ] SobolevSpace μ hQ)
    (B : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace μ hQ) (a b : Euclidean m) :
    localHessianAction μ hQ f (U a) (U b) (G a) (G b) (B a b) =ᵐ[μ]
      fun x => hessianCoordinateForm μ hQ f U G B x a b := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localHessianAction, OAI.RegularPointCoordinates.hessianCoordinateForm

  4. theorem OAI.RegularPointCoordinates.hessianCoordinateForm_symmetric line 72