Theorem 2.2 — a continuous function with the mean-value property is smooth and harmonic

Proved

HunterPDE.Harmonic.smooth_of_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-v1pderegularity

Let $\Omega \subseteq \mathbb{R}^n$ be open and let $u \in C(\Omega)$ have the mean-value property (2.3): for every ball $B_r(x) \Subset \Omega$ ,

u(x) = ⨍_{B_r(x)} u \, dx \quad\text{and}\quad u(x) = ⨍_{\partial B_r(x)} u \, dS.

Then $u \in C^\infty(\Omega)$ and $\Delta u = 0$ in $\Omega$ .

Together with Theorem 2.1 this characterizes harmonic functions by the mean-value property and shows that every $C^2$ harmonic function is $C^\infty$ , which the proof of analyticity (Theorem 2.10) uses.

Formalization Note. $u \in C(\Omega)$ is ContinuousOn u Ω; the mean-value property is HasMeanValueProperty Ω u from the definition item MeanValue (both identities of (2.3), for every $r > 0$ with $\overline{B}_r(x) \subseteq \Omega$ ). $C^\infty$ is ContDiffOn ℝ ∞ u Ω with ∞ the smooth order (not ω, which would be analyticity). $\Delta$ is Mathlib's laplacian.

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Harmonic_MeanValue

open Laplacian
open scoped ContDiff

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.2 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 21: if `u ∈ C(Ω)` has the
mean-value property (2.3) in the open set `Ω ⊆ ℝⁿ`, then `u ∈ C^∞(Ω)` and `Δu = 0` in `Ω`.
`∞` is `C^∞` (not `ω`, which would be analyticity). -/
theorem smooth_of_mean_value_property {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hΩ : IsOpen Ω) (hu : ContinuousOn u Ω)
    (hmv : HasMeanValueProperty Ω u) :
    ContDiffOn ℝ ∞ u Ω ∧ ∀ x ∈ Ω, Δ u x = 0 := by sorry

end HunterPDE.Harmonic

Source

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

Read-back

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

Hypotheses.

$n \in \mathbb{N}$ is arbitrary.
$\Omega \subseteq \mathbb{R}^n$ is open.
$u : \mathbb{R}^n \to \mathbb{R}$ is continuous on $\Omega$ .
$u$ has the mean-value property on $\Omega$ . For every $x$ and every $r > 0$ with $\overline{B}_r(x) \subseteq \Omega$ :

u(x) = \frac{1}{\lambda(B_r(x))}\int_{B_r(x)} u\,d\lambda \qquad\text{and}\qquad u(x) = \frac{1}{\sigma(S^{n-1})}\int_{S^{n-1}} u(x+ry)\,d\sigma(y).

Here $\lambda$ is Lebesgue measure and $S^{n-1}$ the unit sphere. The measure is $\sigma(A) = n\,\lambda(\{ta: 0<t<1,\ a\in A\})$ . Each average is $0$ when its integrand is non-integrable or the measure of the domain is $0$ .

Conclusion. Both of the following hold:

$u$ is infinitely differentiable ( $C^\infty$ ) on $\Omega$ , in the sense of $C^\infty$ relative to $\Omega$ , which for open $\Omega$ is ordinary smoothness near each point.
$\Delta u(x) = 0$ for every $x \in \Omega$ , where $\Delta u(x) = \sum_i D^2u(x)(e_i,e_i)$ .

Degenerate cases.

Empty $\Omega$ . Both conclusions hold trivially.
$n = 0$ . There is no hypothesis $n \ge 1$ . The space is one point, the sphere average is $0$ , and the ball average is $u(0)$ . So for $\Omega = \{0\}$ the mean-value hypothesis amounts to $u(0) = 0$ . The conclusion is then automatic: any function is smooth on a point, and the Laplacian on a $0$ -dimensional space is the empty sum $0$ .
Integrability. Continuity of $u$ on $\Omega$ makes $u$ integrable over each admissible compact closed ball and its sphere. So the zero convention for non-integrable integrands is not triggered by admissible balls.

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