English
Let f be a continuous multilinear map on a family (M_i). The derivative of f at x in the direction y is a continuous linear map f.linearDeriv(x): (∀ i, M_i) → M_2, defined by summing the partial derivatives along each coordinate. Concretely, for any x = (x_i) and y = (y_i), (f.linearDeriv x)(y) = ∑_i f(x with i-th coordinate replaced by y_i).
Русский
Пусть f — непрерывное мультилинейное отображение на системе пространств M_i. Производная f в точке x по направлению y образует непрерывно-линейное отображение f.linearDeriv(x): (∀ i, M_i) → M₂, заданное суммой частичных производных по каждой координате: f.linearDeriv(x)(y) = ∑_i f(x_1, ..., y_i, ..., x_n).
LaTeX
$$$(f.linearDeriv x)(y) = \sum_{i \in \iota} f\bigl(\text{update}_i(x,y_i)\bigr) ,$$$
Lean4
/-- The derivative of a continuous multilinear map, as a continuous linear map
from `∀ i, M₁ i` to `M₂`; see `ContinuousMultilinearMap.hasFDerivAt`. -/
def linearDeriv : (∀ i, M₁ i) →L[R] M₂ :=
∑ i : ι, (f.toContinuousLinearMap x i).comp (.proj i)
