iterate — Mathlib

English

Same as above: iterates preserve differentiability within s with derivatives (f')^n.

Русский

То же самое: итерации сохраняют дифференцируемость внутри s с производными (f')^n.

LaTeX

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

Lean4

@[fun_prop]
protected theorem iterate {f : E → E} {f' : E →L[𝕜] E} (hf : HasFDerivWithinAt f f' s x) (hx : f x = x)
    (hs : MapsTo f s s) (n : ℕ) : HasFDerivWithinAt f^[n] (f' ^ n) s x :=
  by
  refine HasFDerivAtFilter.iterate hf ?_ hx n
  rw [nhdsWithin]
  convert tendsto_inf.2 ⟨hf.continuousWithinAt, _⟩
  exacts [hx.symm, (tendsto_principal_principal.2 hs).mono_left inf_le_right]

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