English
The derivative of the map x ↦ f(x)(g · x) exists with derivative given by a linear combination of the derivatives of f and of g.
Русский
Существуют производная для отображения x ↦ f(x)(g · x) и она равна линейной комбинации производных f и g.
LaTeX
$$$\text{HasFDerivAt}\bigl( x \mapsto f(x)(g \cdot x)\bigr) = (\text{terms from }f'\text{ and }g').$$$
Lean4
/-- Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied
to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`. -/
theorem _root_.HasFDerivAt.multilinear_comp [DecidableEq ι] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
{g : ∀ i, G → E i} {g' : ∀ i, G →L[𝕜] E i} {x : G} (hg : ∀ i, HasFDerivAt (g i) (g' i) x) :
HasFDerivAt (fun x ↦ f (fun i ↦ g i x)) ((∑ i : ι, (f.toContinuousLinearMap (fun j ↦ g j x) i) ∘L (g' i))) x := by
simpa using (hasFDerivAt_const f x).continuousMultilinearMap_apply hg
