Constant spherical averages give the same ball average

Proved

HunterPDE.Harmonic.ball_average_eq_of_sphereAverage_eq

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

harmonic-functionsintegrationmean-value-property

Let $n\ge1$ , $r>0$ , and let $u$ be continuous on $\overline B_r(x)\subset\mathbb R^n$ . Suppose that its normalized surface average equals a fixed real number $c$ at every radius $0<t\le r$ . Then

\frac{1}{|B_r(x)|}\int_{B_r(x)}u(y)\,dy=c.

This is the polar-coordinate averaging step in Hunter's proof of Theorem 2.1, obtained from Proposition 1.45. It does not assume harmonicity and can be reused for any continuous function with constant spherical means.

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 ball_average_eq_of_sphereAverage_eq {n : ℕ} (hn : 0 < n) {u : EuclideanSpace ℝ (Fin n) → ℝ}
    {x : EuclideanSpace ℝ (Fin n)} {r c : ℝ} (hr : 0 < r)
    (hu : ContinuousOn u (Metric.closedBall x r))
    (havg : ∀ t ∈ Ioc 0 r, sphereAverage u x t = c) :
    (⨍ y in Metric.ball x r, u y) = c := 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