English
The k-th iterated derivative of a continuous multilinear map f at a point x is defined as the finite sum over all embeddings e: Fin k ↪ ι of the corresponding iteratedFDerivComponent evaluated at the right-projected input Pi.compRightL 𝕜 _ Subtype.val x.
Русский
k-я итеративная производная непрерывного многолинейного отображения f в точке x определяется как конечная сумма по всем вложениям e: Fin k ↪ ι от соответствующей компоненты iteratedFDerivComponent, оцененной на указанном входе.
LaTeX
$$$\operatorname{iteratedFDeriv} f k x = \sum_{e: Fin k \hookrightarrow ι} \operatorname{iteratedFDerivComponent} f e.toEquivRange (\Pi.\text{compRightL } x)$$$
Lean4
/-- The `k`-th iterated derivative of a continuous multilinear map `f` at the point `x`. It is a
continuous 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`).
The fact that this is indeed the iterated Fréchet derivative is proved in
`ContinuousMultilinearMap.iteratedFDeriv_eq`.
-/
protected def iteratedFDeriv (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
ContinuousMultilinearMap 𝕜 (fun (_ : Fin k) ↦ (∀ i, E₁ i)) G :=
∑ e : Fin k ↪ ι, iteratedFDerivComponent f e.toEquivRange (Pi.compRightL 𝕜 _ Subtype.val x)
