Differentiating spherical averages under the unit-sphere integral

Proved

HunterPDE.Harmonic.hasDerivAt_sphereAverage_radial

by Mazecto · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

differentiation-under-integralharmonic-functionsintegration

Let $n\ge1$ , $r>0$ , and suppose $u:\mathbb R^n\to\mathbb R$ is continuously differentiable in a neighborhood of each point of the closed ball $\overline B_r(x)$ . Let $\sigma$ denote the surface measure of the unit sphere. Then the spherical average has the derivative

\frac{d}{dt}\bigg|_{t=r}\operatorname{sphereAverage}(u,x,t)=\frac{1}{\sigma(S^{n-1})}\int_{S^{n-1}} Du(x+r\omega)[\omega]\,d\sigma(\omega).

The derivative is two-sided. Compactness of the closed ball and neighborhood regularity provide the uniform control needed to differentiate under the integral. This is the differentiation step in Hunter's derivation of (2.4).

Preamble

import Definitions.Def_HunterPDE_Harmonic_MeanValue
import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

open MeasureTheory Set
open HunterPDE.Harmonic

Formal statement

namespace HunterPDE.Harmonic

theorem hasDerivAt_sphereAverage_radial {n : ℕ} (hn : 0 < n)
    {u : EuclideanSpace ℝ (Fin n) → ℝ} {x : EuclideanSpace ℝ (Fin n)}
    {r : ℝ} (hr : 0 < r)
    (hu : ∀ y ∈ Metric.closedBall x r, ContDiffAt ℝ 1 u y) :
    HasDerivAt (sphereAverage u x)
      (⨍ ω : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1,
        fderiv ℝ u (x + r • ω.1) ω.1 ∂(volume.toSphere)) r := by sorry

end HunterPDE.Harmonic

Source

John K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, p. 20, proof of Theorem 2.1, derivation of Eq. (2.4); divergence theorem: p. 17, Theorem 1.46. Neighborhood regularity is expressed pointwise as ContDiffAt on the closed ball.

View graph