Swap Symmetry of Higher Derivatives

This is a pointwise Schwarz-type symmetry statement for iterated Fréchet derivatives.

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$, and $v:\operatorname{Fin}(n+2)\to E$, swapping the first two derivative directions leaves the $(n+2)$-nd iterated derivative unchanged:

Here $(0\ 1)$ is the permutation exchanging the indices $0$ and $1$.

The lemma is a technical component for establishing full permutation symmetry of higher derivatives.

Original Lean declaration header

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

theorem iteratedFDeriv_comp_swap_zero_one {f : E → F} (hf : ContDiff ℝ ∞ f) (n : ℕ) (x : E)
    (v : Fin (n + 2) → E) :
    iteratedFDeriv ℝ (n + 2) f x (v ∘ Equiv.swap 0 1) = iteratedFDeriv ℝ (n + 2) f x v

Module navigation

Module: Analysis/BakryEmery/IteratedDerivative.

Previous: iteratedFDeriv_succ_comp_perm_of_fix_zero · Next: iteratedFDeriv_comp_perm_of_contDiff.

Source excerpt, lines 222–224 · Frozen source 408915f.