Vanishing radial derivative of spherical averages of harmonic functions

Proved

HunterPDE.Harmonic.hasDerivAt_sphereAverage_zero

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

harmonic-functionsintegrationmean-value-property

Let $n\ge1$ , $r>0$ , and let $u$ be harmonic in a neighborhood of every point of the closed ball $\overline B_r(x)\subset\mathbb R^n$ . Write $A(t)$ for the normalized surface average of $u$ on the sphere of radius $t$ about $x$ . Then

A'(r)=0.

This is the harmonic specialization of Hunter's radial derivative identity (2.4). It isolates the differentiation-under-the-integral and divergence-theorem step, and applies without selecting a surrounding open domain.

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_zero {n : ℕ} (hn : 0 < n) {u : EuclideanSpace ℝ (Fin n) → ℝ}
    {x : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 < r)
    (hu : InnerProductSpace.HarmonicOnNhd u (Metric.closedBall x r)) :
    HasDerivAt (sphereAverage u x) 0 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, Eq. (2.4); polar integration: p. 17, Proposition 1.45.

View graph