Theorem 2.10 — harmonic functions are real-analytic

Proved

HunterPDE.Harmonic.harmonic_real_analytic

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

analyticityharmonic-functionsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pde

Let $\Omega \subseteq \mathbb{R}^n$ be open. If $u \in C^2(\Omega)$ is harmonic in $\Omega$ , then $u$ is real-analytic in $\Omega$ : every $x \in \Omega$ has a neighbourhood on which $u$ is the sum of a convergent power series centred at $x$ ,

u(x + h) = \sum_{\alpha \in \mathbb{N}_0^n} \frac{\partial^\alpha u(x)}{\alpha!} h^\alpha \qquad (|h| \text{ small}).

A $C^2$ solution of Laplace's equation is therefore determined on a connected open set by its germ at a single point (Corollary 2.11); this is the prototype of analytic regularity for elliptic equations.

Formalization Note. Real-analytic in $\Omega$ is Mathlib's AnalyticOnNhd ℝ u Ω (analytic at every point of $\Omega$ , i.e. a power series with positive radius converging to $u$ near each point); it is not analyticity on a single ball. Harmonic on the open set $\Omega$ is InnerProductSpace.HarmonicOnNhd u Ω. The statement holds for every $n$ .

Preamble

import Mathlib

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.10 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 24: if `u ∈ C²(Ω)` is harmonic
in an open set `Ω ⊆ ℝⁿ`, then `u` is real-analytic in `Ω`: at every point of `Ω` it has a power
series expansion converging to `u` on a ball of positive radius (`AnalyticOnNhd ℝ u Ω`). -/
theorem harmonic_real_analytic {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hΩ : IsOpen Ω) (hu : InnerProductSpace.HarmonicOnNhd u Ω) :
    AnalyticOnNhd ℝ u Ω := by sorry

end HunterPDE.Harmonic

Source

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

Read-back

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

Let $n \in \mathbb{N}$ be arbitrary, and write $\mathbb{R}^n$ for $n$ -dimensional Euclidean space: real $n$ -tuples $x = (x_1, \dots, x_n)$ with the standard Euclidean inner product and norm. Let $\Omega \subseteq \mathbb{R}^n$ be a set, and let $u : \mathbb{R}^n \to \mathbb{R}$ be a real-valued function defined on all of $\mathbb{R}^n$ , not only on $\Omega$ . The statement makes two assumptions:

$\Omega$ is open in $\mathbb{R}^n$ .
$u$ $u$ is harmonic on a neighbourhood of every point of $\Omega$ $Ω$ . Concretely, for every $x \in \Omega$ $x \in Ω$ both of the following hold:
- $u$ is $C^2$ at $x$ , meaning $u$ is twice continuously (Fréchet) differentiable on some open neighbourhood of $x$ ;
- the Laplacian of $u$ vanishes at every point of some neighbourhood $U_x$ of $x$ . The Laplacian is the trace of the second derivative with respect to an orthonormal basis, which here amounts to

\Delta u(y) \;=\; \sum_{i=1}^{n} \frac{\partial^2 u}{\partial x_i^2}(y) \;=\; 0 \quad \text{for all } y \in U_x.

These neighbourhoods are only required to exist around each point of $\Omega$ . Nothing prevents them from reaching outside $\Omega$ , and no condition is placed on $u$ away from such neighbourhoods.

Under these hypotheses, the theorem concludes that $u$ is real-analytic at every point of $\Omega$ . That is, for every $x_0 \in \Omega$ there exist:

a formal power series $\sum_{k \ge 0} p_k$ in the displacement, where each $p_k$ is a continuous symmetric $k$ -linear map on $\mathbb{R}^n$ , applied as $p_k(h, \dots, h)$ ;
a radius $r > 0$ , not exceeding the series' radius of convergence,

such that

u(x_0 + h) \;=\; \sum_{k=0}^{\infty} p_k(h,\dots,h) \qquad \text{for all } h \text{ with } \|h\| < r,

with the series converging there. The radius $r$ may depend on $x_0$ . The statement does not assert that the ball of radius $r$ lies inside $\Omega$ , and it gives no uniformity of $r$ across $\Omega$ .

Degenerate cases:

$\Omega = \emptyset$ . Both the hypothesis and the conclusion are vacuous, so the statement asserts nothing.
$n = 0$ . Here $\mathbb{R}^0$ is a single point. Every function on it is constant, the Laplacian is an empty sum and therefore identically $0$ , and the conclusion holds trivially for every $u$ and every $\Omega$ .
Undefined second derivatives. No junk value of the Laplacian enters at points that matter: at every point of $U_x$ where the vanishing is required, $u$ is twice differentiable, provided $U_x$ is taken inside the $C^2$ neighbourhood. The formal definition, however, does not itself insist on this.
The openness hypothesis. The assumption that $\Omega$ is open is stated separately. The conclusion concerns only points of $\Omega$ and neighbourhoods around them.

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