English
If f and g are differentiable at x with derivatives f', g', then the map y ↦ B(f(y), g(y)) has a Fréchet derivative at x equal to B.precompR(f x) g' + B.precompL f' (g x).
Русский
Если f,g дифференцируемы в x с производными f', g', то отображение y↦B(f(y),g(y)) имеет Фрéше-производную в x, равную указанной сумме.
LaTeX
$$$\text{HasFDerivAt} (y\mapsto B(f(y),g(y))) \; ( B.precompR(G')(f x)\; g' + B.precompL G' f' (g x))$$$
Lean4
theorem comp {g : F → G} {g' : F →L[𝕜] G} {L' : Filter F} (hg : HasFDerivAtFilter g g' (f x) L')
(hf : HasFDerivAtFilter f f' x L) (hL : Tendsto f L L') : HasFDerivAtFilter (g ∘ f) (g'.comp f') x L :=
by
let eq₁ := (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO
let eq₂ := (hg.isLittleO.comp_tendsto hL).trans_isBigO hf.isBigO_sub
refine .of_isLittleO <| eq₂.triangle <| eq₁.congr_left fun x' => ?_
simp
/- A readable version of the previous theorem, a general form of the chain rule. -/
