English
If a function has a power series on a ball, then its nth iterated derivative is given by the permutation-sum formula.
Русский
Если функция имеет степенной ряд внутри шара, то n-я итеративная производная выражается через сумму по перестановкам.
LaTeX
$$$$ HasFPowerSeriesWithinOnBall f p s x r \\Rightarrow \\forall n, \\forall v, \\, iteratedFDerivWithin 𝕜 n f s x v = \\sum_{\\sigma} p n (v(\\sigma(1)),\\dots,v(\\sigma(n))). $$$$
Lean4
/-- The `n`-th iterated derivative of an analytic function on a set is symmetric. -/
theorem iteratedFDerivWithin_comp_perm (h : ContDiffWithinAt 𝕜 ω f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ}
(v : Fin n → E) (σ : Perm (Fin n)) : iteratedFDerivWithin 𝕜 n f s x (v ∘ σ) = iteratedFDerivWithin 𝕜 n f s x v :=
by
rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩
rw [insert_eq_of_mem hx] at hu
have : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
iteratedFDerivWithin_inter_open u_open xu
rw [← this]
exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _
