Theorem 4.11 — unique weak solution of −Δu = f in H¹₀(Ω) for f ∈ H⁻¹(Ω)

Proved

HunterPDE.Elliptic.dirichlet_existence

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

elliptic-pdep2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdeweak-solutions

Let $\Omega$ be an open set in $\mathbb{R}^n$ that is bounded in some direction, and let $f \in H^{-1}(\Omega)$ be a bounded linear functional on $H^1_0(\Omega)$ . Then there is a unique weak solution $u \in H^1_0(\Omega)$ of $-\Delta u = f$ in the sense of Definition 4.2, that is,

\int_\Omega Du\cdot D\phi\,dx = \langle f, \phi\rangle \qquad \text{for all } \phi \in H^1_0(\Omega).

This is the model existence theorem of the chapter: the weak Dirichlet problem for the Laplacian is well posed.

Formalization Note. $H^{-1}(\Omega)$ is StrongDual ℝ (H10 n Ω), the bounded linear functionals on $H^1_0(\Omega)$ with its standard norm (Definition 4.1).

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Elliptic_H10

open MeasureTheory

Formal statement

namespace HunterPDE.Elliptic

/-- Theorem 4.11 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 99: if `Ω` is an open set in
`ℝⁿ` that is bounded in some direction and `f ∈ H⁻¹(Ω)`, then there is a unique weak solution
`u ∈ H¹₀(Ω)` of `−Δu = f` in the sense of Definition 4.2, i.e.
`∫_Ω Du · Dφ dx = ⟨f, φ⟩` for all `φ ∈ H¹₀(Ω)`.
`H⁻¹(Ω)` is the space of bounded linear functionals on `H¹₀(Ω)` with its standard norm
(Definition 4.1), `StrongDual ℝ (H10 n Ω)`. -/
theorem dirichlet_existence {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩ : IsOpen Ω)
    (hΩd : BoundedInSomeDirection Ω) (f : StrongDual ℝ (H10 n Ω)) :
    ∃! u : H10 n Ω, ∀ φ : H10 n Ω, ∫ x in Ω, inner ℝ (grad u x) (grad φ x) = f φ := by sorry

end HunterPDE.Elliptic

Source

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

Read-back

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

Let $n \in \mathbb N$ , and let $\Omega \subseteq \mathbb R^n$ satisfy two hypotheses:

$\Omega$ is open;
$\Omega$ is bounded in some direction: there are a unit vector $e$ and reals $a, b$ with $a < x\cdot e < b$ on $\Omega$ .

$H^1_0(\Omega)$ is the closure, in $L^2(\Omega;\mathbb R\times\mathbb R^n)$ , of the span of jets $(\varphi,\nabla\varphi)$ of smooth compactly supported $\varphi$ with closed support in $\Omega$ . Its norm is $\|u\|^2 = \int_\Omega (u^2 + |Du|^2)$ , and $Du(x)$ is the second component of a fixed representative of $u$ .

Let $f$ be any continuous linear functional $H^1_0(\Omega) \to \mathbb R$ , continuous for that norm.

The theorem asserts that there is exactly one $u \in H^1_0(\Omega)$ such that

\int_\Omega Du(x)\cdot D\varphi(x)\,dx = f(\varphi)\quad\text{for every }\varphi \in H^1_0(\Omega).

Uniqueness is as an element of $H^1_0(\Omega)$ , that is, of the almost-everywhere class of the pair $(u, Du)$ .

Degenerate cases:

$n = 0$ : the directional-boundedness hypothesis is unsatisfiable, so the statement is vacuous.
$\Omega = \emptyset$ with $n \ge 1$ : $H^1_0(\Omega)=\{0\}$ and $f = 0$ , so $u = 0$ is the unique solution.
Integrability: the integrand is integrable, because $Du$ and $D\varphi$ are square-integrable. No default integral value arises.

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