Iterated coordinate derivatives remain smooth on an open set

Proved

HunterPDE.Shared.contDiffOn_iteratedPartial

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

derivative-estimatesmultilinear-algebrareal-analysis

If a real-valued function on Euclidean n-space is smooth on an open set s, then every iterated coordinate derivative indexed by a finite list is smooth on s. The empty list gives the original function. The coordinate derivatives are defined using the Frechet derivative and the standard basis, so the assertion applies to the published Hunter partial-derivative definitions.

Preamble

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.contDiffOn_iteratedPartial {n : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hs : IsOpen s) (hu : ContDiffOn ℝ ∞ u s)
    (l : List (Fin n)) : ContDiffOn ℝ ∞ (iteratedPartial u l) 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.

View graph