iterated_deriv — Mathlib

English

If f is analytic on s, then the k-th iterated derivative is analytic on s for any natural number k.

Русский

Если f аналитична на s, то k-я итерационная производная аналитична на s, для любого k ∈ ℕ.

LaTeX

$$$\text{AnalyticOnNhd } 𝕜 f s \to \forall n : \mathbb{N}, AnalyticOnNhd 𝕜 (\mathrm{deriv}^{(n)} f) s$$$

Lean4

/-- If a function is analytic on a set `s`, so are its successive derivatives. -/
theorem iterated_deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) : AnalyticOnNhd 𝕜 (deriv^[n] f) s := by
  induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

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