HeatKernelDifferenceInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local finite-difference consequence of the published heat gradient bound

Jiang--Li--Zhang (2016), Corollary 1.2, equation (1.4), bounds the minimal weak gradient of the kernel by a Gaussian. Local Sobolev-to-Lipschitz, Bishop--Gromov and kernel continuity give this finite-difference consequence when the displacement is at most the heat length. The Gaussian constant is not required to be sharp, and only times at most one are used. The bound is stated at every source pole, including poles in the singular mass support.

def OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds line 27
Source documentation
The localized Gaussian gradient estimate, integrated along a short path, in the only finite-difference form used by the application.
```
def HasGaussianHeatDifferenceBounds (μ : Measure X) (ker : ℝ → X → X → ℝ) : Prop :=
…
```