iterated_deriv — Mathlib

English

If a function is polynomial on a set, then its iterated derivative is polynomial on that set.

Русский

Если функция полиномальна на множестве, то её итерационная производная тоже полиномальна на этом множестве.

LaTeX

$$$\text{CPolynomialOn } 𝕜 f s \Rightarrow \forall n, \text{CPolynomialOn } 𝕜 (\text{Nat.iterate deriv } n f) s$$$

Lean4

/-- If a function is polynomial on a set `s`, so are its successive derivatives. -/
theorem iterated_deriv (h : CPolynomialOn 𝕜 f s) (n : ℕ) : CPolynomialOn 𝕜 (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

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