iterate — Mathlib

English

If f has a derivative within s at x, and f(x) = x and MapsTo f s s, then all iterates f^[n] have derivatives within s at x with derivatives (f')^n.

Русский

Если у f есть производная внутри s в x, и f(x) = x, а f отображает s в s, тогда все итерации f^[n] имеют производные внутри s в x и производные (f')^n.

LaTeX

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

Lean4

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

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