Theorem 4.9 — Poincaré inequality on H¹₀(Ω) for Ω bounded in some direction

Proved

HunterPDE.Elliptic.poincare

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

p2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1pdepoincare-inequalitysobolev-spaces

Let $\Omega$ be an open set in $\mathbb{R}^n$ that is bounded in some direction: there are a unit vector $e$ and constants $a, b$ with $a < x \cdot e < b$ for all $x \in \Omega$ . Then there is a constant $C$ such that

\int_\Omega u^2\,dx \le C \int_\Omega |Du|^2\,dx \qquad \text{for all } u \in H^1_0(\Omega).

The inequality shows that $\big(\int_\Omega |Du|^2\big)^{1/2}$ is a norm on $H^1_0(\Omega)$ equivalent to the standard one, which is the entry point to existence for the Dirichlet problem.

Formalization Note. $C$ depends only on $\Omega$ : it is quantified before $u$ . $H^1_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in the $H^1$ norm (definition H10).

Preamble

import Mathlib
import Definitions.Def_HunterPDE_Elliptic_H10

open MeasureTheory

Formal statement

namespace HunterPDE.Elliptic

/-- Theorem 4.9 of Hunter, *Notes on PDEs* (revised 6/18/2014), p. 98 (Poincaré inequality): if
`Ω` is an open set in `ℝⁿ` that is bounded in some direction (it lies between two parallel
hyperplanes `a < x · e < b`, `e` a unit vector), then there is a constant `C` such that
`∫_Ω u² dx ≤ C ∫_Ω |Du|² dx` for all `u ∈ H¹₀(Ω)`. The constant `C` depends only on `Ω`: it is
quantified before `u`. -/
theorem poincare {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩ : IsOpen Ω)
    (hΩd : BoundedInSomeDirection Ω) :
    ∃ C : ℝ, ∀ u : H10 n Ω,
      ∫ x in Ω, val u x ^ 2 ≤ C * ∫ x in Ω, ‖grad u x‖ ^ 2 := by sorry

end HunterPDE.Elliptic

Source

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

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 \in \mathbb R^n$ and reals $a, b$ with $a < x\cdot e < b$ for every $x \in \Omega$ .

Here $H^1_0(\Omega)$ is the closure, in $L^2(\Omega;\mathbb R\times\mathbb R^n)$ , of the span of the jets $(\varphi,\nabla\varphi)$ of smooth compactly supported $\varphi$ with closed support in $\Omega$ . For $u$ in that space, $u(x)$ and $Du(x)$ are the first and second components of a fixed representative of the pair.

The theorem asserts that there is a real number $C$ such that, for every $u \in H^1_0(\Omega)$ ,

\int_\Omega u(x)^2\,dx \;\le\; C\int_\Omega |Du(x)|^2\,dx .

$C$ is chosen before $u$ , so it is the same for all $u$ . $C$ is not required to be positive.

Degenerate cases:

$n = 0$ : no unit vector exists in $\mathbb R^0$ , so the directional-boundedness hypothesis cannot hold and the statement is vacuous.
$\Omega = \emptyset$ with $n \ge 1$ : the hypotheses hold, both integrals are $0$ , and every real $C$ works.
Integrability: both integrands are integrable because $u$ and $Du$ are square-integrable on $\Omega$ . So 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