English
If f has a derivative at x with respect to a filter L and f(x) = x and Tendsto f L L, then all iterates f^[n] have derivatives at x with respect to L, with derivatives (f')^n.
Русский
Если у f есть производная по фильтру HasFDerivAtFilter в x, и f(x) = x, Tendsto f L L, тогда все итерации f^[n] имеют производные в x по L и производные (f')^n.
LaTeX
$$$$ \text{HasFDerivAtFilter } f f' x L \to \text{Tendsto } f L L \to f x = x \to \forall n,\; \text{HasFDerivAtFilter } f^{[n]} (f')^{n} x L. $$$$
Lean4
protected theorem iterate {f : E → E} {f' : E →L[𝕜] E} (hf : HasFDerivAtFilter f f' x L) (hL : Tendsto f L L)
(hx : f x = x) (n : ℕ) : HasFDerivAtFilter f^[n] (f' ^ n) x L := by
induction n with
| zero => exact hasFDerivAtFilter_id x L
| succ n ihn =>
rw [Function.iterate_succ, pow_succ]
rw [← hx] at ihn
exact ihn.comp x hf hL
