English
For any power series f and natural n, the truncation of the derivative equals the derivative of the truncation shifted by one: trunc n f'. = derivative (trunc (n+1) f).
Русский
Для любой степенной серии f и натурального n выполняется: trunc n f'. = derivative (trunc (n+1) f).
LaTeX
$$$ \\operatorname{trunc}_n(f') = \\operatorname{derivative}(\\operatorname{trunc}_{n+1} f) $$$
Lean4
theorem trunc_derivativeFun (f : R⟦X⟧) (n : ℕ) : trunc n f.derivativeFun = derivative (trunc (n + 1) f) :=
by
ext d
rw [coeff_trunc]
split_ifs with h
· have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]
· have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]
--A special case of `derivativeFun_mul`, used in its proof.
