OAI/Geometry/RCD/Heat/SeparatedGaussianBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform Gaussian bounds at a fixed positive separation

  1. theorem OAI.RegularPointCoordinates.exists_separated_gaussian_bound line 12

    Source documentation

    A positive separation absorbs every inverse power of the heat scale, uniformly over all positive scales.

    theorem exists_separated_gaussian_bound (n : ℕ) {δ D : ℝ} (hδ : 0 < δ) (hD : 0 < D) :
    ∃ C : ℝ, 0 < C ∧ ∀ s d : ℝ, 0 < s → δ ≤ d →
      s⁻¹ ^ n * Real.exp (-d ^ 2 / (D * s ^ 2)) ≤ C := by
…