Shifted higher product rule for smooth coordinate derivatives

Proved

HunterPDE.Sobolev.iteratedPartial_shifted_mul

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

calculuspartial-differential-equations

Let η and φ be globally C∞ real functions on Euclidean n-space, and let δ and β be arbitrary multi-indices. For any finite set S containing every coordinatewise sub-index of β, the βth derivative of (D^δ η)φ equals the sum over γ in S of the multi-index binomial coefficient times D^(δ+(β−γ)) η times D^γ φ, evaluated at the same point. Additional indices in S contribute zero. The coordinate derivatives are composed in the order fixed by the Sobolev definition; global smoothness permits commuting mixed partial derivatives. This is the ordinary higher product rule with an arbitrary initial derivative shift, and has no weak-derivative or measure assumptions.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
import Mathlib.Data.Nat.Choose.Basic

open HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.iteratedPartial_shifted_mul {n : ℕ}
    (η φ : EuclideanSpace ℝ (Fin n) → ℝ)
    (hη : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) η)
    (hφ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) φ)
    (δ β : Fin n → ℕ) (s : Finset (Fin n → ℕ))
    (hs : ∀ γ : Fin n → ℕ, (∀ i, γ i ≤ β i) → γ ∈ s)
    (x : EuclideanSpace ℝ (Fin n)) :
    iteratedPartial β (fun y => iteratedPartial δ η y * φ y) x =
      ∑ γ ∈ s, (∏ i, (Nat.choose (β i) (γ i) : ℝ)) *
        (iteratedPartial (fun i => δ i + (β i - γ i)) η x *
          iteratedPartial γ φ x) := by sorry

Source

John K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, §1.8 printed p. 10 (multi-index notation), and Proposition 3.16 proof, printed p. 54 (smooth product rule). The shifted higher formula is a derived consequence of iterating the product rule and commuting smooth mixed partials, not a verbatim source statement.

View graph