ShortAverageHeatBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The published Gaussian estimate gives the actual short-time average bound

theorem OAI.RegularPointCoordinates.exists_cutoff_short_average_bound line 22

Source documentation

Volume lower bounds are required only at the averaging ball and at source points where the cutoff is nonzero. The constant precedes all radii.

theorem exists_cutoff_short_average_bound (hg : HasCoordinateHeatBounds μ ker)
    (n : ℕ) {A V : ℝ} (hA : 0 ≤ A) (hV : 0 < V) :
    ∃ C : ℝ, 0 < C ∧ ∀ (χ : X → ℝ), (∀ z, 0 ≤ χ z ∧ χ z ≤ 1) →
      ∀ (r t : ℝ) (x q : X), 0 < r → r ≤ 1 → 0 < t → t ≤ r ^ 2 →
      μ (ball q r) ≠ ∞ → V * r ^ n ≤ μ.real (ball q r) → dist x q ≤ A * r →
      (∀ z, χ z ≠ 0 → V * (Real.sqrt t) ^ n ≤ μ.real (ball z (Real.sqrt t))) →
      ∀ z, χ z * kernelAverage μ ker t (ball q r) z ≤
        C * r⁻¹ ^ n * Real.exp (-(dist x z) ^ 2 / (36 * r ^ 2)) := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.kernelAverage