Higher-Derivative Symmetry Under Permutations Fixing One Index

This is a technical symmetry lemma 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$. Fix $n\in\mathbb N$ and assume that the $n$-th derivative is invariant under every permutation of its $n$ input directions. Then, for every $x\in E$, every $v:\operatorname{Fin}(n+1)\to E$, and every permutation $\sigma$ of $\operatorname{Fin}(n+1)$ satisfying $\sigma(0)=0$,

The statement supplies the stabilizer-of-the-first-index step in the permutation symmetry of higher derivatives.

Original Lean declaration header

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

theorem iteratedFDeriv_succ_comp_perm_of_fix_zero {f : E → F} (hf : ContDiff ℝ ∞ f) {n : ℕ}
    (ih : ∀ (y : E) (w : Fin n → E) (τ : Equiv.Perm (Fin n)),
      iteratedFDeriv ℝ n f y (w ∘ τ) = iteratedFDeriv ℝ n f y w)
    (x : E) (v : Fin (n + 1) → E) (σ : Equiv.Perm (Fin (n + 1))) (hσ : σ 0 = 0) :
    iteratedFDeriv ℝ (n + 1) f x (v ∘ σ) = iteratedFDeriv ℝ (n + 1) f x v

Module navigation

Module: Analysis/BakryEmery/IteratedDerivative.

Previous: iteratedFDeriv_inner_self_apply · Next: iteratedFDeriv_comp_swap_zero_one.

Source excerpt, lines 126–130 · Frozen source 408915f.