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

Let Ω be a bounded convex open subset of a finite-dimensional real inner product space E of dimension n, let μ be an additive Haar measure, and let S ⊆ Ω be null-measurable and have positive measure. This file proves, for 1 ≤ p < ∞ and every u ∈ W^{1,p}(Ω),

‖u - ⨍_S u‖_{Lᵖ(Ω)} ≤ μ(B(0, 1)) * (diam Ω) ^ (n + 1) / μ(S) * ‖∇u‖_{Lᵖ(Ω)},

the inequality that TauCeti.eLpNorm_sub_setAverage_le_of_convex proves, with the same constant, for C¹ functions. A weakly differentiable function need not be C¹, so the two are genuinely different statements, and it is the Sobolev one that an existence or regularity argument can use.

Subtracting the mean is not a normalisation that could be dropped: no inequality of this shape holds for the deviation from an arbitrary constant, since the nonzero constants themselves lie in W^{1,p}(Ω) with vanishing gradient.

The approximation

Test functions on Ω are dense in W^{1,p}(Ω) only after Ω is shrunk: TauCeti.W1p.restrictL_mem_closure_range_ofTestFunctionₗ approximates u on a subdomain U whose closure is a compact subset of Ω. Two limits are therefore taken.

• On a fixed such U, convex so that the C¹ inequality applies to it, the Sobolev functions satisfying the inequality form a closed set — the mean over S is a continuous functional, by Set.setIntegralLp — which contains every test function, hence their closure.
• The convex subdomains are then increased to Ω, along the exhaustion TauCeti.exists_seq_isOpen_convex_isCompact_closure_subset_iUnion_eq. The means over S ∩ U converge to the mean over S, and Fatou's lemma for the Lᵖ seminorm, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, passes the inequality to the limit. Only the measure of S ∩ U needs to be tracked, since diam U ≤ diam Ω already bounds the numerator of the constant.

Main declarations

• TauCeti.W1p.eLpNorm_value_sub_setAverage_le_of_convex: the inequality on W^{1,p}(Ω).
• TauCeti.W1p.eLpNorm_value_sub_setAverage_le_of_eq_ball: the constant on a ball of radius R is 2 ^ (n + 1) * R.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.16.
• L. C. Evans, Partial Differential Equations, Section 5.8.1.

The inequality on a relatively compact convex subdomain

The inequality on the whole domain

theorem TauCeti.W1p.eLpNorm_value_sub_setAverage_le_of_convex {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {S : Set E} (hp : p ≠ ⊤) (hconv : Convex ℝ ↑Omega) (hb : Bornology.IsBounded ↑Omega) (hSm : MeasureTheory.NullMeasurableSet S mu) (hS : S ⊆ ↑Omega) (hS0 : mu S ≠ 0) (u : ↥(W1p mu Omega p)) : MeasureTheory.eLpNorm (fun (x : E) => ↑↑(value u) x - ⨍ (y : E) in S, ↑↑(value u) y ∂mu) p (mu.restrict ↑Omega) ≤ ENNReal.ofReal (mu.real (Metric.ball 0 1) * Metric.diam ↑Omega ^ (Module.finrank ℝ E + 1) / mu.real S) * ‖gradient u‖ₑ

The Poincaré–Wirtinger inequality on W^{1,p}(Ω). Let Ω be a bounded convex open set in a finite-dimensional real inner product space of dimension n, and let S ⊆ Ω be null-measurable of positive measure. For 1 ≤ p < ∞, every u ∈ W^{1,p}(Ω) deviates from its mean over S by at most μ(B(0, 1)) * (diam Ω) ^ (n + 1) / μ(S) times the Lᵖ norm of its weak gradient.

theorem TauCeti.W1p.eLpNorm_value_sub_setAverage_le_of_eq_ball {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {c : E} {R : ℝ} (hp : p ≠ ⊤) (hR : 0 < R) (hOmega : ↑Omega = Metric.ball c R) (u : ↥(W1p mu Omega p)) : MeasureTheory.eLpNorm (fun (x : E) => ↑↑(value u) x - ⨍ (y : E) in ↑Omega, ↑↑(value u) y ∂mu) p (mu.restrict ↑Omega) ≤ ENNReal.ofReal (2 ^ (Module.finrank ℝ E + 1) * R) * ‖gradient u‖ₑ

The Poincaré–Wirtinger inequality on a ball. On a ball of radius R the constant of TauCeti.W1p.eLpNorm_value_sub_setAverage_le_of_convex is 2 ^ (n + 1) * R: the deviation of u ∈ W^{1,p}(B(c, R)) from its mean over the ball is at most 2 ^ (n + 1) * R times the Lᵖ norm of its weak gradient. The constant is proportional to R, as the scaling of both sides forces.