English
If g_i have derivatives, then the strict derivative of the map x ↦ f(x)(g · x) exists and is given by a sum of two parts: one from differentiating x in the left argument and one from differentiating each g_i in the right argument slots.
Русский
Если g_i имеют производные, существует строгая производная отображения x ↦ f(x)(g · x), и она равна сумме двух частей: производной по x в левом аргументе и производным по каждому g_i в правых слотах.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( x \mapsto f(x)(g \cdot x) \bigr) = (\text{left term}) + \sum_i (\text{right term}_i).$$$
Lean4
theorem _root_.HasFDerivAt.continuousMultilinearMap_apply {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
[DecidableEq ι] {x : G} {f : G → ContinuousMultilinearMap 𝕜 E F} {g : ∀ i, G → E i}
{f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F} {g' : ∀ i, G →L[𝕜] E i} (hf : HasFDerivAt f f' x)
(hg : ∀ i, HasFDerivAt (g i) (g' i) x) :
HasFDerivAt (fun x ↦ f x (g · x))
(ContinuousMultilinearMap.apply 𝕜 E F (g · x) ∘L f' + ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L g' i) x :=
by
simp only [← hasFDerivWithinAt_univ] at *
exact hf.continuousMultilinearMap_apply hg
