Product Rule for Weak Directional Derivatives

This is the product rule for a weak directional derivative with a compactly supported $C^1$ multiplier.

Let $E$ be a finite-dimensional real inner-product space equipped with its Borel measurable structure. Let $f,g:E\to\mathbb{R}$ and $v\in E$. Assume HasWeakDerivAlong f g v, meaning that $g$ is the weak derivative of $f$ in direction $v$. Let $\chi:E\to\mathbb{R}$ be $C^1$ and compactly supported.

Then the product $\chi f$ has weak directional derivative

Here $D\chi(x)[v]$ is represented by fderiv ℝ χ x v. The result is a general weak-calculus lemma for localized test functions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem HasWeakDerivAlong.mul_contDiff {f g : E → ℝ} {v : E} (h : HasWeakDerivAlong f g v)
    {χ : E → ℝ} (hχ : ContDiff ℝ 1 χ) (hχc : HasCompactSupport χ) :
    HasWeakDerivAlong (fun x => χ x * f x) (fun x => χ x * g x + fderiv ℝ χ x v * f x) v

Module navigation

Module: Analysis/WeakDerivative/Basic.

Previous: hasWeakDerivAlong_of_lipschitz · Next: HasWeakDerivAlong.congr_ae.

Source excerpt, lines 113–115 · Frozen source 408915f.