OAI/Geometry/RCD/Sobolev/LocalPoissonShiftedHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_shifted_hessian_of_scalar line 22

   Source documentation

   Actual local Poisson extensions and the prescribed full measure inherit the sharp shifted estimate. The scalar finite-dimensional Bochner inequality is the only additional analytic premise.

   theorem NoncollapsedRCD.local_poisson_shifted_hessian_of_scalar {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n)
       (hscalar : ScalarDimensionalBochner (hausdorff n X) hX.quadratic K n)
       (f a : SobolevSpace (hausdorff n X) hX.quadratic) (c d κ : ℝ) (hK : -κ≤K)
       {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)
   …

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