LongAverageHeatBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The averaged kernel difference on every time above the ball scale

theorem OAI.RegularPointCoordinates.gaussian_denominator_mono line 15
theorem OAI.RegularPointCoordinates.inverse_volume_power line 23

theorem OAI.RegularPointCoordinates.exists_long_average_difference_bound line 36

Source documentation

The Gaussian gradient input controls long times; the ordinary Gaussian bound handles the finite transition interval just above r².

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

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