English
If ω-analytic at x (ContDiffAt 𝕜 ω f x), then for every n and every permutation σ of Fin(n), the nth iterated derivative is symmetric in its inputs: (iteratedFDeriv 𝕜 n f x)(v ∘ σ) = (iteratedFDeriv 𝕜 n f x)(v).
Русский
Если функция аналитична в точке x (ContDiffAt 𝕜 ω f x), то для любого n и перестановки σ на Fin(n) n-я итеративная производная симметрична по входам: (iteratedFDeriv 𝕜 n f x)(v ∘ σ) = (iteratedFDeriv 𝕜 n f x)(v).
LaTeX
$$$\left(\operatorname{iteratedFDeriv}_{\mathbb{k}}^{(n)} f \right)(x)(v \circ \sigma) = \left(\operatorname{iteratedFDeriv}_{\mathbb{k}}^{(n)} f \right)(x)(v).$$$
Lean4
/-- The `n`-th iterated derivative of an analytic function is symmetric. -/
theorem iteratedFDeriv_comp_perm (h : ContDiffAt 𝕜 ω f x) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v :=
by
rw [← iteratedFDerivWithin_univ]
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _
