Constancy of a class with zero weak gradient on a connected open set

Evans states this as Problem 11 of Chapter 5 and uses it in the proof of the Poincaré inequality of §5.8.1, where the limit of the renormalised sequence has zero weak gradient and must be constant to contradict its unit norm. Guo's Poincaré inequality is the W_0^{1,p} form and does not need it.

The proof runs in three steps. On a ball whose double lies in the set, the mollifications of the class have zero classical gradient, since the mollified weak gradient is the gradient of the mollification, so each is constant on the ball, and an L¹ limit of constants on a set of positive finite measure is constant, the constants spanning a closed line in L¹. The constant attached to each ball is locally constant in the centre, two overlapping balls sharing it on their intersection, so on a preconnected set it is one constant. A countable subcover of the set by such balls then puts the class equal to that constant almost everywhere.

Main declarations

• EllipticPdes.Embedding.ae_const_of_tendsto_ae_const: an L¹ limit of almost-everywhere constant functions is almost-everywhere constant.
• EllipticPdes.Embedding.ae_const_on_ball_of_hasWeakGradOn_zero: the class is constant on every ball whose double lies in the set.
• EllipticPdes.Embedding.ae_const_of_hasWeakGradOn_zero: the class is constant on a preconnected open set.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.8.1 Theorem 1 (p. 290) and Chapter 5 Problem 11.

The limit of constants

theorem EllipticPdes.Embedding.ae_const_of_tendsto_ae_const {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBfin : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict B)) {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.MemLp f 1 (MeasureTheory.volume.restrict B)) {fn : ℕ → EuclideanSpace ℝ (Fin d) → ℝ} {c : ℕ → ℝ} (hfn : ∀ (n : ℕ), fn n =ᵐ[MeasureTheory.volume.restrict B] fun (x : EuclideanSpace ℝ (Fin d)) => c n) (htend : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fn n - f) 1 (MeasureTheory.volume.restrict B)) Filter.atTop (nhds 0)) : ∃ (c₀ : ℝ), f =ᵐ[MeasureTheory.volume.restrict B] fun (x : EuclideanSpace ℝ (Fin d)) => c₀

Constancy of an L¹ limit of constants. On a set of positive finite measure the constants span a line in L¹, which is closed, so a limit of almost-everywhere constant functions is almost-everywhere constant.

Constancy on a ball

theorem EllipticPdes.Embedding.ae_const_on_ball_of_hasWeakGradOn_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u fun (x : Fin d) (x_1 : EuclideanSpace ℝ (Fin d)) => 0) {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hr : 0 < r) (hx : Metric.closedBall x (2 * r) ⊆ Ω) : ∃ (c : ℝ), u =ᵐ[MeasureTheory.volume.restrict (Metric.ball x r)] fun (x : EuclideanSpace ℝ (Fin d)) => c

Constancy on a ball whose double lies in the set. The mollifications of the class have zero gradient on the ball, since the mollified weak gradient is the classical gradient of the mollification, so each is constant there; they converge to the class in L¹, and the limit of constants is constant.

Constancy on a preconnected open set

theorem EllipticPdes.Embedding.ae_const_of_hasWeakGradOn_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩconn : IsPreconnected Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u fun (x : Fin d) (x_1 : EuclideanSpace ℝ (Fin d)) => 0) : ∃ (c : ℝ), u =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => c

Constancy of a class with zero weak gradient on a preconnected open set (Evans, Chapter 5 Problem 11). The constant attached to each ball whose double lies in the set is locally constant in the centre, two overlapping balls sharing it on their intersection, so it is one constant on the set; a countable subcover by such balls then puts the class equal to it almost everywhere.