English
If f is a continuous multilinear map and g_i are differentiable, then the map (f, x) ↦ f(x) with x input to the multilinear map has a Fréchet derivative equal to the sum of the two contributions: derivative in the f-direction and derivative from differentiating each argument x in its slot.
Русский
Пусть f — непрерывно мультилинейное отображение, а функции g_i дифференцируемы. Тогда отображение (f, x) ↦ f(x) имеет Фрéше-дифференциал, равный сумме вкладов при дифференцировании по f и по каждому аргументу x.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( (f, x) \mapsto f(x) \bigr) = \text{(derivative terms from }f\text{ and from each slot)}.$$$
Lean4
protected theorem hasFDerivAt [DecidableEq ι] : HasFDerivAt f (f.linearDeriv x) x :=
(f.hasStrictFDerivAt _).hasFDerivAt
