English
If f and g are differentiable at x with derivatives f', g' respectively, then the map y ↦ B(f(y), g(y)) has a 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{HasFDerivAt} (y\mapsto B(f(y),g(y)))\; ( B.precompR(G')(f x)\, g' + B.precompL G' f' (g x))$$$
Lean4
@[fun_prop]
theorem hasFDerivAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'}
(hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
HasFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x := by
-- need `by exact` to deal with tricky unification
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prodMk hg)
