CutoffGaussianBlock.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One uniform Gaussian majorant for all cutoff kernels in a time block

theorem OAI.RegularPointCoordinates.cutoff_gaussian_block_bound line 19

Source documentation

The published Gaussian bound gives one coefficient before the scale, pole and cutoff are chosen. Volume control is needed only on its support.

theorem cutoff_gaussian_block_bound (μ : Measure X) {ker : ℝ → X → X → ℝ}
    (hg : HasCoordinateHeatBounds μ ker) (n : ℕ) {V : ℝ} (hV : 0 < V) :
    ∃ C D : ℝ, 0 < C ∧ 0 < D ∧ ∀ r t : ℝ, 0 < r → r ≤ 1 → 0 < t → t ≤ r ^ 2 →
      ∀ (p : X) (χ : X → ℝ), (∀ z, 0 ≤ χ z ∧ χ z ≤ 1) →
      (∀ z, χ z ≠ 0 → V * r ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ q : ℝ, 0 ≤ q → ∀ z : X, q * r ≤ dist p z →
        χ z * ker t p z ≤ (C / r ^ n) * Real.exp (-q ^ 2 / D) := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds