English
If a function has a power series within a ball with values in a complete space F, then the nth iterated derivative equals the sum over permutations of p n.
Русский
Если функция имеет степенной ряд внутри шара, значения в полном пространстве F, тогда 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 iteratedFDerivWithin_eq_sum_of_completeSpace [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E) :
iteratedFDerivWithin 𝕜 n f s x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i)) :=
by
have : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x :=
(iteratedFDerivWithin_inter_open EMetric.isOpen_ball (EMetric.mem_ball_self h.r_pos)).symm
rw [this]
apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
· exact h.mono inter_subset_left
· apply h.analyticOn.mono
rw [insert_eq_of_mem hx]
· exact hs.inter EMetric.isOpen_ball
· exact ⟨hx, EMetric.mem_ball_self h.r_pos⟩
· exact inter_subset_right
