KernelGaussianDifference.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The localized Gaussian heat difference estimate from the actual RCD flow

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.gaussianHeatDifferenceBounds_of_upper line 22

Source documentation

The finite-difference estimate uses only a coarse Gaussian upper bound, the proved reverse Poincaré inequality, and actual CD volume comparison.

theorem NoncollapsedRCD.gaussianHeatDifferenceBounds_of_upper {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [ProperSpace X] [(hausdorff n X).Regular]
    (hn : 2 ≤ n) {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    {C B : ℝ} (hC : 0 < C) (hB : 0 ≤ B)
    (hupper : ∀ t, 0 < t → ∀ x y,
      ker t x y ≤ C/(hausdorff n X).real (ball y (Real.sqrt t))*
        Real.exp (-dist x y^2/(5*t)+B*t)) :
    HasGaussianHeatDifferenceBounds (hausdorff n X) ker := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.gaussianHeatDifferenceBounds line 86
Source documentation
Compatibility with the published two-sided input.
```
theorem NoncollapsedRCD.gaussianHeatDifferenceBounds {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [ProperSpace X] [(hausdorff n X).Regular]
    (hn : 2 ≤ n) {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    (hg : HasGaussianHeatBounds (hausdorff n X) ker) :
    HasGaussianHeatDifferenceBounds (hausdorff n X) ker := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasGaussianHeatBounds, OAI.RegularPointCoordinates.HasGaussianHeatDifferenceBounds