Full Permutation Symmetry of Iterated Derivatives

This is the full permutation-symmetry theorem for iterated Fréchet derivatives of a smooth map.

Let $E$ be a real inner-product space, let $F$ be a real normed space, and let $f:E\to F$ be $C^\infty$. For every $n\in\mathbb N$, $x\in E$, every list of directions $v:\operatorname{Fin}(n)\to E$, and every permutation $\sigma$ of $\operatorname{Fin}(n)$,

This provides the higher-order symmetry used when rearranging derivative slots in multilinear and cumulant expansions.

Formalization Note. The smoothness assumption is ContDiff ℝ ∞; the statement includes the case $n=0$.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem iteratedFDeriv_comp_perm_of_contDiff {f : E → F} (hf : ContDiff ℝ ∞ f) (n : ℕ) (x : E)
    (v : Fin n → E) (σ : Equiv.Perm (Fin n)) :
    iteratedFDeriv ℝ n f x (v ∘ σ) = iteratedFDeriv ℝ n f x v

Module navigation

Module: Analysis/BakryEmery/IteratedDerivative.

Supporting theorems: iteratedFDeriv_comp_swap_zero_one, iteratedFDeriv_succ_comp_perm_of_fix_zero.

Previous: iteratedFDeriv_comp_swap_zero_one.

Source excerpt, lines 250–252 · Frozen source 408915f.