natDegree_iterate_derivative — Mathlib

English

For any p and k, the natDegree of the k-th derivative satisfies natDegree((derivative)^k p) ≤ natDegree(p) − k.

Русский

Для любого p и k natDegree(derivative^k p) ≤ natDegree(p) − k.

LaTeX

$$$\operatorname{natDegree}(\operatorname{derivative}^{k}(p)) \le \operatorname{natDegree}(p) - k$$$

Lean4

theorem natDegree_iterate_derivative (p : R[X]) (k : ℕ) : (derivative^[k] p).natDegree ≤ p.natDegree - k := by
  induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
    rw [Function.iterate_succ_apply', Nat.sub_succ']
    exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

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