English
If f and g have strict Fréchet derivatives at x with derivatives f', g', then the map y ↦ B(f(y), g(y)) has a strict Fréchet derivative at x given by B.precompR(f x) g' + B.precompL f' (g x).
Русский
Если f и g имеют строгую Фрéше-частную производную в x с производными f', g', то y ↦ B(f(y), g(y)) имеет строгую Фрéше-производную в x, равную B.precompR(f x) g' + B.precompL f' (g x).
LaTeX
$$$\text{HasStrictFDerivAt} (y\mapsto B(f(y),g(y)))\; ( B.precompR(G')(f x)\, g' + B.precompL G' f' (g x))$$$
Lean4
@[fun_prop]
theorem hasStrictFDerivAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'}
(hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
HasStrictFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x :=
(B.isBoundedBilinearMap.hasStrictFDerivAt (f x, g x)).comp x (hf.prodMk hg)
