Chain rule for weak gradients

A C¹ function of a class with a weak gradient has a weak gradient, the derivative of the function at the class times the gradient, once the derivative is bounded. The proof mollifies the class inside the domain: on the support of a test function, the partials of the mollifications are the mollified gradient, the classical chain rule and integration by parts apply to each mollification, and both sides pass to the limit. The function side uses the Lipschitz bound on f; the gradient side uses a subsequence converging almost everywhere and dominated convergence for the continuous, bounded derivative.

The positive part follows from the chain rule applied to the C¹ functions t ↦ √((t⁺)² + ε²) - ε, which increase to t⁺ as ε decreases to 0 with derivatives bounded by one, and from dominated convergence once more. The weak gradient of u⁺ is the gradient of u where u > 0 and zero elsewhere. Splitting u - c into positive and negative parts and using uniqueness of the weak gradient, the gradient vanishes almost everywhere on every level set.

Integrability is asked for locally on the domain throughout, which is the class the sources state the results for, and the domain is open.

Main declarations

• EllipticPdes.Embedding.hasWeakGradOn_comp: the chain rule for a C¹ function with bounded derivative.
• EllipticPdes.Embedding.hasWeakGradOn_posPart: the weak gradient of the positive part.
• EllipticPdes.Embedding.hasWeakGradOn_posPart_sub_const: the weak gradient of (u - c)⁺.
• EllipticPdes.Embedding.ae_eq_zero_of_eq_const_of_hasWeakGradOn: the weak gradient vanishes almost everywhere on a level set.

References

D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §7.4 Lemma 7.5 (p. 151), Lemma 7.6 and Lemma 7.7 (p. 152); L. C. Evans, Partial Differential Equations (2nd ed.), §5.10 Problems 17 and 18 (p. 308).

Integrability against a test factor

theorem EllipticPdes.Embedding.integrable_mul_of_locallyIntegrableOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous h) (hcs : HasCompactSupport h) (hs : tsupport h ⊆ Ω) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => u x * h x) MeasureTheory.volume

Integrability against a test factor. A locally integrable class on a set, times a continuous function with compact support inside the set, is integrable on the whole space.

theorem EllipticPdes.Embedding.integrable_bdd_mul_mul_bdd {d : ℕ} {a b c : EuclideanSpace ℝ (Fin d) → ℝ} (ha : MeasureTheory.AEStronglyMeasurable a MeasureTheory.volume) {A : ℝ} (hA : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖a x‖ ≤ A) (hb : MeasureTheory.Integrable b MeasureTheory.volume) (hc : MeasureTheory.AEStronglyMeasurable c MeasureTheory.volume) {C : ℝ} (hC : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖c x‖ ≤ C) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => a x * b x * c x) MeasureTheory.volume

Product of two bounded factors and an integrable one.

theorem EllipticPdes.Embedding.integrable_comp_mul_of_lipschitz {d : ℕ} {w : EuclideanSpace ℝ (Fin d) → ℝ} (hw : MeasureTheory.Integrable w MeasureTheory.volume) {f : ℝ → ℝ} {M : NNReal} (hf : LipschitzWith M f) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous h) (hcs : HasCompactSupport h) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => f (w x) * h x) MeasureTheory.volume

Lipschitz function of an integrable class against a test factor. The product with a continuous compactly supported factor is integrable.

Elementary closure properties with local integrability

theorem EllipticPdes.Embedding.HasWeakGradOn.neg {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (h : HasWeakGradOn B u g) : HasWeakGradOn B (fun (x : EuclideanSpace ℝ (Fin d)) => -u x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => -g k x

Negation of a weak gradient.

theorem EllipticPdes.Embedding.HasWeakGradOn.add_of_locallyIntegrableOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u v : EuclideanSpace ℝ (Fin d) → ℝ} {g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hv : MeasureTheory.LocallyIntegrableOn v Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hh : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (h k) Ω MeasureTheory.volume) (hU : HasWeakGradOn Ω u g) (hV : HasWeakGradOn Ω v h) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => u x + v x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => g k x + h k x

Additivity of a weak gradient, with local integrability on an open set.

theorem EllipticPdes.Embedding.hasWeakGradOn_sub_const {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) (c : ℝ) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => u x - c) g

Subtracting a constant leaves the weak gradient unchanged.

theorem EllipticPdes.Embedding.hasWeakGradOn_unique_ae_of_locallyIntegrableOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g g' : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hg' : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g' k) Ω MeasureTheory.volume) (h : HasWeakGradOn Ω u g) (h' : HasWeakGradOn Ω u g') (k : Fin d) : g k =ᵐ[MeasureTheory.volume.restrict Ω] g' k

Uniqueness of the weak gradient on an open set, with local integrability.

The chain rule

theorem EllipticPdes.Embedding.hasWeakGradOn_comp {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) {f : ℝ → ℝ} (hf : ContDiff ℝ 1 f) {M : NNReal} (hM : ∀ (t : ℝ), ‖deriv f t‖₊ ≤ M) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => f (u x)) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => deriv f (u x) * g k x

Chain rule for weak gradients (Gilbarg and Trudinger Lemma 7.5, Evans §5.10 Problem 17). A C¹ function with bounded derivative, composed with a class with a locally integrable weak gradient on an open set, has the weak gradient f'(u) ∇u there.

The positive part

noncomputable def EllipticPdes.Embedding.posPartApprox (ε t : ℝ) : ℝ

The C¹ approximation of the positive part, √((t⁺)² + ε²) - ε.

Equations

• EllipticPdes.Embedding.posPartApprox ε t = √(max t 0 ^ 2 + ε ^ 2) - ε

theorem EllipticPdes.Embedding.hasDerivAt_max_sq (t : ℝ) : HasDerivAt (fun (s : ℝ) => max s 0 ^ 2) (2 * max t 0) t

The square of the positive part is differentiable, with derivative 2 t⁺.

theorem EllipticPdes.Embedding.contDiff_max_sq : ContDiff ℝ 1 fun (s : ℝ) => max s 0 ^ 2

The square of the positive part is C¹.

theorem EllipticPdes.Embedding.posPartApprox_arg_pos {ε : ℝ} (hε : ε ≠ 0) (t : ℝ) : 0 < max t 0 ^ 2 + ε ^ 2

The argument of the square root in posPartApprox is positive.

theorem EllipticPdes.Embedding.hasDerivAt_posPartApprox {ε : ℝ} (hε : ε ≠ 0) (t : ℝ) : HasDerivAt (posPartApprox ε) (2 * max t 0 / (2 * √(max t 0 ^ 2 + ε ^ 2))) t

The derivative of the approximation.

theorem EllipticPdes.Embedding.contDiff_posPartApprox {ε : ℝ} (hε : ε ≠ 0) : ContDiff ℝ 1 (posPartApprox ε)

The approximation is C¹.

theorem EllipticPdes.Embedding.deriv_posPartApprox {ε : ℝ} (hε : ε ≠ 0) (t : ℝ) : deriv (posPartApprox ε) t = max t 0 / √(max t 0 ^ 2 + ε ^ 2)

The derivative of the approximation, in closed form.

theorem EllipticPdes.Embedding.deriv_posPartApprox_mem {ε : ℝ} (hε : ε ≠ 0) (t : ℝ) : 0 ≤ deriv (posPartApprox ε) t ∧ deriv (posPartApprox ε) t ≤ 1

The derivative of the approximation lies in [0, 1].

theorem EllipticPdes.Embedding.nnnorm_deriv_posPartApprox_le {ε : ℝ} (hε : ε ≠ 0) (t : ℝ) : ‖deriv (posPartApprox ε) t‖₊ ≤ 1

The derivative of the approximation has nonnegative norm at most one.

theorem EllipticPdes.Embedding.posPartApprox_mem {ε : ℝ} (hε : 0 ≤ ε) (t : ℝ) : 0 ≤ posPartApprox ε t ∧ posPartApprox ε t ≤ max t 0

The approximation lies between 0 and the positive part.

theorem EllipticPdes.Embedding.tendsto_posPartApprox (t : ℝ) : Filter.Tendsto (fun (ε : ℝ) => posPartApprox ε t) (nhds 0) (nhds (max t 0))

The approximation tends to the positive part as ε → 0.

theorem EllipticPdes.Embedding.tendsto_deriv_posPartApprox (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => deriv (posPartApprox (1 / (↑n + 1))) t) Filter.atTop (nhds (if 0 < t then 1 else 0))

The derivative of the approximation tends to the indicator of {t > 0} as ε → 0 along positive values.

theorem EllipticPdes.Embedding.hasWeakGradOn_posPart {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => max (u x) 0) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => if 0 < u x then g k x else 0

Weak gradient of the positive part (Gilbarg and Trudinger Lemma 7.6, Evans §5.10 Problem 18). On an open set, u⁺ = max u 0 has the weak gradient ∇u where u > 0 and 0 elsewhere.

theorem EllipticPdes.Embedding.hasWeakGradOn_posPart_sub_const {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) (c : ℝ) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => max (u x - c) 0) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => if c < u x then g k x else 0

Weak gradient of (u - c)⁺.

theorem EllipticPdes.Embedding.locallyIntegrableOn_of_norm_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {f g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : MeasureTheory.LocallyIntegrableOn g Ω MeasureTheory.volume) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict Ω)) (h : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖f x‖ ≤ ‖g x‖) : MeasureTheory.LocallyIntegrableOn f Ω MeasureTheory.volume

Local integrability by domination.

theorem EllipticPdes.Embedding.aestronglyMeasurable_ite_lt {d : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} {u w : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u μ) (hw : MeasureTheory.AEStronglyMeasurable w μ) (c : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin d)) => if c < u x then w x else 0) μ

Measurability of a truncation.

theorem EllipticPdes.Embedding.locallyIntegrableOn_ite_lt {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u w : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict Ω)) (hw : MeasureTheory.LocallyIntegrableOn w Ω MeasureTheory.volume) (c : ℝ) : MeasureTheory.LocallyIntegrableOn (fun (x : EuclideanSpace ℝ (Fin d)) => if c < u x then w x else 0) Ω MeasureTheory.volume

Local integrability of a truncated gradient.

theorem EllipticPdes.Embedding.locallyIntegrableOn_posPart_sub_const {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (c : ℝ) : MeasureTheory.LocallyIntegrableOn (fun (x : EuclideanSpace ℝ (Fin d)) => max (u x - c) 0) Ω MeasureTheory.volume

Local integrability of the positive part of u - c.

theorem EllipticPdes.Embedding.ae_eq_zero_of_eq_const_of_hasWeakGradOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) (c : ℝ) (k : Fin d) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, u x = c → g k x = 0

Vanishing of the weak gradient on level sets (Gilbarg and Trudinger Lemma 7.7). On an open set, the weak gradient of u is zero almost everywhere on {u = c}.

theorem EllipticPdes.Embedding.hasWeakGradOn_negPart {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => min (u x) 0) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => if u x < 0 then g k x else 0

Weak gradient of the negative part (Gilbarg and Trudinger Lemma 7.6, second clause). u⁻ = min u 0 has the weak gradient ∇u where u < 0 and 0 elsewhere.

theorem EllipticPdes.Embedding.locallyIntegrableOn_posPart {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) : MeasureTheory.LocallyIntegrableOn (fun (x : EuclideanSpace ℝ (Fin d)) => max (u x) 0) Ω MeasureTheory.volume

Local integrability of the positive part.

theorem EllipticPdes.Embedding.hasWeakGradOn_abs {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u Ω MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.LocallyIntegrableOn (g k) Ω MeasureTheory.volume) (hwg : HasWeakGradOn Ω u g) : HasWeakGradOn Ω (fun (x : EuclideanSpace ℝ (Fin d)) => |u x|) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => if 0 < u x then g k x else if u x < 0 then -g k x else 0

Weak gradient of the absolute value (Gilbarg and Trudinger Lemma 7.6, third clause). |u| has the weak gradient ∇u where u > 0, -∇u where u < 0, and 0 elsewhere.