sum_taylor_eq — Mathlib

English

Taylor's formula: f = sum_{i≥0} a_i (X − r)^i, where a_i are the coefficients of taylor r f.

Русский

Формула Тейлора: f = ∑ a_i (X − r)^i, где a_i — коэффициенты в taylor r f.

LaTeX

$$$$ f = \\sum_{i \\ge 0} \\bigl( \\mathrm{coeff}_i(\\operatorname{taylor}(r,f)) \\bigr) \\bigl(X - r\\bigr)^i. $$$$

Lean4

/-- Taylor's formula. -/
theorem sum_taylor_eq (f : R[X]) (r : R) : ((taylor r f).sum fun i a => C a * (X - C r) ^ i) = f := by
  rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel, taylor_zero]

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