English
If a function f: 𝕜 → 𝕜 has a derivative f' at x with x fixed by f and MapsTo property ensuring s maps into s, then the n-th iterate f^[n] has derivative f' raised to the n-th power at x within s.
Русский
Пусть f: 𝕜 → 𝕜 имеет производную f' в точке x; если f(x) = x и s сохраняется при применении f (MapsTo f s s), то n-й составной итерат f^[n] имеет производную f'^n в x внутри s.
LaTeX
$$$$HasDerivWithinAt\ f^{[n]}\bigl(f'^n\bigr)\ s\ x.$$$$
Lean4
protected theorem iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivWithinAt f f' s x) (hx : f x = x) (hs : MapsTo f s s)
(n : ℕ) : HasDerivWithinAt f^[n] (f' ^ n) s x :=
by
have := HasFDerivWithinAt.iterate hf hx hs n
rwa [ContinuousLinearMap.smulRight_one_pow] at this
