LocalPoissonHessianPairing.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual local Poisson Hessian pairings on every interior ball

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_hessian_pairing line 19

Source documentation

Bounded local gradients and the Poisson equations construct the full integrated Hessian pairing, including a dense regular test core.

theorem NoncollapsedRCD.local_poisson_hessian_pairing {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
    (f a : SobolevSpace (hausdorff n X) hX.quadratic) (c d : ℝ)
    {p : X} {r t : ℝ} (hr : 0<r) (ht : t≤2*r)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8*r)) f c)
    (ha : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8*r)) a d)
    (L M : ℝ≥0)
    (hL : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8*r)),
      localGamma (hausdorff n X) hX.quadratic f f x ≤ (L:ℝ)^2)
    (hM : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8*r)),
      localGamma (hausdorff n X) hX.quadratic a a x ≤ (M:ℝ)^2) :
    Nonempty (LocalHessianPairing (hausdorff n X) hX.quadratic (ball p t) f a) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.LocalHessianPairing