iterate_derivative_comp_one_sub_X

English

For p and natural k, the k-th derivative of p ∘ (1 − X) equals (−1)^k times the k-th derivative of p composed with (1 − X).

Русский

Для p и натурального k, k-я производная от p ∘ (1 − X) равна (−1)^k умноженному на [k-я производная] p, композиция с (1 − X).

LaTeX

$$$\operatorname{derivative}^{[k]}\big(p \circ (1 - X)\big) = (-1)^k \cdot \big(\operatorname{derivative}^{[k]} p\big) \circ (1 - X)$$$

Lean4

@[simp]
theorem iterate_derivative_comp_one_sub_X (p : R[X]) (k : ℕ) :
    derivative^[k] (p.comp (1 - X)) = (-1) ^ k * (derivative^[k] p).comp (1 - X) := by
  induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih (derivative p), derivative_comp, pow_succ]

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