The Leibniz rule for the weak gradient and the weak Hessian

Let ζ be a smooth function on a finite-dimensional real inner product space. This file computes the recorded weak derivatives of any Sobolev function whose value is ζ u:

• if u, w ∈ W^{1,p}(Ω) and w = ζ u almost everywhere on Ω, then ∇w = ζ ∇u + u ∇ζ (TauCeti.Wkp.iteratedGradient_zero_ae_eq_of_value_ae_eq_mul);

• if u, w ∈ W^{2,p}(Ω) and w = ζ u almost everywhere on Ω, then the weak Hessian is

  D²w = ζ D²u + ∇ζ ⊗ ∇u + ∇u ⊗ ∇ζ + u D²ζ

  (TauCeti.Wkp.iteratedGradient_one_ae_eq_of_value_ae_eq_mul), where D²w is TauCeti.Wkp.iteratedGradient 1 w, a field of endomorphisms of E, and a ⊗ b denotes the rank-one map v ↦ ⟪a, v⟫ b. The remainder ∇ζ ⊗ ∇u + ∇u ⊗ ∇ζ + u D²ζ is at most 2 ‖∇ζ‖ ‖∇u‖ + ‖D²ζ‖ |u| pointwise in operator norm (TauCeti.norm_leibnizRemainder_le), and it vanishes off the support of ζ (TauCeti.leibnizRemainder_eq_zero_of_notMem_tsupport).

• consequently ‖D²w - ζ D²u‖ ≤ 2 c₁ ‖∇u‖ + c₂ ‖u‖ for ‖∇ζ‖ ≤ c₁, ‖D²ζ‖ ≤ c₂ (TauCeti.Wkp.norm_iteratedGradient_one_sub_toLp_le_of_value_ae_eq_mul), and for a cutoff ζ with |ζ| ≤ 1, ‖D²w‖ ≤ ‖D²u‖ + 2 c₁ ‖∇u‖ + c₂ ‖u‖ (TauCeti.Wkp.norm_iteratedGradient_one_le_of_value_ae_eq_mul).

Nothing is assumed about ζ beyond smoothness, nor about Ω beyond openness: the formulas follow from uniqueness of weak derivatives, so they hold for every w with value ζ u, however it was produced. When ζ has compact support in Ω and p < ∞, such a w exists in W^{k,p}_0(Ω) by TauCeti.Wkp.exists_mem_wkp0Submodule_value_ae_eq_mul.

Such a w also exists in W^{k,p}(Ω) whenever ζ is smooth on an open set containing the compact set closure Ω (TauCeti.Wkp.exists_value_ae_eq_mul_of_contDiffOn), for every 1 ≤ p ≤ ∞. The factor need not be smooth away from closure Ω: this is the form in which the derivatives of a coefficient field smooth on a larger domain act on Sobolev functions on a compactly contained subdomain. On an arbitrary open Ω, such a w exists in W^{k,p}(Ω) whenever ζ has compact support (TauCeti.Wkp.exists_value_ae_eq_mul_of_hasCompactSupport); the support may meet ∂Ω, which is the situation of a cutoff near a boundary point.

The Hessian formula is what localizes a second-order estimate. Writing L = ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼ, it gives L(ζ u) = ζ L u + (terms in ∇u and u), so an estimate for compactly supported functions, applied to ζ u, controls ζ D²u by ζ L u and lower-order norms of u. In that form, for ζ compactly supported with ‖∇ζ‖ ≤ M₁ and ‖D²ζ‖ ≤ M₂, the remainder is an element T of Lᵖ vanishing off the support of ζ with ‖T‖ ≤ 2 M₁ ‖∇u‖ + M₂ ‖u‖, and ‖ζ D²u‖ = ‖D²w - T‖ (TauCeti.Wkp.exists_iteratedGradient_one_ae_eq_smul_add_of_value_ae_eq_mul).

References

• L. C. Evans, Partial Differential Equations, §5.2.3, Theorem 1(iv).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, proof of Theorem 9.11.

theorem TauCeti.norm_leibnizRemainder_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (zeta : E → ℝ) (v : E) (s : ℝ) (x : E) : ‖((innerSL ℝ) (gradient zeta x)).smulRight v + ((innerSL ℝ) v).smulRight (gradient zeta x) + s • fderiv ℝ (gradient zeta) x‖ ≤ 2 * ‖gradient zeta x‖ * ‖v‖ + ‖fderiv ℝ (gradient zeta) x‖ * ‖s‖

The Leibniz remainder ∇ζ ⊗ v + v ⊗ ∇ζ + s D²ζ of the weak Hessian of ζ u (TauCeti.Wkp.iteratedGradient_one_ae_eq_of_value_ae_eq_mul, with v = ∇u and s = u) is at most 2 ‖∇ζ‖ ‖v‖ + ‖D²ζ‖ |s| in operator norm.

theorem TauCeti.leibnizRemainder_eq_zero_of_notMem_tsupport {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {zeta : E → ℝ} {x : E} (hx : x ∉ tsupport zeta) (v : E) (s : ℝ) : ((innerSL ℝ) (gradient zeta x)).smulRight v + ((innerSL ℝ) v).smulRight (gradient zeta x) + s • fderiv ℝ (gradient zeta) x = 0

The Leibniz remainder ∇ζ ⊗ v + v ⊗ ∇ζ + s D²ζ vanishes off the support of ζ.

theorem TauCeti.Wkp.iteratedGradient_zero_ae_eq_of_value_ae_eq_mul {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)] {zeta : E → ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) {u w : Wkp mu Omega p 1} (hw : ↑↑(value 1 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x * ↑↑(value 1 u) x) : ↑↑(iteratedGradient 0 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x • ↑↑(iteratedGradient 0 u) x + ↑↑(value 1 u) x • gradient zeta x

The Leibniz rule for the weak gradient. If u, w ∈ W^{1,p}(Ω) and w = ζ u almost everywhere on Ω for a smooth ζ, then ∇w = ζ ∇u + u ∇ζ almost everywhere on Ω.

theorem TauCeti.Wkp.iteratedGradient_one_ae_eq_of_value_ae_eq_mul {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)] {zeta : E → ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) {u w : Wkp mu Omega p 2} (hw : ↑↑(value 2 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x * ↑↑(value 2 u) x) : ↑↑(iteratedGradient 1 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x • ↑↑(iteratedGradient 1 u) x + ((innerSL ℝ) (gradient zeta x)).smulRight (↑↑(iteratedGradient 0 (lowerOrder 1 u)) x) + ((innerSL ℝ) (↑↑(iteratedGradient 0 (lowerOrder 1 u)) x)).smulRight (gradient zeta x) + ↑↑(value 2 u) x • fderiv ℝ (gradient zeta) x

The Leibniz rule for the weak Hessian. If u, w ∈ W^{2,p}(Ω) and w = ζ u almost everywhere on Ω for a smooth ζ, then almost everywhere on Ω

D²w = ζ D²u + ∇ζ ⊗ ∇u + ∇u ⊗ ∇ζ + u D²ζ,

where D² is the weak Hessian TauCeti.Wkp.iteratedGradient 1, ∇u is the weak gradient TauCeti.Wkp.iteratedGradient 0 (TauCeti.Wkp.lowerOrder 1 u), and a ⊗ b is the rank-one map v ↦ ⟪a, v⟫ b.

theorem TauCeti.Wkp.norm_iteratedGradient_one_sub_toLp_le_of_value_ae_eq_mul {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)] {zeta : E → ℝ} {u w : Wkp mu Omega p 2} {c₁ c₂ : ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) (hg : ∀ (x : E), ‖gradient zeta x‖ ≤ c₁) (hh : ∀ (x : E), ‖fderiv ℝ (gradient zeta) x‖ ≤ c₂) (hzu : MeasureTheory.MemLp (fun (x : E) => zeta x • ↑↑(iteratedGradient 1 u) x) p (mu.restrict ↑Omega)) (hw : ↑↑(value 2 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x * ↑↑(value 2 u) x) : ‖iteratedGradient 1 w - MeasureTheory.MemLp.toLp (fun (x : E) => zeta x • ↑↑(iteratedGradient 1 u) x) hzu‖ ≤ 2 * c₁ * ‖iteratedGradient 0 (lowerOrder 1 u)‖ + c₂ * ‖value 2 u‖

The weak Hessian of a product, minus the principal part. If u, w ∈ W^{2,p}(Ω) and w = ζ u almost everywhere on Ω for a smooth ζ with ‖∇ζ‖ ≤ c₁ and ‖D²ζ‖ ≤ c₂, and ζ D²u ∈ Lᵖ(Ω), then

‖D²w - ζ D²u‖ ≤ 2 c₁ ‖∇u‖ + c₂ ‖u‖.

theorem TauCeti.Wkp.norm_iteratedGradient_one_le_of_value_ae_eq_mul {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)] {zeta : E → ℝ} {u w : Wkp mu Omega p 2} {c₁ c₂ : ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) (habs : ∀ (x : E), |zeta x| ≤ 1) (hg : ∀ (x : E), ‖gradient zeta x‖ ≤ c₁) (hh : ∀ (x : E), ‖fderiv ℝ (gradient zeta) x‖ ≤ c₂) (hw : ↑↑(value 2 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x * ↑↑(value 2 u) x) : ‖iteratedGradient 1 w‖ ≤ ‖iteratedGradient 1 u‖ + (2 * c₁ * ‖iteratedGradient 0 (lowerOrder 1 u)‖ + c₂ * ‖value 2 u‖)

The weak Hessian of a cutoff. If u, w ∈ W^{2,p}(Ω) and w = η u almost everywhere on Ω for a smooth η with |η| ≤ 1, ‖∇η‖ ≤ c₁ and ‖D²η‖ ≤ c₂, then

‖D²w‖ ≤ ‖D²u‖ + 2 c₁ ‖∇u‖ + c₂ ‖u‖.

theorem TauCeti.Wkp.exists_iteratedGradient_one_ae_eq_smul_add_of_value_ae_eq_mul {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)] {zeta : E → ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) (hcpt : HasCompactSupport zeta) {M₁ M₂ : ℝ} (hM₁ : ∀ (x : E), ‖gradient zeta x‖ ≤ M₁) (hM₂ : ∀ (x : E), ‖fderiv ℝ (gradient zeta) x‖ ≤ M₂) {u w : Wkp mu Omega p 2} (hw : ↑↑(value 2 w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => zeta x * ↑↑(value 2 u) x) : ∃ (T : ↥(MeasureTheory.Lp (IteratedGradient E 1) p (mu.restrict ↑Omega))), (∀ᵐ (x : E) ∂mu.restrict ↑Omega, ↑↑(iteratedGradient 1 w) x = zeta x • ↑↑(iteratedGradient 1 u) x + ↑↑T x) ∧ (∀ᵐ (x : E) ∂mu.restrict ↑Omega, x ∉ tsupport zeta → ↑↑T x = 0) ∧ ‖T‖ ≤ 2 * M₁ * ‖iteratedGradient 0 (lowerOrder 1 u)‖ + M₂ * ‖value 2 u‖ ∧ MeasureTheory.lpNorm (fun (x : E) => zeta x • ↑↑(iteratedGradient 1 u) x) p (mu.restrict ↑Omega) = ‖iteratedGradient 1 w - T‖

The Leibniz remainder of a cutoff in Lᵖ. Let ζ be smooth with compact support, ‖∇ζ‖ ≤ M₁ and ‖D²ζ‖ ≤ M₂, and let u, w ∈ W^{2,p}(Ω) with w = ζ u almost everywhere on Ω. Then D²w = ζ D²u + T for some T ∈ Lᵖ(Ω) that vanishes off the support of ζ and satisfies ‖T‖ ≤ 2 M₁ ‖∇u‖ + M₂ ‖u‖, where ∇u is the weak gradient TauCeti.Wkp.iteratedGradient 0 (TauCeti.Wkp.lowerOrder 1 u); in particular ‖ζ D²u‖_{Lᵖ(Ω)} = ‖D²w - T‖. This is the form in which the Leibniz rule TauCeti.Wkp.iteratedGradient_one_ae_eq_of_value_ae_eq_mul enters the localization of second-order estimates.

theorem TauCeti.Wkp.exists_value_ae_eq_mul_of_contDiffOn {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)] {U : Set E} (hU : IsOpen U) (hΩ : IsCompact (closure ↑Omega)) (hΩU : closure ↑Omega ⊆ U) (k : ℕ) {psi : E → ℝ} (hpsi : ContDiffOn ℝ (↑⊤) psi U) (u : Wkp mu Omega p k) : ∃ (w : Wkp mu Omega p k), ↑↑(value k w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => psi x * ↑↑(value k u) x

Smooth multiplication in W^{k,p}. Let Ω have compact closure inside an open set U. If ψ is smooth on U and u ∈ W^{k,p}(Ω), then ψ u lies in W^{k,p}(Ω): some element of W^{k,p}(Ω) has value ψ u almost everywhere on Ω.

No bound on ψ or its derivatives is assumed: they are bounded on the compact set closure Ω, which is all the proof uses.

theorem TauCeti.Wkp.exists_value_ae_eq_mul_of_hasCompactSupport {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)] (k : ℕ) {psi : E → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) (hcpt : HasCompactSupport psi) (u : Wkp mu Omega p k) : ∃ (w : Wkp mu Omega p k), ↑↑(value k w) =ᵐ[mu.restrict ↑Omega] fun (x : E) => psi x * ↑↑(value k u) x

Multiplication by a compactly supported smooth function in W^{k,p}. If ψ is smooth with compact support and u ∈ W^{k,p}(Ω), then ψ u lies in W^{k,p}(Ω): some element of W^{k,p}(Ω) has value ψ u almost everywhere on Ω. The open set Ω is arbitrary, and the support of ψ may meet ∂Ω.