PoissonInteriorSmallRadii.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior Poisson estimates for locally bounded solutions at small radii

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_gradient_at_small_radii line 20

Source documentation

The half-ball form of the Poisson estimate for radii at most one. The amplitude hypothesis is local; global truncation is internal.

theorem NoncollapsedRCD.poisson_gradient_at_small_radii {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) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (r : ℝ), 0 < r → r ≤ 1 → -1 ≤ K*r^2 →
      ∀ (f : SobolevSpace (hausdorff n X) hX.quadratic) (c A : ℝ), 0 ≤ A →
      IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8*r)) f c →
      (∀ᵐ x ∂(hausdorff n X).restrict (ball p (8*r)), |SobolevSpace.toLp _ _ f x| ≤ A) →
      ∀ᵐ x ∂(hausdorff n X).restrict (ball p (4*r)),
        localGamma (hausdorff n X) hX.quadratic f f x ≤ (C*(A/r+|c| *r))^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