English
The iterated derivative of a function, when expanded along the ball, equals factorial times the corresponding term of a formal power series.
Русский
Интерпретация итеративной производной по шарy: факториал умножает соответствующий член ряда.
LaTeX
$$$n! \cdot p(n) = \text{iteratedFDeriv}_n(f)$ на диагонали.$$
Lean4
/-- Given `f` a linear map into multilinear maps, then the derivative
of `x ↦ f (a x) (b₁ x, ..., bₙ x)` at `x` applied to a vector `v` is given by
`f (a' v) (b₁ x, ...., bₙ x) + ∑ i, f a (b₁ x, ..., b'ᵢ v, ..., bₙ x)`. -/
theorem _root_.HasFDerivAt.linear_multilinear_comp [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : ∀ i, H → G i}
{b' : ∀ i, H →L[𝕜] G i} {x : H} (ha : HasFDerivAt a a' x) (hb : ∀ i, HasFDerivAt (b i) (b' i) x)
(f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
HasFDerivAt (fun y ↦ f (a y) (fun i ↦ b i y))
((f.flipMultilinear (fun i ↦ b i x)) ∘L a' + ∑ i, ((f (a x)).toContinuousLinearMap (fun j ↦ b j x) i) ∘L (b' i))
x :=
(f.hasFDerivAt.comp x ha).continuousMultilinearMap_apply hb
