OAI/Geometry/RCD/Sobolev/LocalPoissonMeasureLaplacian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_measure_laplacian line 16
2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_measure_laplacian_of_curvature line 58

   Source documentation

   At bounded rescaled curvature the cutoff is constructed from the RCD heat resolvent; only local bounds on the Poisson function are needed.

   theorem NoncollapsedRCD.local_poisson_measure_laplacian_of_curvature {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
       {Ω : Set X} (hΩ : MeasurableSet Ω)
       (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ)
       (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic Ω f c)
       (A L : ℝ≥0) (hA : ∀ᵐ x ∂(hausdorff n X).restrict Ω,
         |SobolevSpace.toLp (hausdorff n X) hX.quadratic f x| ≤ A)
       (hL : ∀ᵐ x ∂(hausdorff n X).restrict Ω,
         localGamma (hausdorff n X) hX.quadratic f f x ≤ (L : ℝ) ^ 2)
       {p : X} {R : ℝ} (hR : 0 < R) (hsub : closedBall p (3 * R) ⊆ Ω)
       (hcurv : -1 ≤ K * (3 * R / 2) ^ 2) (κ : ℝ) (hK : -κ ≤ K) :
       ∃ (G : SobolevSpace (hausdorff n X) hX.quadratic) (σ : Measure X),
   …

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