Scalar multiplication preserves weak derivatives

Proved

HunterPDE.Shared.HasWeakDeriv.smul

by Mazecto · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisweak-derivatives

If $g$ is the weak derivative of $f$ of multi-index $\alpha$ on a subset $\Omega$ of Euclidean space, then $cg$ is the same weak derivative of $cf$ for every real scalar $c$ . Both local integrability conditions and the test-function identity are preserved. No openness assumption on $\Omega$ is required.

Preamble

import Definitions.Def_HunterPDE_Shared_WeakDeriv
import Mathlib.MeasureTheory.Integral.Bochner.Set

open MeasureTheory HunterPDE.Shared
set_option autoImplicit false

Formal statement

theorem HunterPDE.Shared.HasWeakDeriv.smul {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))}
    {α : Fin n → ℕ} {f g : EuclideanSpace ℝ (Fin n) → ℝ}
    (h : HasWeakDeriv Ω α f g) (c : ℝ) :
    HasWeakDeriv Ω α (c • f) (c • g) := by sorry

Source

J. K. Hunter, Notes on Partial Differential Equations (2014), https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, Definitions 3.1–3.2, pp.47–48; linearity of the defining integral identity.

View graph