Theorem 2.9 — |∂^α u(x)| ≤ nᵏ e^{k−1} k!/rᵏ · max |u| for harmonic u

Proved

HunterPDE.Harmonic.harmonic_higher_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 multi-index $\alpha \in \mathbb{N}_0^n$ of order $k = |\alpha| \ge 1$

|\partial^\alpha u(x)| \le \frac{n^k e^{k-1} k!}{r^k} \max_{\overline{B}_r(x)} |u|.

The constant grows like $k!$ times a geometric factor, which is exactly what makes the Taylor series of $u$ converge (Theorem 2.10).

Formalization Note. The constant is the book's, stated exactly. The book writes "for any multi-index $\alpha \in \mathbb{N}_0^n$ "; the statement adds the restriction $k \ge 1$ , because at $k = 0$ the bound would read $|u(x)| \le e^{-1}\max|u|$ , which fails for $u \equiv 1$ , and the book's induction starts at $k = 1$ (Theorem 2.7). As in Theorem 2.7, the maximum is expressed through an arbitrary bound $M \ge |u|$ on $\overline{B}_r(x)$ , equivalently. $\partial^\alpha u$ is HunterPDE.Shared.multiDeriv u α from the shared definition HunterPDE.Shared.PartialDeriv (0-based coordinates); $k$ is given with the hypothesis $\sum_i \alpha_i = k$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Shared_PartialDeriv

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.9 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 multi-index `α` of order `k = |α| ≥ 1`,
`|∂^α u(x)| ≤ (n^k e^{k-1} k! / r^k) max_{B̄_r(x)} |u|`. The maximum is expressed through an
arbitrary bound `M` of `|u|` on `B̄_r(x)`. The page states the bound for every `α ∈ ℕ₀ⁿ`; at
`k = 0` it would read `|u(x)| ≤ e^{-1} max |u|`, which fails for `u ≡ 1`, and the proof's induction
starts at `k = 1` (Theorem 2.7), so `1 ≤ k` is assumed. -/
theorem harmonic_higher_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 ⊆ Ω)
    (α : Fin n → ℕ) (k : ℕ) (hk : ∑ i, α i = k) (hk1 : 1 ≤ k)
    {M : ℝ} (hM : ∀ y ∈ Metric.closedBall x r, |u y| ≤ M) :
    |Shared.multiDeriv u α x| ≤ ((n : ℝ) ^ k * Real.exp 1 ^ (k - 1) * (k.factorial : ℝ) / r ^ k) * M := by sorry

end HunterPDE.Harmonic

Source

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

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$ .
$\alpha = (\alpha_1,\dots,\alpha_n) \in \mathbb{N}^n$ is a multi-index.
$k \in \mathbb{N}$ satisfies $\alpha_1 + \cdots + \alpha_n = k$ and $k \ge 1$ .
$M$ is a real number with $|u(y)| \le M$ for all $y \in \overline{B}_r(x)$ .

Conclusion.

\big|\operatorname{multiDeriv}(u,\alpha,x)\big| \le \frac{n^k\, e^{\,k-1}\, k!}{r^k}\, M.

Here $e$ is Euler's number and $n$ is taken as a real number. $\operatorname{multiDeriv}(u,\alpha,x)$ is a notion defined elsewhere in the bundle, whose definition is not part of the code shown. By its name it is the mixed partial derivative $\partial^\alpha u(x)$ , but its precise meaning, including the order of differentiation and any convention where derivatives do not exist, cannot be read off from this text.

Degenerate cases.

Exponent $k-1$ . This is natural-number subtraction, but $k \ge 1$ , so it is the true value $k-1$ . The division by $r^k$ is by a positive number.
$n = 0$ . The only multi-index is empty with sum $0$ , which contradicts $k \ge 1$ . So the statement is vacuous.
$k = 0$ . Excluded by hypothesis.
Sign and choice of $M$ . Any admissible $M$ is $\ge |u(x)| \ge 0$ . $M$ may be any upper bound for $|u|$ on the closed ball, not necessarily the maximum.

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