LongAverageGaussian.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Averaging a Gaussian above the averaging-ball scale

theorem OAI.RegularPointCoordinates.kernelAverage_gaussian_above_scale line 20

Source documentation

When the heat length exceeds the averaging radius, a Gaussian at any averaging point gives a Gaussian at the fixed reference center.

theorem kernelAverage_gaussian_above_scale {r t A B D : ℝ}
    (hr : 0 < r) (ht : 0 < t) (hA : 0 ≤ A) (hB : 0 ≤ B) (hD : 0 < D)
    (hrtime : r ^ 2 ≤ t) (x q z : X)
    (hfinite : μ (ball q r) ≠ ∞) (hvol : 0 < μ.real (ball q r))
    (hcenter : dist x q ≤ A * r)
    (hbound : ∀ y ∈ ball q r,
      ker t y z ≤ B * Real.exp (-(dist y z) ^ 2 / (D * t))) :
    kernelAverage μ ker t (ball q r) z ≤
      (B * Real.exp ((A + 1) ^ 2 / D)) *
        Real.exp (-(dist x z) ^ 2 / (2 * D * t)) := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage