Weak partial derivatives of $c\,(f-g)$

Proved

JHolomorphic.HasWeakPartialsOn.smul_sub

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

sobolev-spacesweak-derivatives

Let $E$ be a real normed space and $U\subseteq\mathbb{C}$ . Suppose $f_s,f_t$ are weak partial derivatives of $f:\mathbb{C}\to E$ on $U$ and $g_s,g_t$ are weak partial derivatives of $g$ on $U$ , and that $f,f_s,f_t,g,g_s,g_t$ are integrable on every compact subset of $U$ . Then for every $c\in\mathbb{R}$ the functions $c\,(f_s-g_s)$ and $c\,(f_t-g_t)$ are weak partial derivatives of $c\,(f-g)$ on $U$ . This is the linearity of weak differentiation, in the form used for difference quotients.

Formalization Note Weak partial derivatives are HasWeakPartialsOn, tested against real $C^\infty$ functions with compact support in the given open set; the first weak partial is the derivative in the direction $1$ and the second in the direction $i$ .

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open MeasureTheory Metric
open scoped ContDiff

/-- Weak partial derivatives of `c • (f - g)`: if `f` and `g` have weak partials on `U` and all six
functions are integrable on compact subsets of `U`, then `c • (f - g)` has weak partials
`c • (fₛ - gₛ)` and `c • (fₜ - gₜ)` on `U`. -/
theorem HasWeakPartialsOn.smul_sub {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {U : Set ℂ} {f fs ft g gs gt : ℂ → E} (hf : HasWeakPartialsOn U f fs ft)
    (hg : HasWeakPartialsOn U g gs gt)
    (hfi : ∀ K ⊆ U, IsCompact K → IntegrableOn f K ∧ IntegrableOn fs K ∧ IntegrableOn ft K)
    (hgi : ∀ K ⊆ U, IsCompact K → IntegrableOn g K ∧ IntegrableOn gs K ∧ IntegrableOn gt K)
    (c : ℝ) :
    HasWeakPartialsOn U (fun z => c • (f z - g z)) (fun z => c • (fs z - gs z))
      (fun z => c • (ft z - gt z)) := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and Lebesgue spaces).

View graph

Weak partial derivatives of c (f−g)c\,(f-g)c(f−g)

Weak partial derivatives of $c\,(f-g)$