PoissonGradientBochner.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Scale-uniform Poisson gradient control from the energy subsolution

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_gradient_bochner line 21

Source documentation

The Bochner mean bound removes the small-radius restriction from the heat construction of a locally bounded gradient.

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