OAI/Geometry/RCD/Heat/GaussianAnnularGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the gradient singularity at a separated annulus

  1. theorem OAI.RegularPointCoordinates.exists_annular_gaussian_gradient_bound line 12

    Source documentation

    After the ball-volume power is included, separation by half the working radius absorbs the full short-time gradient singularity.

    theorem exists_annular_gaussian_gradient_bound (n : ℕ) {D : ℝ} (hD : 0 < D) :
    ∃ Q : ℝ, 1 ≤ Q ∧ ∀ R t : ℝ, 0 < R → 0 < t → t ≤ R^2 →
      ((R/Real.sqrt t)^n/Real.sqrt t)*Real.exp (-(R/2)^2/(D*t)) ≤ Q/R := by
…