English
For polynomials p, q ∈ R[X], the n-th derivative of p q is given by Leibniz-type convolution: derivative^[n](p q) = sum_{k=0}^{n} binom(n,k) (derivative^[n−k] p) (derivative^[k] q).
Русский
Для многочленов p, q ∈ R[X] n-я производная от произведения p q равна свёртке Лейбница: derivative^[n](p q) = ∑_{k=0}^{n} binom(n,k) (derivative^[n−k] p) (derivative^[k] q).
LaTeX
$$$$ \operatorname{derivative}^{n}(p q) = \sum_{k=0}^{n} {n \choose k} \big( \operatorname{derivative}^{n-k} p \big) \big( \operatorname{derivative}^{k} q \big) $$$$
Lean4
theorem iterate_derivative_mul {n} (p q : R[X]) :
derivative^[n] (p * q) = ∑ k ∈ range n.succ, (n.choose k • (derivative^[n - k] p * derivative^[k] q)) := by
induction n with
| zero => simp [Finset.range]
| succ n
IH =>
calc
derivative^[n + 1] (p * q) =
derivative (∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k] q)) :=
by rw [Function.iterate_succ_apply', IH]
_ =
(∑ k ∈ range n.succ, n.choose k • (derivative^[n - k + 1] p * derivative^[k] q)) +
∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
by
simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply', smul_add,
sum_add_distrib]
_ =
(∑ k ∈ range n.succ, n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
1 • (derivative^[n + 1] p * derivative^[0] q) +
∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
?_
_ =
((∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q)) +
∑ k ∈ range n.succ, n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
1 • (derivative^[n + 1] p * derivative^[0] q) :=
by rw [add_comm, add_assoc]
_ =
(∑ i ∈ range n.succ, (n + 1).choose (i + 1) • (derivative^[n + 1 - (i + 1)] p * derivative^[i + 1] q)) +
1 • (derivative^[n + 1] p * derivative^[0] q) :=
by simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
_ = ∑ k ∈ range n.succ.succ, n.succ.choose k • (derivative^[n.succ - k] p * derivative^[k] q) := by
rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
congr
refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
· rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
refine sum_congr rfl fun k hk => ?_
rw [mem_range] at hk
congr
cutsat
· rw [Nat.choose_zero_right, tsub_zero]
