iterate — Mathlib

English

If f is differentiable at x with derivative f', and f(x) = x, then all iterates f^[n] are differentiable at x with derivative (f')^n.

Русский

Если f дифференцируема в x и f(x) = x, то все итерации f^[n] дифференцируемы в x с производной (f')^n.

LaTeX

$$$$ \text{HasFDerivAt } f f' x \land f(x) = x \Rightarrow \forall n,\; \text{HasFDerivAt } f^{[n]} (f')^{n} x. $$$$

Lean4

@[fun_prop]
protected theorem iterate {f : E → E} (hf : Differentiable 𝕜 f) (n : ℕ) : Differentiable 𝕜 f^[n] :=
  Nat.recOn n differentiable_id fun _ ihn => ihn.comp hf

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