Continuity of spherical averages on a closed radius interval
ProvedHunterPDE.Harmonic.sphereAverage_continuousOnharmonic-functionsintegrationmean-value-property
Let be a real-valued continuous function on the closed ball of radius about in . Its normalized spherical average , defined using the fixed unit sphere and the map , satisfies
This supplies the continuity at radius zero and at the outer radius needed to pass from a radial derivative identity to a mean-value formula. In dimension zero the defining spherical measure is zero, and the average remains the constant zero function.
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 sphereAverage_continuousOn {n : ℕ} {u : EuclideanSpace ℝ (Fin n) → ℝ}
{x : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 ≤ r)
(hu : ContinuousOn u (Metric.closedBall x r)) :
ContinuousOn (sphereAverage u x) (Icc 0 r) := by sorry
end HunterPDE.HarmonicSource
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.