KernelHalfBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the earlier row in a half-time heat decomposition

theorem OAI.RegularPointCoordinates.kernel_half_uniform_bound line 20

Source documentation

Gaussian decay may be dropped for the earlier row; a single volume comparison transfers its normalization to the final heat scale.

theorem kernel_half_uniform_bound (hk : IsContinuousHeatKernel μ hQ ker)
    {C B : ℝ} (hC : 0 < C) (hB : 0 ≤ B)
    (hupper : ∀ t, 0 < t → ∀ x y, ker t x y ≤ C/μ.real (ball y (Real.sqrt t))*
      Real.exp (-dist x y^2/(5*t)+B*t))
    {t D : ℝ} (ht : 0 < t) (z : X)
    (hV : 0 < μ.real (ball z (Real.sqrt t)))
    (hVh : 0 < μ.real (ball z (Real.sqrt (t/2))))
    (hvol : μ.real (ball z (Real.sqrt t)) ≤ D*μ.real (ball z (Real.sqrt (t/2)))) :
    ∀ w, ker (t/2) z w ≤ C*D/μ.real (ball z (Real.sqrt t))*Real.exp (B*t) := by
…

Mentions: OAI.RegularPointCoordinates.IsContinuousHeatKernel