The Poincaré inequality on a slab

This file proves the Poincaré inequality (also called the Friedrichs inequality) for C¹ functions supported in a slab: if u vanishes outside the slab {x | x i ∈ Set.Icc a b} of width b - a, then

‖u‖_p ≤ (b - a) * ‖Du‖_p

for every exponent 1 ≤ p < ∞. This is the PDE roadmap's Lane A, item 5, the estimate that W^{1,p}_0(Ω) inherits by passing to the closure of C_c^∞(Ω), and the coercivity input for the energy method of Lane D.

The constant is b - a exactly: the hypothesis a bound of this shape needs is not that Ω be bounded but only that it be bounded in one direction, and the constant depends on nothing except the width of the slab containing the support — not on the dimension, not on p, and not on the shape of the domain. TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv shows that some such hypothesis is genuinely needed: no constant works on the whole space.

The proof is the classical one-dimensional argument. Along the line through x in the direction of the i-th coordinate the function starts at 0, so the fundamental theorem of calculus gives ‖u‖ ≤ ∫ ‖∂ᵢ u‖ over the width of the slab; Hölder's inequality — in the form of the nesting L^p ⊆ L^1 of the Lᵖ scale, TauCeti.rpow_lintegral_le_measure_univ_rpow_mul — turns that into ‖u‖^p ≤ (b - a)^{p-1} ∫ ‖∂ᵢ u‖^p, and integrating in the remaining variables by Fubini gives the result. See Evans, Partial Differential Equations, Section 5.6.

Since the estimate compares the function with a single partial derivative, the one-dimensional statement TauCeti.eLpNorm_le_eLpNorm_deriv_of_support_subset_Icc is proved first for a function on ℝ and is the whole analytic content; the n-dimensional statement is Fubini plus the bound ‖Du x (eᵢ)‖ ≤ ‖Du x‖.

Main declarations

• TauCeti.eLpNorm_le_eLpNorm_deriv_of_support_subset_Icc: the one-dimensional inequality ‖g‖_p ≤ (b - a) ‖g'‖_p for a C¹ function on ℝ supported in Set.Icc a b.
• TauCeti.eLpNorm_le_eLpNorm_fderiv_of_support_subset_slab: the Poincaré inequality on EuclideanSpace ℝ (Fin (n + 1)) for a C¹ function supported in a slab of width b - a.
• TauCeti.eLpNorm_le_eLpNorm_fderiv_of_support_subset_ball: the form for a support inside a ball, with twice the radius as the constant.

The passage from a bound between the ∫⁻ ‖·‖ₑ ^ p integrals to one between the Lᵖ seminorms is generic measure theory and lives in TauCeti.MeasureTheory.Function.Lp.LIntegralRpow.

theorem TauCeti.lintegral_enorm_rpow_le_of_support_subset_Icc {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} {a b : ℝ} [NormedSpace ℝ F] {g' : ℝ → F} (hab : a ≤ b) (hg : ∀ (t : ℝ), HasDerivAt g (g' t) t) (hg' : Continuous g') (hsupp : Function.support g ⊆ Set.Icc a b) {r : ℝ} (hr : 1 ≤ r) : ∫⁻ (t : ℝ), ‖g t‖ₑ ^ r ≤ ENNReal.ofReal ((b - a) ^ r) * ∫⁻ (t : ℝ), ‖g' t‖ₑ ^ r

The one-dimensional Poincaré inequality, in the ∫⁻ form the Fubini argument below consumes: a C¹ function on ℝ that vanishes outside Set.Icc a b satisfies ∫ ‖g‖^r ≤ (b - a)^r ∫ ‖g'‖^r for every 1 ≤ r.

The two ingredients are the fundamental theorem of calculus, which bounds ‖g t‖ by the total variation ∫ ‖g'‖ over the interval, and the nesting L^r ⊆ L^1 of the Lᵖ scale on the finite measure space Set.Ioc a b, which converts that L^1 bound into an L^r one at the cost of the factor (b - a)^{r-1}.

F need not be complete.

theorem TauCeti.eLpNorm_le_eLpNorm_deriv_of_support_subset_Icc {F : Type u_1} [NormedAddCommGroup F] {g : ℝ → F} {a b : ℝ} [NormedSpace ℝ F] {g' : ℝ → F} (hab : a ≤ b) (hg : ∀ (t : ℝ), HasDerivAt g (g' t) t) (hg' : Continuous g') (hsupp : Function.support g ⊆ Set.Icc a b) {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) : MeasureTheory.eLpNorm g p MeasureTheory.volume ≤ ENNReal.ofReal (b - a) * MeasureTheory.eLpNorm g' p MeasureTheory.volume

The one-dimensional Poincaré inequality: a C¹ function on ℝ supported in an interval of length b - a obeys ‖g‖_p ≤ (b - a) ‖g'‖_p for every 1 ≤ p < ∞.

The interval hypothesis is essential; TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv shows no such bound holds uniformly over all compactly supported functions.

theorem TauCeti.eLpNorm_le_eLpNorm_fderiv_of_support_subset_slab {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {u : EuclideanSpace ℝ (Fin (n + 1)) → F} {i : Fin (n + 1)} {a b : ℝ} (hu : ContDiff ℝ 1 u) (hab : a ≤ b) (hsupp : ∀ x ∈ Function.support u, x.ofLp i ∈ Set.Icc a b) {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) : MeasureTheory.eLpNorm u p MeasureTheory.volume ≤ ENNReal.ofReal (b - a) * MeasureTheory.eLpNorm (fderiv ℝ u) p MeasureTheory.volume

The Poincaré inequality on a slab. A C¹ function on ℝ^{n+1} that vanishes outside the slab {x | x i ∈ Set.Icc a b} satisfies ‖u‖_p ≤ (b - a) ‖Du‖_p for every 1 ≤ p < ∞.

Only the width of the slab enters the constant: neither the dimension nor the exponent nor the shape of the region where u lives has any effect. In particular that region need not be bounded — being trapped between two parallel hyperplanes is enough — and the hypothesis cannot be dropped, by TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv.

This is the estimate that passes to W^{1,p}_0(Ω) by density of C_c^∞(Ω), for any Ω contained in such a slab.

theorem TauCeti.apply_mem_Icc_of_mem_ball {n : ℕ} {c x : EuclideanSpace ℝ (Fin (n + 1))} {R : ℝ} (hx : x ∈ Metric.ball c R) (i : Fin (n + 1)) : x.ofLp i ∈ Set.Icc (c.ofLp i - R) (c.ofLp i + R)

Membership in a Euclidean ball bounds every coordinate by the corresponding slab.

theorem TauCeti.eLpNorm_le_eLpNorm_fderiv_of_support_subset_ball {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {u : EuclideanSpace ℝ (Fin (n + 1)) → F} {c : EuclideanSpace ℝ (Fin (n + 1))} {R : ℝ} (hu : ContDiff ℝ 1 u) (hsupp : Function.support u ⊆ Metric.ball c R) {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) : MeasureTheory.eLpNorm u p MeasureTheory.volume ≤ ENNReal.ofReal (2 * R) * MeasureTheory.eLpNorm (fderiv ℝ u) p MeasureTheory.volume

The Poincaré inequality on a ball. A C¹ function on ℝ^{n+1} supported in a ball of radius R satisfies ‖u‖_p ≤ 2R ‖Du‖_p for every 1 ≤ p < ∞.

This is the shape the estimate takes on a bounded domain: any Ω ⊆ Metric.ball c R sits inside a slab of width 2R, so the constant may be taken to be twice the radius. It is not the optimal constant — for the ball the sharp one is smaller — but it is explicit and depends on nothing but R, as the roadmap asks.