OAI/Geometry/RCD/Heat/EuclideanRadialKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.euclideanRadialKernel line 14
2. theorem OAI.RegularPointCoordinates.euclideanRadialKernel_smooth line 17
3. theorem OAI.RegularPointCoordinates.euclideanRadialKernel_support line 21
4. theorem OAI.RegularPointCoordinates.euclideanRadialKernel_compact line 31
5. theorem OAI.RegularPointCoordinates.convolution_radialKernel_eq line 37

   Source documentation

   Scaling the kernel produces precisely the dilation average, including its Euclidean volume factor.

   theorem convolution_radialKernel_eq (n : ℕ) (f : Euclidean n → ℝ) (p : Euclidean n)
       {r : ℝ} (hr : 0 < r) :
       (f ⋆[ContinuousLinearMap.mul ℝ ℝ,volume] euclideanRadialKernel n r) p =
         r^n*(∫ x, f (p+r • x)*euclideanRadialWeight n x) := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialKernel, OAI.RegularPointCoordinates.euclideanRadialWeight

6. theorem OAI.RegularPointCoordinates.harmonic_convolution_radialKernel line 68

   Source documentation

   The radial mean theorem becomes an actual local convolution identity.

   theorem harmonic_convolution_radialKernel {n : ℕ} {f : Euclidean n → ℝ}
       (hf : ContDiff ℝ 2 f) (hfs : HasCompactSupport f) (p : Euclidean n)
       {R r : ℝ} (hR : 0 < R) (hr : 0 < r) (hrR : r < R)
       (hh : InnerProductSpace.HarmonicOnNhd f (ball p R)) :
       (f ⋆[ContinuousLinearMap.mul ℝ ℝ,volume] euclideanRadialKernel n r) p =
         (r^n*(∫ x, euclideanRadialWeight n x))*f p := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.euclideanRadialKernel, OAI.RegularPointCoordinates.euclideanRadialWeight