The potential estimate behind the Poincaré–Wirtinger inequality

This file proves the pointwise estimate that controls the oscillation of a C¹ function about its mean by a Riesz potential of its derivative. Let Ω be an open subset of a finite-dimensional real normed space E of dimension n, star-convex about x and contained in closedBall x D, let μ be an additive Haar measure, and let u be C¹ on Ω. Then

∫⁻ y in Ω, ‖u x - u y‖ₑ ∂μ ≤ D ^ n / n * ∫⁻ y in Ω, ‖Du y‖ₑ * ‖x - y‖ₑ ^ (1 - n) ∂μ,

and consequently, for every S ⊆ Ω of positive measure,

‖u x - ⨍ y in S, u y ∂μ‖ₑ ≤ D ^ n / (n μ(S)) * ∫⁻ y in Ω, ‖Du y‖ₑ * ‖x - y‖ₑ ^ (1 - n) ∂μ.

For a bounded convex open Ω and x ∈ Ω one may take D = diam Ω; this is Gilbarg–Trudinger, Lemma 7.16. Integrating the right-hand side in x and bounding the Riesz potential y ↦ ‖x - y‖ ^ (1 - n) in Lᵖ yields the Poincaré–Wirtinger inequality.

The statements use lower Lebesgue integrals, so no integrability of the derivative or of the kernel is assumed.

Main declarations

• TauCeti.setLIntegral_closedBall_lintegral_segment_le: integrating a function along the segments from x to the points of closedBall x D gives at most D ^ n / n times its Riesz potential at x.
• TauCeti.setLIntegral_enorm_sub_le_of_starConvex: the integrated oscillation bound.
• TauCeti.enorm_sub_setAverage_le_of_starConvex: the bound on the deviation from the mean over any subset of positive measure.
• TauCeti.enorm_sub_setAverage_le_of_convex: the form for convex sets with D = diam Ω.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Lemma 7.16.

theorem TauCeti.lintegral_comp_add_smul_sub_mul_ite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (g : E → ENNReal) (x : E) (D : ℝ) {t : ℝ} (ht : 0 < t) : ∫⁻ (y : E), g (x + t • (y - x)) * if ‖x - y‖ ≤ D then ENNReal.ofReal ‖x - y‖ else 0 ∂μ = ∫⁻ (w : E), ENNReal.ofReal (t ^ (-↑(Module.finrank ℝ E) - 1)) * (g w * if ‖x - w‖ ≤ t * D then ENNReal.ofReal ‖x - w‖ else 0) ∂μ

The substitution w = x + t • (y - x), of Jacobian t ^ n, in the integral over y ∈ closedBall x D of g at the point of parameter t on the segment from x to y, weighted by the length of the segment.

theorem TauCeti.setLIntegral_closedBall_lintegral_segment_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {g : E → ENNReal} (hg : Measurable g) (x : E) (D : ℝ) : ∫⁻ (y : E) in Metric.closedBall x D, (∫⁻ (t : ℝ) in Set.Ioc 0 1, g (x + t • (y - x))) * ‖x - y‖ₑ ∂μ ≤ ENNReal.ofReal (D ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E)) * ∫⁻ (w : E), g w * ‖x - w‖ₑ ^ (1 - ↑(Module.finrank ℝ E)) ∂μ

Averaging along segments produces the Riesz potential. Integrating a function g along the segments from x to the points y of closedBall x D, weighted by their lengths, gives at most D ^ n / n times the Riesz potential ∫ w, g w * ‖x - w‖ ^ (1 - n), where n is the dimension of the space.

theorem TauCeti.setLIntegral_enorm_sub_le_of_starConvex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → F} {Ω : Set E} {x : E} {D : ℝ} (hΩ : IsOpen Ω) (hu : ContDiffOn ℝ 1 u Ω) (hx : StarConvex ℝ x Ω) (hD : Ω ⊆ Metric.closedBall x D) : ∫⁻ (y : E) in Ω, ‖u x - u y‖ₑ ∂μ ≤ ENNReal.ofReal (D ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E)) * ∫⁻ (y : E) in Ω, ‖fderiv ℝ u y‖ₑ * ‖x - y‖ₑ ^ (1 - ↑(Module.finrank ℝ E)) ∂μ

The integrated oscillation bound. If u is C¹ on an open set Ω which is star-convex about x and contained in closedBall x D, then the integral over Ω of ‖u x - u y‖ is bounded by D ^ n / n times the Riesz potential at x of the norm of the derivative of u, where n is the dimension of the space.

theorem TauCeti.enorm_sub_setAverage_le_of_starConvex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → F} {Ω S : Set E} {x : E} {D : ℝ} [CompleteSpace F] (hΩ : IsOpen Ω) (hu : ContDiffOn ℝ 1 u Ω) (hx : StarConvex ℝ x Ω) (hD : Ω ⊆ Metric.closedBall x D) (hS : S ⊆ Ω) (hS₀ : μ S ≠ 0) : ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ≤ ENNReal.ofReal (D ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E)) / μ S * ∫⁻ (y : E) in Ω, ‖fderiv ℝ u y‖ₑ * ‖x - y‖ₑ ^ (1 - ↑(Module.finrank ℝ E)) ∂μ

The potential estimate for the mean. If u is C¹ on an open set Ω which is star-convex about x and contained in closedBall x D, then for every S ⊆ Ω of positive measure the deviation of u x from the mean of u over S is bounded by D ^ n / (n μ(S)) times the Riesz potential at x of the norm of the derivative of u, where n is the dimension of the space.

theorem TauCeti.enorm_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] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → F} {Ω S : Set E} {x : E} [CompleteSpace F] (hΩ : IsOpen Ω) (hΩc : Convex ℝ Ω) (hb : Bornology.IsBounded Ω) (hu : ContDiffOn ℝ 1 u Ω) (hx : x ∈ Ω) (hS : S ⊆ Ω) (hS₀ : μ S ≠ 0) : ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ≤ ENNReal.ofReal (Metric.diam Ω ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E)) / μ S * ∫⁻ (y : E) in Ω, ‖fderiv ℝ u y‖ₑ * ‖x - y‖ₑ ^ (1 - ↑(Module.finrank ℝ E)) ∂μ

Gilbarg–Trudinger, Lemma 7.16. If u is C¹ on a bounded convex open set Ω and x ∈ Ω, then for every S ⊆ Ω of positive measure the deviation of u x from the mean of u over S is bounded by (diam Ω) ^ n / (n μ(S)) times the Riesz potential at x of the norm of the derivative of u, where n is the dimension of the space.