English
Derivative of the uncurry map (f, g) ↦ f(g1 x, ..., gn x) is the sum of derivatives with respect to each argument slot after currying.
Русский
Дифференциал раскрученного отображения (f, g) ↦ f(g1 x, ..., gn x) равен сумме вкладов дифференциалов по каждому слоту аргументов после каррирования.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( x \mapsto f(g_1 x, \dots, g_n x) \bigr) = \sum_i (f(g_i x) \text{ derivative in slot i}).$$$
Lean4
theorem _root_.HasFDerivWithinAt.continuousMultilinearMap_apply {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
[DecidableEq ι] {s : Set G} {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 : HasFDerivWithinAt f f' s x)
(hg : ∀ i, HasFDerivWithinAt (g i) (g' i) s x) :
HasFDerivWithinAt (fun x ↦ f x (g · x))
(ContinuousMultilinearMap.apply 𝕜 E F (g · x) ∘L f' + ∑ i, (f x).toContinuousLinearMap (g · x) i ∘L g' i) s x :=
by
convert
ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.hasFDerivAt.comp_hasFDerivWithinAt x
(hf.prodMk (hasFDerivWithinAt_pi.2 hg))
ext
simp
