English
If f has a strict derivative at x, and f(x) = x, then all iterates f^[n] have derivatives (f')^n at x.
Русский
Если у f есть строгая производная в x и x — фиксированная точка, тогда для всех n функции f^[n] имеют производную (f')^n в x.
LaTeX
$$$$ \text{HasStrictFDerivAt } f f' x \land f(x) = x \Rightarrow \forall n,\; \text{HasStrictFDerivAt } f^{[n]} (f')^{n} x. $$$$
Lean4
/-- The chain rule for derivatives in the sense of strict differentiability. -/
@[fun_prop]
protected theorem comp {g : F → G} {g' : F →L[𝕜] G} (hg : HasStrictFDerivAt g g' (f x))
(hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => g (f x)) (g'.comp f') x :=
.of_isLittleO <|
((hg.isLittleO.comp_tendsto (hf.continuousAt.prodMap' hf.continuousAt)).trans_isBigO hf.isBigO_sub).triangle <| by
simpa only [g'.map_sub, f'.coe_comp'] using (g'.isBigO_comp _ _).trans_isLittleO hf.isLittleO
