The Poincaré inequality fails on the whole space

A Poincaré inequality bounds the Lᵖ seminorm of a function by the Lᵖ seminorm of its derivative, ‖u‖_p ≤ C ‖Du‖_p. Mathlib proves such an estimate in MeasureTheory.eLpNorm_le_eLpNorm_fderiv, for 1 ≤ p < n and functions supported in a fixed bounded set s, with the explicit s-dependent constant MeasureTheory.eLpNormLESNormFDerivOfLeConst ℝ μ s p p. The PDE roadmap asks for the companion fact that pins the role of that hypothesis: on the whole of a finite-dimensional space no single constant works for all compactly supported functions, so the boundedness of the support is load-bearing rather than an artefact of the proof.

The obstruction is scaling. Dilating the variable by r > 0 multiplies ‖u‖_p by r ^ (n / p) and ‖Du‖_p by r ^ (n / p - 1) (TauCeti.eLpNorm_comp_inv_smul and TauCeti.eLpNorm_fderiv_comp_inv_smul), so applying a putative inequality to the dilates of one fixed bump function forces ‖u‖_p ≤ C r⁻¹ ‖Du‖_p for every r, and letting r → ∞ makes the bump's own seminorm vanish. Note that p ≠ 0 is the only hypothesis needed: the failure is not confined to the subcritical range p < n in which the positive result lives, and includes p = ∞.

TauCeti.Analysis.Sobolev.Poincare.Slab proves the matching positive statement: bounding the support in a single direction already suffices, and the constant is then the width of the slab.

Main declarations

• TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv: no constant C satisfies ‖u‖_p ≤ C ‖Du‖_p for all compactly supported C¹ functions on a finite-dimensional real normed space with an additive Haar measure.
• TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv_euclideanSpace: the roadmap's ℝⁿ form, for Lebesgue measure on EuclideanSpace ℝ (Fin n).

theorem TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {p : ENNReal} (hp₀ : p ≠ 0) : ¬∃ (C : NNReal), ∀ (u : E → ℝ), ContDiff ℝ 1 u → HasCompactSupport u → MeasureTheory.eLpNorm u p μ ≤ ↑C * MeasureTheory.eLpNorm (fderiv ℝ u) p μ

No Poincaré inequality holds on the whole space. There is no constant C with ‖u‖_p ≤ C ‖Du‖_p for every compactly supported C¹ function u, for any p ≠ 0, including p = ∞.

Compare MeasureTheory.eLpNorm_le_eLpNorm_fderiv, which supplies such a constant once every u is supported in one fixed bounded set; the proof here shows that hypothesis cannot be dropped.

theorem TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv_euclideanSpace (n : ℕ) {p : ENNReal} (hp₀ : p ≠ 0) : ¬∃ (C : NNReal), ∀ (u : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ 1 u → HasCompactSupport u → MeasureTheory.eLpNorm u p MeasureTheory.volume ≤ ↑C * MeasureTheory.eLpNorm (fderiv ℝ u) p MeasureTheory.volume

The Poincaré inequality fails on ℝⁿ with Lebesgue measure: the roadmap's form of TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv.