Prove2Me

Product rule for weak partial derivatives with a C1C^1 real factor

Proved
JHolomorphic.HasWeakPartialsOn.smul_left

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

sobolev-spacesweak-derivatives

Let EE be a finite-dimensional real normed space, U⊆CU\subseteq\mathbb{C} open, and let w:C→Ew:\mathbb{C}\to E have weak partial derivatives ws,wtw_s,w_t on UU, with w,ws,wtw,w_s,w_t integrable on every compact subset of UU. If β:C→R\beta:\mathbb{C}\to\mathbb{R} is C1C^1, then βw\beta w has weak partial derivatives on UU given by

∂s(βw)=(∂sβ) w+β ws,∂t(βw)=(∂tβ) w+β wt.\partial_s(\beta w)=(\partial_s\beta)\,w+\beta\,w_s,\qquad \partial_t(\beta w)=(\partial_t\beta)\,w+\beta\,w_t.

This is the weak Leibniz rule for multiplication by a smooth cutoff.

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

Preamble
import Definitions.Def_JHolomorphic_Setting
Formal statement
namespace JHolomorphic

open MeasureTheory Metric
open scoped ContDiff

/-- Product rule for weak partial derivatives with a real `C¹` factor: if `w` has weak partials
`wₛ`, `wₜ` on the open set `U`, all integrable on compact subsets of `U`, and `β : ℂ → ℝ` is `C¹`,
then `β • w` has weak partials `(∂ₛβ) w + β wₛ` and `(∂ₜβ) w + β wₜ` on `U`. -/
theorem HasWeakPartialsOn.smul_left {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {U : Set ℂ} (hU : IsOpen U) {β : ℂ → ℝ} (hβ : ContDiff ℝ 1 β)
    {w ws wt : ℂ → E} (hw : HasWeakPartialsOn U w ws wt)
    (hint : ∀ K ⊆ U, IsCompact K →
      IntegrableOn w K ∧ IntegrableOn ws K ∧ IntegrableOn wt K) :
    HasWeakPartialsOn U (fun z => β z • w z) (fun z => fderiv ℝ β z 1 • w z + β z • ws z)
      (fun z => fderiv ℝ β z Complex.I • w z + β z • wt z) := by
  sorry

end JHolomorphic
Source
Standard (weak derivatives and Lebesgue spaces).

View graph