OAI/Geometry/RCD/Sobolev/PoissonGradientBoundedness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_gradient_locally_bounded line 18

   Source documentation

   A uniformly small auxiliary radius gives qualitative boundedness on every interior ball. The later Bochner iteration removes its radius loss.

   theorem NoncollapsedRCD.poisson_gradient_locally_bounded {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
       {ker : ℝ → X → X → ℝ}
       (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
       (hg : HasCoordinateHeatBounds (hausdorff n X) ker)
       (p : X) (R : ℝ) (hR : 0 < R)
       (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ) (A : ℝ≥0)
       (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8*R)) f c)
       (hA : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8*R)), |SobolevSpace.toLp _ _ f x| ≤ A) :
       ∃ L : ℝ≥0, ∀ᵐ x ∂(hausdorff n X).restrict (ball p (4*R)),
         localGamma (hausdorff n X) hX.quadratic f f x ≤ (L:ℝ)^2 := by
   …

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