ShortAverageGaussian.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian bounds for an averaged kernel below the averaging scale

theorem OAI.RegularPointCoordinates.kernelAverage_le_uniform line 20

Source documentation

A pointwise bound on a finite averaging set is preserved by averaging.

theorem kernelAverage_le_uniform {t : ℝ} (ht : 0 < t) (s : Set X)
    (hs : MeasurableSet s) (hfinite : μ s ≠ ∞) (hvol : 0 < μ.real s) (z : X) {B : ℝ}
    (hbound : ∀ y ∈ s, ker t y z ≤ B) : kernelAverage μ ker t s z ≤ B := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage

theorem OAI.RegularPointCoordinates.exists_short_average_gaussian line 37

Source documentation

The short-time averaged kernel has Gaussian decay at the averaging radius. Its constants depend only on the displayed geometric bounds.

theorem exists_short_average_gaussian (n : ℕ) {A V Cg D : ℝ}
    (hA : 0 ≤ A) (hV : 0 < V) (hCg : 0 ≤ Cg) (hD : 0 < D) :
    ∃ C : ℝ, 0 < C ∧ ∀ (r t : ℝ) (x q z : X),
      0 < r → 0 < t → t ≤ r ^ 2 → μ (ball q r) ≠ ∞ →
      V * r ^ n ≤ μ.real (ball q r) → dist x q ≤ A * r →
      (∀ y ∈ ball q r, ker t y z ≤
        Cg * (Real.sqrt t)⁻¹ ^ n * Real.exp (-(dist y z) ^ 2 / (D * t))) →
      kernelAverage μ ker t (ball q r) z ≤
        C * r⁻¹ ^ n * Real.exp (-(dist x z) ^ 2 / (8 * D * r ^ 2)) := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage