OAI/Geometry/RCD/Coordinates/RegularCoreHessianBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_core_directional_hessian line 20

   Source documentation

   A regular function and one regular direction have a full positive Bochner measure controlling their diagonal Hessian action. The measure and all Gram representatives are constructed from the RCD structure.

   theorem NoncollapsedRCD.regular_core_directional_hessian {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤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 dg : SobolevSpace (hausdorff n X) hX.quadratic)
       (qf qg : Lp ℝ 2 (hausdorff n X))
       (hqf : IsWeakLaplacian (hausdorff n X) hX.quadratic f.val qf)
       (hqg : IsWeakLaplacian (hausdorff n X) hX.quadratic g.val qg)
       (A B : ℝ≥0)
       (hdf : ∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic df x|≤A)
       (hdg : ∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic dg x|≤B)
       (hsf : qf =ᵐ[(hausdorff n X).restrict (ball p R)]
   …

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