OAI/Geometry/RCD/Harmonic/EuclideanRadialAverageDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.hasDerivAt_radial_average line 16

   Source documentation

   A global C² compact extension permits differentiation in the averaging radius with an integrable bound independent of that radius.

   theorem hasDerivAt_radial_average {n : ℕ} {f : Euclidean n → ℝ}
       (hf : ContDiff ℝ 2 f) (hfs : HasCompactSupport f) (p : Euclidean n) (t : ℝ) :
       HasDerivAt (fun s : ℝ => ∫ x, f (p+s • x)*euclideanRadialWeight n x)
         (∫ x, fderiv ℝ f (p+t • x) x*euclideanRadialWeight n x) t := by
   …

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