OAI/Geometry/RCD/Sobolev/CompactPoissonHessian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_test_gradient line 18
2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_poisson_hessian_pairing line 36

   Source documentation

   All Sobolev representatives in the Koszul identity are constructed from the RCD energy-density theorem and a proved dense compact core.

   theorem NoncollapsedRCD.compact_poisson_hessian_pairing {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n) (p : X)
       {Ω : Set X} (hΩ : IsOpen Ω)
       (f a : SobolevSpace (hausdorff n X) hX.quadratic)
       {v w : X → ℝ} {L M : ℝ≥0}
       (hv : LipschitzWith L v) (hvc : HasCompactSupport v)
       (hfr : SobolevSpace.toLp (hausdorff n X) hX.quadratic f =ᵐ[hausdorff n X] v)
       (hw : LipschitzWith M w) (hwc : HasCompactSupport w)
       (har : SobolevSpace.toLp (hausdorff n X) hX.quadratic a =ᵐ[hausdorff n X] w)
       (df da : Lp ℝ 2 (hausdorff n X))
       (hdf : IsWeakLaplacian (hausdorff n X) hX.quadratic f df)
       (hda : IsWeakLaplacian (hausdorff n X) hX.quadratic a da)
   …

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