Theorem 2.7 — first-derivative estimate |∂ᵢu(x)| ≤ (n/r) max |u| for harmonic u

Proved

HunterPDE.Harmonic.harmonic_derivative_estimate

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

derivative-estimatesharmonic-functionsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pde

Let $\Omega \subseteq \mathbb{R}^n$ be open, let $u \in C^2(\Omega)$ be harmonic in $\Omega$ , and let $B_r(x) \Subset \Omega$ . Then for every $1 \le i \le n$

|\partial_i u(x)| \le \frac{n}{r} \max_{\overline{B}_r(x)} |u|.

The estimate bounds a derivative of a harmonic function at a point by the size of the function on a surrounding ball; it gives Liouville's theorem (Corollary 2.8) and is the base case of the higher-order estimate (Theorem 2.9).

Formalization Note. The maximum over the closed ball is expressed through an arbitrary bound: for every real $M$ with $|u| \le M$ on $\overline{B}_r(x)$ , $|\partial_i u(x)| \le (n/r) M$ . Since $u$ is continuous on the compact ball the maximum is attained, so taking $M = \max_{\overline{B}_r(x)} |u|$ recovers the book's form, and the two are equivalent. Coordinates are 0-based (i : Fin n); $\partial_i u$ is HunterPDE.Shared.partialDeriv u i from the shared definition HunterPDE.Shared.PartialDeriv. Harmonic on $\Omega$ is InnerProductSpace.HarmonicOnNhd u Ω.

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Shared_PartialDeriv

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.7 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 23: if `u ∈ C²(Ω)` is harmonic
in the open set `Ω ⊆ ℝⁿ` and `B_r(x) ⋐ Ω`, then for every coordinate `i`,
`|∂ᵢu(x)| ≤ (n / r) max_{B̄_r(x)} |u|`. The maximum is expressed through an arbitrary bound `M`
of `|u|` on the closed ball `B̄_r(x)` (taking `M` to be the maximum gives the book's form). -/
theorem harmonic_derivative_estimate {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 ⊆ Ω)
    (i : Fin n) {M : ℝ} (hM : ∀ y ∈ Metric.closedBall x r, |u y| ≤ M) :
    |Shared.partialDeriv u i x| ≤ (n / r) * M := by sorry

end HunterPDE.Harmonic

Source

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

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}$ $u : R^{n} \to R$ is harmonic near every point of $\Omega$ $Ω$ . For each $p \in \Omega$ $p \in Ω$ :
- $u$ is $C^2$ on a neighbourhood of $p$ ;
- $\Delta u = \sum_i D^2u(\cdot)(e_i,e_i)$ vanishes on a neighbourhood of $p$ .
$x \in \mathbb{R}^n$ and $r > 0$ satisfy $\overline{B}_r(x) \subseteq \Omega$ .
$i$ is a coordinate index in $\{1,\dots,n\}$ .
$M$ is a real number with $|u(y)| \le M$ for all $y \in \overline{B}_r(x)$ .

Conclusion.

\big|\operatorname{partialDeriv}(u, i, x)\big| \le \frac{n}{r}\, M.

Here $\operatorname{partialDeriv}(u,i,x)$ is a notion defined elsewhere in the bundle, whose definition is not part of the code shown. By its name it is the $i$ -th partial derivative $\partial_i u(x)$ , but its precise meaning, including any convention at points where the derivative does not exist, cannot be read off from this text.

Degenerate cases.

$n = 0$ . There is no index $i$ , so the statement is vacuous. For $n \ge 1$ the factor $n$ is the real number $n$ .
Sign of $M$ . Since $r > 0$ , the closed ball contains $x$ , so any admissible $M$ satisfies $M \ge |u(x)| \ge 0$ .
Choice of $M$ . $M$ may be any upper bound for $|u|$ on the closed ball, not necessarily the maximum. The bound weakens as $M$ grows.

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