AnnularKernelDifference.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform heat-kernel differences across a separated annulus

theorem OAI.RegularPointCoordinates.inverse_volume_coefficient line 16

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.annular_kernel_difference line 42

Source documentation

Positive separation from a source annulus absorbs all small-time losses in the Gaussian difference estimate. The constant precedes both the center and the working radius.

theorem NoncollapsedRCD.annular_kernel_difference {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) :
    ∃ J : ℝ, 0 < J ∧ ∀ (p : X) (R t : ℝ), 0 < R → -1 ≤ K*R^2 →
      0 < t → t ≤ 1 → t ≤ R^2 → ∀ x y z : X,
      dist x p ≤ R/2 → R ≤ dist z p → dist z p ≤ 2*R → dist x y ≤ Real.sqrt t →
      |ker t x z-ker t y z| ≤
        J/(R*(hausdorff n X).real (ball p R))*dist x y := by
…

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