English
Let f be a continuous multilinear map and g_i differentiable. The strict derivative of x ↦ f(x)(g_i x) is the sum of the derivative in the first coordinate and the derivatives coming from each g_i.
Русский
Пусть f — непрерывно мультилинейное отображение, g_i — дифференцируемы. Строгая производная от x ↦ f(x)(g_i x) равна сумме вкладов: производная по x и производные по каждому g_i.
LaTeX
$$$\text{HasStrictFDerivAt}\bigl( x \mapsto f(x)(g·x) \bigr) = (\text{apply term}) + \sum_i (\text{derivative from } g_i).$$$
Lean4
theorem _root_.HasStrictFDerivAt.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 : HasStrictFDerivAt f f' x)
(hg : ∀ i, HasStrictFDerivAt (g i) (g' i) x) :
HasStrictFDerivAt (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
convert
ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.comp x (hf.prodMk (hasStrictFDerivAt_pi.2 hg))
ext
simp
