English
If f,g are differentiable at x with derivatives f', g', then the Fréchet derivative of y ↦ B(f(y), g(y)) at x is given by the sum B.precompR(f x) g' + B.precompL f' (g x).
Русский
Если f,g дифференцируемы в точке x, то производная билинейного композиционного отображения равна заданной линейной комбинации.
LaTeX
$$$\text{fderiv}_{𝕜} (y\mapsto B(f(y),g(y))) x = B.precompR(G')(f x) \; g' + B.precompL G' f' (g x)$$$
Lean4
example {g : F → G} {g' : F →L[𝕜] G} (hg : HasFDerivAtFilter g g' (f x) (L.map f)) (hf : HasFDerivAtFilter f f' x L) :
HasFDerivAtFilter (g ∘ f) (g'.comp f') x L :=
by
have :=
calc
(fun x' => g (f x') - g (f x) - g' (f x' - f x)) =o[L] fun x' => f x' - f x := hg.isLittleO.comp_tendsto le_rfl
_ =O[L] fun x' => x' - x := hf.isBigO_sub
refine .of_isLittleO <| this.triangle ?_
calc
(fun x' : E => g' (f x' - f x) - g'.comp f' (x' - x))
_ =ᶠ[L] fun x' => g' (f x' - f x - f' (x' - x)) := (Eventually.of_forall fun x' => by simp)
_ =O[L] fun x' => f x' - f x - f' (x' - x) := (g'.isBigO_comp _ _)
_ =o[L] fun x' => x' - x := hf.isLittleO
