OAI/Geometry/RCD/Coordinates/RegularCoreWeakHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_core_shifted_hessian_weak line 21

   Source documentation

   The already constructed regular algebra and full Bochner measure turn scalar finite-dimensional BE into every shifted diagonal action. The scalar finite-dimensional Bochner inequality supplies the second-order bound.

   theorem NoncollapsedRCD.regular_core_shifted_hessian_weak {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n)
       (hscalar : ScalarDimensionalBochner (hausdorff n X) hX.quadratic K n)
       {V : Set X} (f g : compactLaplacianCore (hausdorff n X) hX.quadratic V)
       (p : X) {R : ℝ} (hR : 0<R) {S : Set X} (hS : IsCompact S) (hsub : S ⊆ ball p R)
       (df : SobolevSpace (hausdorff n X) hX.quadratic)
       (qf : Lp ℝ 2 (hausdorff n X))
       (hqf : IsWeakLaplacian (hausdorff n X) hX.quadratic f.val qf)
       (A : ℝ≥0)
       (hdf : ∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic df x|≤A)
       (hsf : qf =ᵐ[(hausdorff n X).restrict (ball p R)]
         SobolevSpace.toLp (hausdorff n X) hX.quadratic df) :
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.ScalarDimensionalBochner, OAI.RegularPointCoordinates.compactLaplacianCore, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp