RegularHessianCore.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Replacing the local Hessian core without changing its functional

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.hessian_pairing_regular_core line 19

Source documentation

For compact Poisson functions, the actual dense regular core can be installed while preserving the given Hessian functional and mixed Gram representative. This makes bounds independent of a prior core choice.

theorem NoncollapsedRCD.hessian_pairing_regular_core {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n) (p : X)
    {Ω : Set X} (hΩ : IsOpen Ω)
    (f a : compactLaplacianCore (hausdorff n X) hX.quadratic univ)
    (c d : ℝ)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic Ω f.val c)
    (ha : IsConstantLaplacianOn (hausdorff n X) hX.quadratic Ω a.val d)
    (G : LocalHessianPairing (hausdorff n X) hX.quadratic Ω f.val a.val) :
    ∃ H : LocalHessianPairing (hausdorff n X) hX.quadratic Ω f.val a.val,
      H.core=regularDirichletCore (hausdorff n X) hX.quadratic Ω ∧
      H.mixed=G.mixed ∧ H.hessian=G.hessian := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.regularDirichletCore