Theorem 2.1 — mean value property of harmonic functions on balls and spheres

Proved

HunterPDE.Harmonic.mean_value_property

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

harmonic-functionsmean-value-propertyp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pde

Let $n \ge 1$ , let $\Omega \subseteq \mathbb{R}^n$ be open and let $u \in C^2(\Omega)$ be harmonic in $\Omega$ , i.e. $\Delta u = 0$ in $\Omega$ . If $B_r(x) \Subset \Omega$ (with $r > 0$ , the closed ball $\overline{B}_r(x)$ lies in $\Omega$ ), then $u(x)$ equals both its average over the ball and its average over the sphere:

u(x) = ⨍_{B_r(x)} u \, dx, \qquad u(x) = ⨍_{\partial B_r(x)} u \, dS. \qquad (2.3)

This is the basic tool of the chapter: the derivative estimates (Theorems 2.7, 2.9), analyticity (Theorem 2.10) and the maximum principle all rest on it.

Formalization Note. "Harmonic, $u \in C^2(\Omega)$ " on the open set $\Omega$ is Mathlib's InnerProductSpace.HarmonicOnNhd u Ω ( $C^2$ near every point of $\Omega$ and $\Delta u = 0$ near every point). $B_r(x) \Subset \Omega$ is 0 < r and Metric.closedBall x r ⊆ Ω. The sphere average is sphereAverage from the definition item MeanValue. The hypothesis $n \ge 1$ makes the sphere nonempty (for $n = 0$ it is empty and its average is the junk value $0$ ); the book works in $\mathbb{R}^n$ with $n \ge 1$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Harmonic_MeanValue

open MeasureTheory

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.1 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 20: if `u ∈ C²(Ω)` is harmonic
in an open set `Ω ⊆ ℝⁿ` and `B_r(x) ⋐ Ω` (the closed ball lies in `Ω`, `r > 0`), then `u(x)` is
the average of `u` over the ball `B_r(x)` and over the sphere `∂B_r(x)`. Harmonic on the open set
`Ω` is Mathlib's `HarmonicOnNhd` (`C²` near every point of `Ω` and `Δu = 0` there). -/
theorem mean_value_property {n : ℕ} (hn : 0 < n) {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hΩ : IsOpen Ω) (hu : InnerProductSpace.HarmonicOnNhd u Ω)
    {x : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall x r ⊆ Ω) :
    u x = (⨍ y in Metric.ball x r, u y) ∧ u x = sphereAverage u x r := by sorry

end HunterPDE.Harmonic

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), p. 20, Theorem 2.1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Hypotheses.

$n \ge 1$ .
$\Omega \subseteq \mathbb{R}^n$ is open.
$u : \mathbb{R}^n \to \mathbb{R}$ is harmonic near every point of $\Omega$ . That is, for each $p \in \Omega$ :
- $u$ is $C^2$ on some neighbourhood of $p$ ;
- $\Delta u$ vanishes identically on some neighbourhood of $p$ .
Here $\Delta u(y) = \sum_i D^2u(y)(e_i,e_i)$ , the trace of the second Fréchet derivative.
$x \in \mathbb{R}^n$ and $r > 0$ are such that $\overline{B}_r(x) = \{y : |y-x| \le r\} \subseteq \Omega$ .

Conclusion. Both

u(x) = \frac{1}{\lambda(B_r(x))}\int_{B_r(x)} u \, d\lambda \qquad\text{and}\qquad u(x) = \operatorname{sphereAverage}(u,x,r).

Here $\lambda$ is Lebesgue measure and $B_r(x)$ the open ball. The sphere average is

\operatorname{sphereAverage}(u,x,r) = \frac{1}{\sigma(S^{n-1})}\int_{S^{n-1}} u(x+ry)\,d\sigma(y),

where $S^{n-1}$ is the unit sphere and $\sigma(A) = n\,\lambda(\{ta : 0<t<1,\ a\in A\})$ . Either average is defined to be $0$ if the integrand is not integrable.

Degenerate cases.

$n = 0$ . Excluded by hypothesis. In that case the sphere would be empty and its average $0$ .
$n = 1$ . The sphere average is $\tfrac12(u(x+r)+u(x-r))$ .
Integrability. Under the hypotheses, $u$ is continuous on a neighbourhood of the compact set $\overline{B}_r(x)$ . So the integrals are over integrable functions, and the zero convention for non-integrable integrands does not come into play.
No admissible ball. If $\Omega$ contains no closed ball of positive radius, for example if $\Omega$ is empty, the theorem is vacuous.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph