English
Let B be a bilinear map, f,g differentiable with derivatives f',g' at x. Then the inner derivative of y ↦ B(f(y),g(y)) is B.precompR(...) + B.precompL(...).
Русский
Пусть B - билинейное отображение. Если f,g дифференцируемы в окрестности x с производными f', g', соответственно, то внутри множества существует производная функции y↦B(f(y),g(y)) и она равна сумме B.precompR и B.precompL.
LaTeX
$$$\text{HasFDerivWithinAt} (y\mapsto B(f(y),g(y)))\; ( B\_precompR.G'(f x)\, g' + B\_precompL G' f'\,(g x))$$$
Lean4
@[fun_prop]
theorem hasFDerivWithinAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'}
{s : Set G'} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
HasFDerivWithinAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) s x := by
-- need `by exact` to deal with tricky unification
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prodMk hg)
