English
If hh₂ is HasDerivAtFilter at h(x) with derivative h₂' and hh is HasDerivAtFilter at x with derivative h', then the iterate under the filter has derivative h₂' * h'.
Русский
Если hh₂ имеет HasDerivAtFilter в h(x) с производной h₂', а hh имеет HasDerivAtFilter в x с производной h', то производная итерации по фильтру равна h₂' * h'.
LaTeX
$$$$\\forall x:\\ HasDerivAtFilter h₂ h₂' (h x) L' \\land HasDerivAtFilter h h' x L \\Rightarrow HasDerivAtFilter (h_2\\circ h) (h_2' * h') x L. $$$$
Lean4
protected nonrec theorem iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAtFilter f f' x L) (hL : Tendsto f L L)
(hx : f x = x) (n : ℕ) : HasDerivAtFilter f^[n] (f' ^ n) x L :=
by
have := hf.iterate hL hx n
rwa [ContinuousLinearMap.smulRight_one_pow] at this
