SmallScalePoissonGradient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small-scale interior Poisson gradient estimate from the heat equation

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.small_scale_poisson_gradient line 22

Source documentation

A quantitative interior gradient estimate, with both cutoffs constructed from the RCD condition and no gradient assumption on the solution.

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