Theorem 2.13 — strong maximum principle for subharmonic functions

Proved

HunterPDE.Harmonic.strong_maximum_principle

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

maximum-principlep2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdesubharmonic-functions

Let $\Omega \subseteq \mathbb{R}^n$ be a connected open set and $u \in C^2(\Omega)$ . If $u$ is subharmonic ( $\Delta u \ge 0$ in $\Omega$ ) and attains a global maximum value in $\Omega$ , i.e. there is $x_0 \in \Omega$ with

u(x) \le u(x_0) \qquad \text{for all } x \in \Omega,

then $u$ is constant in $\Omega$ .

Applied to $u$ and $-u$ it gives the strong maximum and minimum principle for harmonic functions (Theorem 2.15).

Formalization Note. Subharmonicity (with $u \in C^2(\Omega)$ ) is IsSubharmonicOn Ω u from the definition item Subharmonic. Connectedness is IsPreconnected Ω; nonemptiness is implied by the existence of the maximum point, so this is the book's "connected". Constant in $\Omega$ is $\exists c, \forall x \in \Omega, u(x) = c$ .

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Harmonic_Subharmonic

Formal statement

namespace HunterPDE.Harmonic

/-- Theorem 2.13 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 26 (strong maximum
principle): if `Ω ⊆ ℝⁿ` is a connected open set, `u ∈ C²(Ω)` is subharmonic (`Δu ≥ 0` in `Ω`) and
`u` attains a global maximum value in `Ω` (at some `x₀ ∈ Ω`), then `u` is constant in `Ω`. -/
theorem strong_maximum_principle {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω)
    (hu : IsSubharmonicOn Ω u) (hmax : ∃ x₀ ∈ Ω, ∀ x ∈ Ω, u x ≤ u x₀) :
    ∃ c : ℝ, ∀ x ∈ Ω, u x = c := by sorry

end HunterPDE.Harmonic

Source

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

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 and preconnected, meaning it cannot be split into two disjoint nonempty relatively open pieces. The empty set counts as preconnected.
$u : \mathbb{R}^n \to \mathbb{R}$ $u : R^{n} \to R$ is subharmonic on $\Omega$ $Ω$ :
- $u$ is $C^2$ on $\Omega$ ;
- $\Delta u(x) = \sum_i D^2u(x)(e_i,e_i) \ge 0$ for all $x \in \Omega$ .
$u$ attains its maximum over $\Omega$ : there is $x_0 \in \Omega$ with $u(x) \le u(x_0)$ for all $x \in \Omega$ .

Conclusion. $u$ is constant on $\Omega$ : there is a real $c$ with $u(x) = c$ for all $x \in \Omega$ .

Degenerate cases.

Empty $\Omega$ . The hypothesis on $x_0$ forces $\Omega$ to be nonempty, so empty $\Omega$ cannot occur.
$n = 0$ . $\Omega$ is the single point, where every function is constant, so the statement is trivially true.
Values outside $\Omega$ . Only the values of $u$ on $\Omega$ are constrained. Since $\Omega$ is open, " $C^2$ on $\Omega$ " is ordinary $C^2$ near each point of $\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