English
The nth iterated derivative is unchanged after permuting the order of taking derivatives.
Русский
Симметричность производной сохраняется при перестановке порядка дифференцирования.
LaTeX
$$$$ (\\iteratedFDerivWithin 𝕜 n f s x)\\mathrm{domDomCongr} \\sigma = \\iteratedFDerivWithin 𝕜 n f s x $$$$
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 (h : HasFPowerSeriesOnBall f p x r) (h' : AnalyticOn 𝕜 f univ) {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 h' uniqueDiffOn_univ (mem_univ x) v
