English
Let f be analytic on the whole space. For every n ≥ 0, for every v: Fin(n) → E and every permutation σ of Fin(n), the nth iterated derivative at x satisfies (iteratedFDeriv 𝕜 n f x)(v) = (iteratedFDeriv 𝕜 n f x)(v ∘ σ). In words, the nth derivative is symmetric in its n arguments.
Русский
Пусть f аналитична на всей пространстве. Для любого n ≥ 0, для любого v: Fin(n) → E и любой перестановки σ ∈ Perm(Fin(n)) выполняется (iteratedFDeriv 𝕜 n f x)(v) = (iteratedFDeriv 𝕜 n f x)(v ∘ σ). Другими словами, n-я производная симметрична по своим n аргументам.
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 : AnalyticOn 𝕜 f univ) {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) _ _
