Composition of smooth multi-index derivatives

Proved

HunterPDE.Sobolev.iteratedPartial_add

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

calculuspartial-differential-equations

For every globally smooth real function on Euclidean n-space and all multi-indices alpha and beta, applying the alpha derivative to the beta derivative equals the derivative of order beta + alpha, as an equality of functions. Smoothness permits reordering the coordinate derivatives. This includes dimension zero and zero derivative orders.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace

open HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.iteratedPartial_add {n : ℕ} (u : EuclideanSpace ℝ (Fin n) → ℝ)
    (hu : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) u) (α β : Fin n → ℕ) :
    iteratedPartial α (iteratedPartial β u) = iteratedPartial (fun i => β i + α i) u := 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, section 1.8 printed p. 10 and Proposition 3.16 proof printed p. 54. Derived classical multi-index calculus identity.

View graph