GaussianScaleAbsorption.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform Gaussian bounds when heat time is shorter than a ball scale

theorem OAI.RegularPointCoordinates.exists_gaussian_polynomial_bound line 14

Source documentation

A fixed Gaussian absorbs every polynomial loss in the heat scale.

theorem exists_gaussian_polynomial_bound (n : ℕ) {c : ℝ} (hc : 0 < c) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ u : ℝ, 1 ≤ u → u ^ n * Real.exp (-c * u ^ 2) ≤ C := by
…

theorem OAI.RegularPointCoordinates.exists_gaussian_scale_absorption line 37

Source documentation

At distance at least one ball radius, a shorter heat scale has a uniform Gaussian envelope at that ball radius.

theorem exists_gaussian_scale_absorption (n : ℕ) {c : ℝ} (hc : 0 < c) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ u v : ℝ, 1 ≤ u → 1 ≤ v →
      u ^ n * Real.exp (-c * (u * v) ^ 2) ≤ C * Real.exp (-(c / 2) * v ^ 2) := by
…

theorem OAI.RegularPointCoordinates.exists_gaussian_short_time_bound line 59

Source documentation

The Gaussian at a time below the ball scale is bounded by a fixed multiple of the Gaussian at that ball scale, away from the ball.

theorem exists_gaussian_short_time_bound (n : ℕ) {D : ℝ} (hD : 0 < D) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ r t d : ℝ, 0 < r → 0 < t → t ≤ r ^ 2 → r ≤ d →
      (Real.sqrt t)⁻¹ ^ n * Real.exp (-d ^ 2 / (D * t)) ≤
        C * r⁻¹ ^ n * Real.exp (-d ^ 2 / (2 * D * r ^ 2)) := by
…