Theorem 2.5 — mean value inequalities for sub- and superharmonic functions

Proved

HunterPDE.Harmonic.mean_value_inequality

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

mean-value-propertyp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesubharmonic-functions

Let $n \ge 1$ , let $\Omega \subseteq \mathbb{R}^n$ be open, $B_r(x) \Subset \Omega$ and $u \in C^2(\Omega)$ . If $u$ is subharmonic in $\Omega$ ( $\Delta u \ge 0$ ), then

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

If $u$ is superharmonic in $\Omega$ ( $\Delta u \le 0$ ), then

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

The inequality (2.5) is what the proof of the strong maximum principle (Theorem 2.13) uses.

Formalization Note. Sub- and superharmonicity (Definition 2.4, including $u \in C^2(\Omega)$ ) are the definition item Subharmonic; the averages are those of MeanValue. $B_r(x) \Subset \Omega$ is 0 < r and Metric.closedBall x r ⊆ Ω. The two cases are stated as a conjunction of two implications. $n \ge 1$ keeps the sphere nonempty.

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Harmonic_MeanValue
import Definitions.Def_HunterPDE_Harmonic_Subharmonic

open MeasureTheory

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.5 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 22: let `Ω ⊆ ℝⁿ` be open,
`B_r(x) ⋐ Ω` (the closed ball lies in `Ω`, `r > 0`) and `u ∈ C²(Ω)`. If `u` is subharmonic in `Ω`
(`Δu ≥ 0`), then `u(x)` is at most its average over the ball `B_r(x)` and at most its average over
the sphere `∂B_r(x)` (2.5); if `u` is superharmonic in `Ω` (`Δu ≤ 0`), both inequalities are
reversed (2.6). The `C²` hypothesis is part of `IsSubharmonicOn` / `IsSuperharmonicOn`
(Definition 2.4). `n ≥ 1`, so that the sphere is nonempty. -/
theorem mean_value_inequality {n : ℕ} (hn : 0 < n) {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hΩ : IsOpen Ω)
    {x : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall x r ⊆ Ω) :
    (IsSubharmonicOn Ω u →
        u x ≤ (⨍ y in Metric.ball x r, u y) ∧ u x ≤ sphereAverage u x r) ∧
      (IsSuperharmonicOn Ω u →
        (⨍ y in Metric.ball x r, u y) ≤ u x ∧ sphereAverage u x r ≤ u x) := by sorry

end HunterPDE.Harmonic

Source

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

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}$ .
$x \in \mathbb{R}^n$ and $r > 0$ satisfy $\overline{B}_r(x) \subseteq \Omega$ .

Write

A_B = \frac{1}{\lambda(B_r(x))}\int_{B_r(x)} u\,d\lambda

for the average over the open ball ( $\lambda$ Lebesgue measure). Write

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

for the sphere average, with $\sigma(A) = n\,\lambda(\{ta : 0<t<1,\ a\in A\})$ on the unit sphere $S^{n-1}$ . Each average is $0$ if its integrand is not integrable.

Conclusion. Two implications hold simultaneously:

If $u$ is $C^2$ on $\Omega$ and $\Delta u(y) \ge 0$ for all $y \in \Omega$ (subharmonic), then

u(x) \le A_B \quad\text{and}\quad u(x) \le A_S.

If $u$ is $C^2$ on $\Omega$ and $\Delta u(y) \le 0$ for all $y \in \Omega$ (superharmonic), then

A_B \le u(x) \quad\text{and}\quad A_S \le u(x).

Here $\Delta u(y) = \sum_i D^2u(y)(e_i,e_i)$ .

Degenerate cases.

$n = 0$ . Excluded by hypothesis.
$n = 1$ . $A_S = \tfrac12(u(x+r)+u(x-r))$ .
Openness. Since $\Omega$ is open, " $C^2$ on $\Omega$ " is ordinary $C^2$ near each point of $\Omega$ .
Integrability. $u$ is then continuous on the compact set $\overline{B}_r(x) \subseteq \Omega$ , so the zero convention for non-integrable integrands does not arise when either implication's premise holds.
Premise fails. If $u$ is neither subharmonic nor superharmonic, the corresponding implication is vacuous.
Both premises hold. If $u$ is both (i.e. $C^2$ with $\Delta u = 0$ on $\Omega$ ), both implications apply and force $u(x) = A_B = A_S$ .

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