English
For a bilinear map, the within-derivative equals the derivative derivative: fderivWithin 𝕜 (y ↦ B(f(y), g(y))) within s at x is the sum of precomp terms involving f', g' and the derivatives in the inner maps.
Русский
Для билинейного отображения внутри-дифференцирование дает сумму пред-образов с использованием производных f' и g'.
LaTeX
$$$fderivWithin 𝕜 (y\mapsto B(f(y),g(y))) s x = B.precompR G' (f x) (f'') + B.precompL G' (f'') (g x)$$$
Lean4
theorem fderivWithin_of_bilinear {f : G' → E} {g : G' → F} {x : G'} {s : Set G'} (hf : DifferentiableWithinAt 𝕜 f s x)
(hg : DifferentiableWithinAt 𝕜 g s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun y => B (f y) (g y)) s x =
B.precompR G' (f x) (fderivWithin 𝕜 g s x) + B.precompL G' (fderivWithin 𝕜 f s x) (g x) :=
(B.hasFDerivWithinAt_of_bilinear hf.hasFDerivWithinAt hg.hasFDerivWithinAt).fderivWithin hs
