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