English
If a function has a power series within a set, then its nth iterated derivative equals the sum over permutations of p n at the 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 iteratedFDerivWithin_eq_sum (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)
(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
· exact h'.mono inter_subset_left
· exact hs.inter EMetric.isOpen_ball
· exact ⟨hx, EMetric.mem_ball_self h.r_pos⟩
· exact inter_subset_right
