iterated_deriv — Mathlib

English

If f is analytic on s, then for every n, the nth iterated derivative is analytic on s.

Русский

Если f аналитична на s, то для каждого n аналитична n-я итерационная производная на s.

LaTeX

$$$\text{AnalyticOnNhd } 𝕜 f s \to IsOpen s \to ∀ n, AnalyticOnNhd 𝕜 (Nat.iterate deriv n f) s$$$

Lean4

theorem iterated_deriv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) (n : ℕ) : AnalyticAt 𝕜 (deriv^[n] f) x := by
  induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

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