English
The n-th derivative of a function is defined inductively as a multilinear map: for n=0, it is the zeroth order map given by f(x); for n+1, it is the derivative of the previous derivative.
Русский
Н-й производной функции задаются индуктивно: при n=0 это нулевой порядок отображения f(x); при n+1 — производная от предыдущей производной.
LaTeX
$$$\text{iteratedFDeriv }_{\mathbb{K}}^{n} f \,=\, \text{ inductive definition with } n=0 \text{ and } n+1}$$
Lean4
/-- The `n`-th derivative of a function, as a multilinear map, defined inductively. -/
noncomputable def iteratedFDeriv (n : ℕ) (f : E → F) : E → E [×n]→L[𝕜] F :=
Nat.recOn n (fun x => ContinuousMultilinearMap.uncurry0 𝕜 E (f x)) fun _ rec x =>
ContinuousLinearMap.uncurryLeft (fderiv 𝕜 rec x)
