English
If ι is finite and f is a multilinear map, the k-th iterated derivative of f at a point x is defined as the sum over all embeddings e: Fin k ↪ ι of the corresponding iteratedFDerivComponent f e x.
Русский
Если ι конечен, а f — многолинейное отображение, k-я итеративная производная f в точке x определяется как сумма по всем встраиваниям e: Fin k ↪ ι соответствующим компонентам iteratedFDerivComponent f e x.
LaTeX
$$$${\rm iteratedFDeriv}_k(f)(x) = \sum_{e: Fin(k) \hookrightarrow ι} \; iteratedFDerivComponent(f, e^{\mathrm{to\,EquivRange}})(x).$$$$
Lean4
/-- The `k`-th iterated derivative of a multilinear map `f` at the point `x`. It is a multilinear
map of `k` vectors `v₁, ..., vₖ` (with the same type as `x`), mapping them
to `∑ f (x₁, (v_{i₁})₂, x₃, ...)`, where at each index `j` one uses either `xⱼ` or one
of the `(vᵢ)ⱼ`, and each `vᵢ` has to be used exactly once.
The sum is parameterized by the embeddings of `Fin k` in the index type `ι` (or, equivalently,
by the subsets `s` of `ι` of cardinality `k` and then the bijections between `Fin k` and `s`).
For the continuous version, see `ContinuousMultilinearMap.iteratedFDeriv`. -/
protected noncomputable def iteratedFDeriv [Fintype ι] (f : MultilinearMap R M₁ M₂) (k : ℕ) (x : (i : ι) → M₁ i) :
MultilinearMap R (fun (_ : Fin k) ↦ (∀ i, M₁ i)) M₂ :=
∑ e : Fin k ↪ ι, iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)
