Prove2Me

Smooth Poincaré estimate on a slab with explicit width constant

Proved
HunterPDE.Elliptic.smooth_slab_poincare

by Mazecto · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

pdepoincare-inequalitysobolev-spaces

Let Ω\Omega be an open subset of Rn\mathbb R^n contained in a slab a<x⋅e<ba<x\cdot e<b, where ∥e∥=1\|e\|=1. Every smooth compactly supported real function φ\varphi whose closed support lies in Ω\Omega satisfies

∫Ωφ2 dx≤(b−a)2∫Ω∥∇φ∥2 dx.\int_\Omega \varphi^2\,dx \le (b-a)^2\int_\Omega \|\nabla\varphi\|^2\,dx.

The constant is independent of the function, and the domain need not be bounded in directions orthogonal to the slab normal. This is the smooth-function part of Hunter's Theorem 4.9: the fundamental theorem of calculus along normal lines, Cauchy–Schwarz, and Fubini give the estimate. It is independent of the Sobolev completion and is intended to extend to that completion by continuity. When the domain is empty both integrals vanish; otherwise its containment implies a<ba<b.

Preamble
import Definitions.Def_HunterPDE_Elliptic_H10

open MeasureTheory
open scoped ContDiff
Formal statement
theorem HunterPDE.Elliptic.smooth_slab_poincare {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩ : IsOpen Ω)
    (e : EuclideanSpace ℝ (Fin n)) (he : ‖e‖ = 1) (a b : ℝ)
    (hab : ∀ x ∈ Ω, a < inner ℝ x e ∧ inner ℝ x e < b)
    (φ : EuclideanSpace ℝ (Fin n) → ℝ) (hφ : ContDiff ℝ ∞ φ)
    (hc : HasCompactSupport φ) (hs : tsupport φ ⊆ Ω) :
    ∫ x in Ω, φ x ^ 2 ≤ (b-a)^2 * ∫ x in Ω, ‖gradient φ x‖ ^ 2 := by sorry
Source
John K. Hunter, Notes on Partial Differential Equations (revised 6/18/2014), p. 98, Theorem 4.9, smooth-function estimate in the proof. https://www.math.ucdavis.edu/~hunter/pdes/ch4.pdf

View graph