English
HasStrictFDerivAt of applying a fixed multilinear map to a vector-valued function: derivative is sum of apply-derivative and slot-derivatives.
Русский
Строгий Ф-дифференциал применения фиксированного мультилокального отображения к векторной функции: сумма частных производных применена и производные по слоту.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( x \mapsto f(x)(g \cdot x) \bigr) = \cdot$$$
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)`. Version inside a set. -/
theorem _root_.HasFDerivWithinAt.multilinear_comp [DecidableEq ι] {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
{g : ∀ i, G → E i} {g' : ∀ i, G →L[𝕜] E i} {s : Set G} {x : G} (hg : ∀ i, HasFDerivWithinAt (g i) (g' i) s x) :
HasFDerivWithinAt (fun x ↦ f (fun i ↦ g i x)) ((∑ i : ι, (f.toContinuousLinearMap (fun j ↦ g j x) i) ∘L (g' i))) s
x :=
by simpa using (hasFDerivWithinAt_const f x s).continuousMultilinearMap_apply hg
