iterate — Mathlib

English

If f has a strict derivative f' at x and f(x) = x, then the nth iterate f^[n] has a strict derivative f'^n at x.

Русский

Если у f есть строгая производная f' в точке x и f(x) = x, то n-й итерат f^[n] имеет строгую производную f'^n в x.

LaTeX

$$$$HasStrictDerivAt\ f^{[n]}\bigl(f'^n\bigr)\ x.$$$$

Lean4

protected nonrec theorem iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasStrictDerivAt f f' x) (hx : f x = x) (n : ℕ) :
    HasStrictDerivAt f^[n] (f' ^ n) x := by
  have := hf.iterate hx n
  rwa [ContinuousLinearMap.smulRight_one_pow] at this

Похожие утверждения