Coordinate evaluations of Frechet derivatives equal multi-index derivatives

Proved

HunterPDE.Shared.iteratedFDeriv_apply_coordinates_eq_multiDeriv

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, and let x∈s. For any assignment a of k coordinate directions, let α_i count how many of those directions equal i. Evaluating the kth Frechet derivative on the standard basis vectors prescribed by a equals the multi-index derivative ∂^αu(x), with the fixed sorted coordinate order of the published Hunter definition. Repeated directions and k=0 are included. This identifies a differential tensor with its multi-index coefficients.

Preamble

import Theorems.Thm_HunterPDE_Shared_iteratedPartial_eq_of_perm
import Theorems.Thm_HunterPDE_Shared_iteratedFDeriv_apply_coordinate_list
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.iteratedFDeriv_apply_coordinates_eq_multiDeriv {n k : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hs : IsOpen s) (hu : ContDiffOn ℝ ∞ u s)
    {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ s) (a : Fin k → Fin n) :
    iteratedFDeriv ℝ k u x (fun j => EuclideanSpace.single (a j) 1) =
      multiDeriv u (fun i => (List.ofFn a).count i) x := 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.

View graph