The Poincaré–Wirtinger inequality for C¹ functions on a convex domain

Let Ω be a bounded convex open subset of a finite-dimensional real normed space E of dimension n, let μ be an additive Haar measure, and let S ⊆ Ω have positive measure. For a C¹ function u on Ω and 1 ≤ p < ∞, this file proves

‖u - ⨍ y in S, u y ∂μ‖_{Lᵖ(Ω)} ≤ C * ‖Du‖_{Lᵖ(Ω)}, where C = μ(B(0, 1)) * (diam Ω) ^ (n + 1) / μ(S).

The constant depends only on the dimension, through the Haar measure of the unit ball, on the diameter of Ω and on the measure of S, as it must: rescaling Ω by t multiplies it by t. The mean may be taken over any subset of positive measure, not only over Ω itself.

The proof bounds the deviation u x - ⨍ S u pointwise by the Riesz potential ∫_Ω ‖Du y‖ ‖x - y‖ ^ (1 - n) dy (TauCeti.enorm_sub_setAverage_le_of_convex), and bounds that potential in Lᵖ(Ω) by Schur's test (TauCeti.lintegral_rpow_lintegral_mul_le): since Ω lies in the closed ball of radius diam Ω about each of its points, the integral of the kernel ‖x - y‖ ^ (1 - n) over Ω in either variable is at most n μ(B(0, 1)) diam Ω. The constant is not sharp; Gilbarg–Trudinger obtain (μ(B(0, 1)) / μ(S)) ^ (1 - 1/n) (diam Ω) ^ n from a finer bound on the Riesz potential.

Main declarations

• TauCeti.lintegral_enorm_sub_setAverage_rpow_le_of_convex: the inequality in ∫⁻ form.
• TauCeti.eLpNorm_sub_setAverage_le_of_convex: the inequality between Lᵖ seminorms.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.16 and equation (7.45).

theorem TauCeti.lintegral_enorm_sub_setAverage_rpow_le_of_convex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → F} {Ω S : Set E} (hΩ : IsOpen Ω) (hΩc : Convex ℝ Ω) (hb : Bornology.IsBounded Ω) (hu : ContDiffOn ℝ 1 u Ω) (hS : S ⊆ Ω) (hS₀ : μ S ≠ 0) {p : ℝ} (hp : 1 ≤ p) : ∫⁻ (x : E) in Ω, ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ^ p ∂μ ≤ ENNReal.ofReal ((μ.real (Metric.ball 0 1) * Metric.diam Ω ^ (Module.finrank ℝ E + 1) / μ.real S) ^ p) * ∫⁻ (y : E) in Ω, ‖fderiv ℝ u y‖ₑ ^ p ∂μ

The Poincaré–Wirtinger inequality on a convex domain, in ∫⁻ form. If u is C¹ on a bounded convex open set Ω and S ⊆ Ω has positive measure, then for 1 ≤ p the p-th power of the deviation of u from its mean over S has integral over Ω at most C ^ p times the integral of ‖Du‖ ^ p over Ω, where C = μ(B(0, 1)) * (diam Ω) ^ (n + 1) / μ(S) and n is the dimension of the space.

theorem TauCeti.eLpNorm_sub_setAverage_le_of_convex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → F} {Ω S : Set E} (hΩ : IsOpen Ω) (hΩc : Convex ℝ Ω) (hb : Bornology.IsBounded Ω) (hu : ContDiffOn ℝ 1 u Ω) (hS : S ⊆ Ω) (hS₀ : μ S ≠ 0) {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) : MeasureTheory.eLpNorm (fun (x : E) => u x - ⨍ (y : E) in S, u y ∂μ) p (μ.restrict Ω) ≤ ENNReal.ofReal (μ.real (Metric.ball 0 1) * Metric.diam Ω ^ (Module.finrank ℝ E + 1) / μ.real S) * MeasureTheory.eLpNorm (fderiv ℝ u) p (μ.restrict Ω)

The Poincaré–Wirtinger inequality on a convex domain. If u is C¹ on a bounded convex open set Ω and S ⊆ Ω has positive measure, then for 1 ≤ p < ∞ the Lᵖ(Ω) seminorm of the deviation of u from its mean over S is at most μ(B(0, 1)) * (diam Ω) ^ (n + 1) / μ(S) times the Lᵖ(Ω) seminorm of the derivative of u, where n is the dimension of the space.