OAI/Geometry/RCD/Heat/AveragedKernelDifference.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.kernelAverage_difference_le line 18

   Source documentation

   Averaging preserves a uniform bound on the pointwise kernel difference.

   theorem kernelAverage_difference_le (μ : Measure X) (ker : ℝ → X → X → ℝ)
       {s : Set X} (hfinite : μ s ≠ ∞) (hvol : 0 < μ.real s)
       (t : ℝ) (x z : X) (hf : IntegrableOn (fun y => ker t y z) s μ)
       {B : ℝ} (hbound : ∀ᵐ y ∂μ.restrict s, |ker t y z - ker t x z| ≤ B) :
       |kernelAverage μ ker t s z - ker t x z| ≤ B := by
   …

   Mentions: OAI.RegularPointCoordinates.kernelAverage

2. theorem OAI.RegularPointCoordinates.averaged_kernel_difference_bound line 48

   Source documentation

   The published kernel gradient estimate yields the long-time averaged kernel bound with the exact displacement-to-heat-length factor.

   theorem averaged_kernel_difference_bound
       {C D B : ℝ} (hC : 0 ≤ C)
       (hdifference : ∀ t : ℝ, 0 < t → t ≤ 1 → ∀ x y z : X, dist x y ≤ Real.sqrt t →
         |ker t x z - ker t y z| ≤
           (C / (Real.sqrt t * μ.real (ball z (Real.sqrt t)))) * dist x y *
             Real.exp (-(dist x z) ^ 2 / (D * t) + B * t))
       {t r A : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) (_hr : 0 < r)
       (x q z : X) (hfinite : μ (ball q r) ≠ ∞) (hvol : 0 < μ.real (ball q r))
       (hcenter : dist x q ≤ A * r) (hscale : (A + 1) * r ≤ Real.sqrt t) :
       |kernelAverage μ ker t (ball q r) z - ker t x z| ≤
         (C / (Real.sqrt t * μ.real (ball z (Real.sqrt t)))) * ((A + 1) * r) *
           Real.exp (-(dist x z) ^ 2 / (D * t) + B * t) := by
   …

   Mentions: OAI.RegularPointCoordinates.kernelAverage