English
The n-th coefficient of taylor r f equals (hasseDeriv n f).eval r.
Русский
n-й коэффициент taylor r f равен (hasseDeriv n f).eval r.
LaTeX
$$$$ (\operatorname{taylor} r f)_{n} = (\operatorname{hasseDeriv} n f).\mathrm{eval}(r) $$$$
Lean4
/-- The `k`th coefficient of `Polynomial.taylor r f` is `(Polynomial.hasseDeriv k f).eval r`. -/
theorem taylor_coeff (n : ℕ) : (taylor r f).coeff n = (hasseDeriv n f).eval r :=
show (lcoeff R n).comp (taylor r) f = (leval r).comp (hasseDeriv n) f
by
congr 1; clear! f; ext i
simp only [leval_apply, mul_one, one_mul, eval_monomial, LinearMap.comp_apply, map_sum, hasseDeriv_monomial,
taylor_apply, monomial_comp, C_1, (commute_X (C r)).add_pow i]
simp only [lcoeff_apply, ← C_eq_natCast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C, (Nat.cast_commute _ _).eq,
coeff_X_pow, boole_mul, Finset.sum_ite_eq, Finset.mem_range]
split_ifs with h; · rfl
push_neg at h; rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
