The Poincaré inequality on W^{1,p}_0(Ω)

This file proves the Poincaré inequality on W^{1,p}_0(Ω): for 1 ≤ p < ∞ and a domain Ω ⊆ ℝ^{n+1} trapped between two parallel hyperplanes at distance b - a,

‖u‖_p ≤ (b - a) ‖∇u‖_p for every u ∈ W^{1,p}_0(Ω).

This is the W^{1,p}_0 half of Lane A.5 of TauCetiRoadmap/PDE/README.md; Poincaré--Wirtinger is not proved here.

The estimate for a single test function is TauCeti.eLpNorm_le_eLpNorm_fderiv_of_support_subset_slab. The set {u | ‖u‖_p ≤ C ‖∇u‖_p} is closed and contains every test-function jet, so TauCeti.w1p0Submodule_subset_of_isClosed passes the estimate to their closure.

The slab hypothesis is load-bearing: no such inequality holds on the whole space, by TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv. So is the boundary condition: the constant function 1 on a nonempty bounded open Ω lies in W^{1,p}(Ω) with zero gradient.

Main declarations

• TauCeti.W1p.norm_value_le_mul_norm_gradient_of_subset_slab: Poincaré on a slab-contained domain.
• TauCeti.W1p.norm_value_le_mul_norm_gradient_of_subset_ball: the bounded-ball corollary.

References

The W^{1,p}_0 half of Lane A.5 of TauCetiRoadmap/PDE/README.md; L. C. Evans, Partial Differential Equations, Sections 5.2 and 5.6.

theorem TauCeti.W1p.norm_value_le_mul_norm_gradient_of_subset_slab {n : ℕ} {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin (n + 1)))} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {i : Fin (n + 1)} {a b : ℝ} (hab : a ≤ b) (hOmega : ∀ x ∈ ↑Omega, x.ofLp i ∈ Set.Icc a b) {u : ↥(W1p MeasureTheory.volume Omega p)} (hu : u ∈ w1p0Submodule MeasureTheory.volume Omega p) : ‖value u‖ ≤ (b - a) * ‖gradient u‖

The Poincaré inequality on W^{1,p}_0(Ω). If 1 ≤ p < ∞ and the domain Ω ⊆ ℝ^{n+1} is trapped between the hyperplanes xᵢ = a and xᵢ = b, then every u ∈ W^{1,p}_0(Ω) satisfies ‖u‖_p ≤ (b - a) ‖∇u‖_p.

Only the width of the slab enters, so Ω need not be bounded; boundedness in one direction is enough.

theorem TauCeti.W1p.norm_value_le_mul_norm_gradient_of_subset_ball {n : ℕ} {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin (n + 1)))} {p : ENNReal} [Fact (1 ≤ p)] {c : EuclideanSpace ℝ (Fin (n + 1))} (hp : p ≠ ⊤) {R : ℝ} (hOmega : ↑Omega ⊆ Metric.ball c R) {u : ↥(W1p MeasureTheory.volume Omega p)} (hu : u ∈ w1p0Submodule MeasureTheory.volume Omega p) : ‖value u‖ ≤ 2 * R * ‖gradient u‖

The Poincaré inequality on W^{1,p}_0(Ω) for a bounded domain. If 1 ≤ p < ∞ and Ω ⊆ ℝ^{n+1} is contained in a ball of radius R, then ‖u‖_p ≤ 2R ‖∇u‖_p for every u ∈ W^{1,p}_0(Ω).

The constant 2R is not sharp, but it is explicit and independent of the centre.