Theorem 2.17 — weak maximum principle on a bounded connected domain

Proved

HunterPDE.Harmonic.weak_maximum_principle

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

harmonic-functionsmaximum-principlep2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pde

Let $n \ge 1$ and let $\Omega \subseteq \mathbb{R}^n$ be a bounded, connected open set. If $u \in C^2(\Omega) \cap C(\overline{\Omega})$ is harmonic in $\Omega$ , then

\max_{\overline{\Omega}} u = \max_{\partial\Omega} u, \qquad \min_{\overline{\Omega}} u = \min_{\partial\Omega} u.

A harmonic function on a bounded domain is thus controlled by its boundary values, which gives uniqueness for the Dirichlet problem (Theorem 2.18).

Formalization Note. $\overline{\Omega}$ is closure Ω and $\partial\Omega$ is frontier Ω. Each equality is stated as attainment: some point $y \in \partial\Omega$ satisfies $u(z) \le u(y)$ for all $z \in \overline{\Omega}$ (respectively $u(y) \le u(z)$ ). Both maxima exist by compactness, and since $\partial\Omega \subseteq \overline{\Omega}$ this is equivalent to the equality of maxima. Connected is IsConnected Ω (which includes nonempty). The hypothesis $n \ge 1$ is the book's ambient dimension: for $n = 0$ the whole one-point space is a bounded connected open set with empty boundary.

Preamble

import Mathlib

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.17 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 27 (weak maximum principle):
if `Ω ⊆ ℝⁿ` is a bounded, connected open set and `u ∈ C²(Ω) ∩ C(Ω̄)` is harmonic in `Ω`, then
`max_{Ω̄} u = max_{∂Ω} u` and `min_{Ω̄} u = min_{∂Ω} u`. Each equality is stated as: some point of
`∂Ω = frontier Ω` is a maximum (resp. minimum) point of `u` on `Ω̄ = closure Ω`. Connected includes
nonempty (`IsConnected`), and `n ≥ 1` (for `n = 0` the only nonempty open set is the whole
one-point space, whose boundary is empty). -/
theorem weak_maximum_principle {n : ℕ} (hn : 0 < n) {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hΩ : IsOpen Ω) (hbdd : Bornology.IsBounded Ω)
    (hconn : IsConnected Ω) (hu : InnerProductSpace.HarmonicOnNhd u Ω)
    (hcont : ContinuousOn u (closure Ω)) :
    (∃ y ∈ frontier Ω, ∀ x ∈ closure Ω, u x ≤ u y) ∧
      (∃ y ∈ frontier Ω, ∀ x ∈ closure Ω, u y ≤ u x) := by sorry

end HunterPDE.Harmonic

Source

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

Read-back

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

Hypotheses.

$n \ge 1$ .
$\Omega \subseteq \mathbb{R}^n$ $Ω \subseteq R^{n}$ is:
- open;
- bounded;
- connected, which here includes being nonempty.
$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$ .
$u$ is continuous on the closure $\overline{\Omega}$ .

Conclusion. Both of the following hold, where $\partial\Omega = \overline{\Omega} \setminus \Omega$ is the boundary (frontier) of $\Omega$ :

There exists $y \in \partial\Omega$ with $u(x) \le u(y)$ for all $x \in \overline{\Omega}$ . That is, some boundary point is a maximum point of $u$ on $\overline{\Omega}$ .
There exists $y' \in \partial\Omega$ with $u(y') \le u(x)$ for all $x \in \overline{\Omega}$ . That is, some boundary point is a minimum point of $u$ on $\overline{\Omega}$ .

The two points $y$ and $y'$ need not coincide.

Degenerate cases.

$n = 0$ . Excluded by hypothesis.
Empty $\Omega$ . Excluded by connectedness.
Constant $u$ . If $u$ is constant, every boundary point serves as both $y$ and $y'$ .
Behaviour outside $\overline{\Omega}$ . No condition is imposed on $u$ outside $\overline{\Omega}$ . No differentiability is required at boundary points, only continuity on $\overline{\Omega}$ .

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