English
Explicitly expresses the (n+1)-th derivative via a curry-right equivalence and the n-th derivative of the derivative.
Русский
Явно выражено (n+1)-я производная через карри-правое отображение и n-ю производную производной.
LaTeX
$$$\operatorname{iteratedFDeriv}_{\mathbb{k}}(n+1)\ f\ x = (\text{continuousMultilinearCurryRightEquiv'}_{\mathbb{k}}\ n\ E\ F)^{\mathrm{symm}} \circ \operatorname{iteratedFDeriv}_{\mathbb{k}} n (\lambda y.\ fderiv_{\mathbb{k}} f\ y)\ x$$$
Lean4
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the `n`-th derivative of the derivative. -/
theorem iteratedFDeriv_succ_eq_comp_right {n : ℕ} :
iteratedFDeriv 𝕜 (n + 1) f x =
((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x :=
by
ext m
rw [iteratedFDeriv_succ_apply_right, comp_apply, continuousMultilinearCurryRightEquiv_symm_apply']
