English
The Taylor expansion of an analytic multilinear map around x is given by its iteratedFDeriv terms and factorial normalization when summing along the ball of radius r.
Русский
Рассматривая область анализа, ряд Тейлора мультилайнерного отображения равен сумме членами iteratedFDeriv с факториальной нормализацией в шаре радиуса r.
LaTeX
$$$\text{HasFTaylorSeriesOnBall }(f) = \dots$$$
Lean4
/-- The iterated derivative of an analytic function, on vectors `(y, ..., y)`, is given by `n!`
times the `n`-th term in the power series. For a more general result giving the full iterated
derivative as a sum over the permutations of `Fin n`, see
`HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum`. -/
theorem factorial_smul (n : ℕ) : n ! • p n (fun _ ↦ y) = iteratedFDeriv 𝕜 n f x (fun _ ↦ y) :=
by
cases n
· rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
· rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag, ← ContinuousLinearMap.smul_apply,
factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
rfl
