The product rule for weak derivatives

A weak derivative is additive and commutes with scalars (TauCeti.HasWeakLineDerivOn.add, TauCeti.HasWeakLineDerivOn.const_smul), but Lane A of the PDE roadmap needs one more algebraic rule before it can localize: multiplication by a variable smooth factor. This file proves it. For a smooth ψ : E → ℝ and a weakly differentiable u,

∂_v (ψ u) = ψ ∂_v u + (∂_v ψ) u

on Ω, in the weak sense of TauCeti.HasWeakLineDerivOn.

The proof is the one-line distributional computation. Testing ψ u against ∂_v φ is the same as testing u against ψ ∂_v φ = ∂_v (ψ φ) − (∂_v ψ) φ, and ψ φ is again a test function on Ω, because multiplying by a smooth function neither enlarges a support nor destroys smoothness. So the defining identity for u applies to it, and the leftover term (∂_v ψ) φ is the second summand of the Leibniz formula. No smoothness of u is used, and no boundary hypothesis on Ω: ψ φ is compactly supported inside Ω, so no boundary term appears.

Smoothness of ψ is more than the identity needs — C¹ would do — but it is what makes ψ φ a member of Mathlib's TestFunction type, whose smoothness order is ∞, and it is what every intended application supplies (cutoffs are built from ContDiffBump).

Why this is the localization tool

ψ will be a cutoff. Multiplying by one is how a global statement about W^{k,p}(Ω) is reduced to a local one: it is the first step of the Meyers–Serrin H = W density theorem and of the extension operator (Lane A.2 and A.6 of TauCetiRoadmap/PDE/README.md), and it is what turns an interior estimate into an estimate on a compactly contained subdomain (Lane E.20). The second summand (∂_v ψ) u is exactly the error such an argument has to absorb, so having it with an explicit, non-asymptotic formula is the point.

Main declarations

• TauCeti.HasWeakLineDerivOn.contDiff_smul: the Leibniz rule in a direction v.
• TauCeti.HasWeakFDerivOn.contDiff_smul: its Fréchet form, with the rank-one correction (fderiv ℝ ψ x).smulRight (u x).
• TauCeti.HasWeakFDerivOn.contDiff_smul_gradient: the form consumed by TauCeti.W1p, where a weak derivative of a scalar function is recorded by its Riesz representative and the rule reads ∇(ψ u) = ψ ∇u + u ∇ψ.

References

L. C. Evans, Partial Differential Equations, §5.2.3, Theorem 1(iv).

theorem TauCeti.HasWeakLineDerivOn.contDiff_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [LocallyCompactSpace E] {Ω : TopologicalSpace.Opens E} {v : E} {μ : MeasureTheory.Measure E} {u u' : E → F} {ψ : E → ℝ} (h : HasWeakLineDerivOn μ Ω u u' v) (hψ : ContDiff ℝ (↑⊤) ψ) : HasWeakLineDerivOn μ Ω (fun (x : E) => ψ x • u x) (fun (x : E) => ψ x • u' x + (fderiv ℝ ψ x) v • u x) v

The Leibniz rule for weak directional derivatives. If u' is a weak derivative of u in the direction v on Ω and ψ is smooth, then ψ u is weakly differentiable in the direction v on Ω, with derivative ψ u' + (∂_v ψ) u.

Nothing is assumed about Ω beyond openness: the test function ψ φ used in the proof is still compactly supported inside Ω, so the boundary term of the classical integration by parts is absent here just as it is in the definition.

theorem TauCeti.HasWeakFDerivOn.contDiff_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [OpensMeasurableSpace E] [LocallyCompactSpace E] {Ω : TopologicalSpace.Opens E} {μ : MeasureTheory.Measure E} {u : E → F} {ψ : E → ℝ} {U : E → E →L[ℝ] F} (h : HasWeakFDerivOn μ Ω u U) (hψ : ContDiff ℝ (↑⊤) ψ) : HasWeakFDerivOn μ Ω (fun (x : E) => ψ x • u x) fun (x : E) => ψ x • U x + (fderiv ℝ ψ x).smulRight (u x)

The Leibniz rule for weak Fréchet derivatives: D(ψ u) = ψ Du + u ⊗ Dψ, the correction being the rank-one map v ↦ (Dψ v) u.

theorem TauCeti.HasWeakFDerivOn.contDiff_smul_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {μ : MeasureTheory.Measure E} {a ψ : E → ℝ} {g : E → E} (h : HasWeakFDerivOn μ Ω a fun (x : E) => (innerSL ℝ) (g x)) (hψ : ContDiff ℝ (↑⊤) ψ) : HasWeakFDerivOn μ Ω (fun (x : E) => ψ x • a x) fun (x : E) => (innerSL ℝ) (ψ x • g x + a x • gradient ψ x)

The Leibniz rule in gradient form: ∇(ψ a) = ψ ∇a + a ∇ψ.

This is the shape TauCeti.W1p stores a weak derivative in — a scalar function together with the Riesz representative of its weak Fréchet derivative — so it is the form a multiplication operator on the Sobolev space consumes.