Poincaré's inequality on a ball

Evans §5.8.1 Theorem 2: one constant, depending on the dimension alone at p = 2, bounds the L² distance of a class on any ball from its mean over that ball by the radius times the L² norm of its gradient. The case of the unit ball is poincare_wirtinger_ball; the general ball is taken onto it by the affine map y ↦ r y + x, under which Lebesgue measure scales by r^d, the mean is unchanged, a weak gradient picks up the factor r, and the L² seminorm on the unit ball is the seminorm on the ball scaled by r^{-d/2}, which cancels between the two sides.

The affine map is a measure-preserving map from the unit ball with Lebesgue measure to the ball with Lebesgue measure scaled by r^{-d}, which is what makes every transport a one-line application of Mathlib's MeasurePreserving API.

Main declarations

• EllipticPdes.Sobolev.affineBall: the map y ↦ r y + x.
• EllipticPdes.Sobolev.measurePreserving_affineBall: its measure transport.
• EllipticPdes.Sobolev.hasWeakGradOn_comp_affineBall: a weak gradient transported through it.
• EllipticPdes.Sobolev.poincare_ball: the inequality.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.8.1 Theorem 2 (p. 291).

The affine map of the unit ball onto a ball

def EllipticPdes.Sobolev.affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) (y : EuclideanSpace ℝ (Fin d)) : EuclideanSpace ℝ (Fin d)

The map y ↦ r y + x of the unit ball onto the ball of centre x and radius r.

Equations

• EllipticPdes.Sobolev.affineBall x r y = r • y + x

theorem EllipticPdes.Sobolev.affineBall_preimage_ball {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : affineBall x r ⁻¹' Metric.ball x r = Metric.ball 0 1

theorem EllipticPdes.Sobolev.measurableEmbedding_affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : r ≠ 0) : MeasurableEmbedding (affineBall x r)

noncomputable def EllipticPdes.Sobolev.ballScale (d : ℕ) (r : ℝ) : ENNReal

The factor by which Lebesgue measure scales under the map, as a measure multiplier.

Equations

• EllipticPdes.Sobolev.ballScale d r = ENNReal.ofReal |(r ^ d)⁻¹|

theorem EllipticPdes.Sobolev.ballScale_ne_zero {d : ℕ} {r : ℝ} (hr : 0 < r) : ballScale d r ≠ 0

theorem EllipticPdes.Sobolev.ballScale_ne_top {d : ℕ} (r : ℝ) : ballScale d r ≠ ⊤

theorem EllipticPdes.Sobolev.ballScale_toReal {d : ℕ} {r : ℝ} (hr : 0 < r) : (ballScale d r).toReal = (r ^ d)⁻¹

theorem EllipticPdes.Sobolev.measurePreserving_affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : MeasureTheory.MeasurePreserving (affineBall x r) (MeasureTheory.volume.restrict (Metric.ball 0 1)) (ballScale d r • MeasureTheory.volume.restrict (Metric.ball x r))

Measure transport of the affine map. From the unit ball with Lebesgue measure to the ball with Lebesgue measure scaled by r^{-d}.

theorem EllipticPdes.Sobolev.integral_comp_affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) (f : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball 0 1, f (affineBall x r y) = (ballScale d r).toReal * ∫ (z : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, f z

Transport of an integral over the ball.

theorem EllipticPdes.Sobolev.eLpNorm_comp_affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Metric.ball x r))) : MeasureTheory.eLpNorm (f ∘ affineBall x r) 2 (MeasureTheory.volume.restrict (Metric.ball 0 1)) = ballScale d r ^ (1 / 2).toReal * MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict (Metric.ball x r))

Transport of an L² seminorm over the ball.

theorem EllipticPdes.Sobolev.average_comp_affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) (f : EuclideanSpace ℝ (Fin d) → ℝ) : ⨍ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball 0 1, f (affineBall x r y) = ⨍ (z : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, f z

The mean over the ball is the mean over the unit ball of the transported function.

The weak gradient through the affine map

theorem EllipticPdes.Sobolev.hasWeakGradOn_comp_affineBall {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hw : Embedding.HasWeakGradOn (Metric.ball x r) u g) : Embedding.HasWeakGradOn (Metric.ball 0 1) (u ∘ affineBall x r) fun (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) => r * g k (affineBall x r y)

Weak gradient transported through the affine map, which picks up the factor r. A test function on the unit ball is pushed forward to one on the ball, whose partial derivative is r⁻¹ times the original's, and the integrals transport by the measure-preserving map.

The inequality

theorem EllipticPdes.Sobolev.poincare_ball {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin d)) (r : ℝ), 0 < r → ∀ (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ), MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Metric.ball x r)) → (∀ (k : Fin d), MeasureTheory.MemLp (g k) 2 (MeasureTheory.volume.restrict (Metric.ball x r))) → Embedding.HasWeakGradOn (Metric.ball x r) u g → (MeasureTheory.eLpNorm (fun (y : EuclideanSpace ℝ (Fin d)) => u y - ⨍ (z : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, u z) 2 (MeasureTheory.volume.restrict (Metric.ball x r))).toReal ≤ C * r * √(∑ k : Fin d, (MeasureTheory.eLpNorm (g k) 2 (MeasureTheory.volume.restrict (Metric.ball x r))).toReal ^ 2)

Poincaré's inequality on a ball (Evans §5.8.1 Theorem 2 at p = 2). One constant, depending on the dimension alone, bounds the L² distance of a class on any ball from its mean over the ball by the radius times the L² norm of its gradient.