English
SumIDeriv is the linear map sending a polynomial to the sum of all its iterated derivatives with respect to natural number indices, i.e., sum over i of derivative^i.
Русский
SumIDeriv задаёт линейное отображение, которое суммирует все повторные производные полинома по натуральному индексу.
LaTeX
$$@[simp] sumIDeriv : R[X] →ₗ[R] R[X] = Finsupp.lsum ℕ (fun _ ↦ id) ∘ₗ derivativeFinsupp$$
Lean4
/-- Sum of iterated derivatives of a polynomial, as a linear map
This definition does not allow different weights for the derivatives. It is likely that it could be
extended to allow them, but this was not needed for the initial use case (the integration by parts
of the integral $I_i$ in the
[Lindemann-Weierstrass](https://en.wikipedia.org/wiki/Lindemann%E2%80%93Weierstrass_theorem)
theorem).
-/
noncomputable def sumIDeriv : R[X] →ₗ[R] R[X] :=
Finsupp.lsum ℕ (fun _ ↦ LinearMap.id) ∘ₗ derivativeFinsupp
