Mixed coordinate derivatives are invariant under list permutations

Proved

HunterPDE.Shared.iteratedPartial_eq_of_perm

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

derivative-estimatesmultilinear-algebrareal-analysis

Let u be a smooth real-valued function on an open set s in Euclidean n-space. If two finite lists of coordinate indices are permutations of one another, their iterated coordinate derivatives agree at every point of s. The statement concerns derivatives along the entire lists, including repeated indices and the empty list. Smoothness ensures symmetry of second derivatives; adjacent swaps generate all list permutations.

Preamble

import Theorems.Thm_HunterPDE_Shared_contDiffOn_iteratedPartial
import Definitions.Def_HunterPDE_Shared_PartialDeriv
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Tactic.Positivity

open scoped ContDiff
open HunterPDE.Shared
set_option autoImplicit false

Formal statement

theorem HunterPDE.Shared.iteratedPartial_eq_of_perm {n : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hs : IsOpen s) (hu : ContDiffOn ℝ ∞ u s)
    {l t : List (Fin n)} (hp : l.Perm t) : Set.EqOn (iteratedPartial u l) (iteratedPartial u t) s := by sorry

Source

Hunter, Notes on Partial Differential Equations, revised 6/18/2014, Section 1.8, printed p.10, and Theorem 1.27, printed pp.10–11, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf. Supporting coordinate-calculus interface extracted from the definitions and the coordinate expansion of the Taylor differential; this is not a verbatim numbered source theorem. Symmetry follows from Mathlib.Analysis.Calculus.FDeriv.Symmetric, ContDiffAt.isSymmSndFDerivAt.

View graph