English
If a function has a power series in a ball, then its nth iterated derivative equals the sum over permutations of p_n evaluated at permuted arguments.
Русский
Если функция имеет степенной ряд в шаре, то n-я итеративная производная равна сумме по перестановкам p_n на переставленных аргументах.
LaTeX
$$$$ iteratedFDerivWithin 𝕜 n f s x v = \\sum_{\\sigma \\in Perm(Fin n)} p n (v(\\sigma(1)),\\dots,v(\\sigma(n))). $$$$
Lean4
/-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by
`(v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)})` where the sum is over all
permutations of `{1, ..., n}`. -/
theorem iteratedFDeriv_eq_sum_of_completeSpace [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {n : ℕ}
(v : Fin n → E) : iteratedFDeriv 𝕜 n f x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i)) :=
by
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢
exact h.iteratedFDerivWithin_eq_sum_of_completeSpace uniqueDiffOn_univ (mem_univ _) v
