proposition: Lemma pseries_diffs_equiv f x : let s i := i%:R * f i * x ^+ i.-1 in cvgn (pseries (pseries_diffs f) x) -> series s @ \oo --> limn (pseries (pseries_diffs f) x).
proof: Proof. move=> s Cx; rewrite -[lim _]subr0. rewrite /pseries/= [X in X @ \oo --> _]/series /=. rewrite [X in X @ \oo --> _](_ : _ = (fun n => \sum_(0 <= i < n) pseries_diffs f i * x ^+ i - n%:R * f n * x ^+ n.-1)); last first. by rewrite funeqE => n; rewrite pseries_diffs_sumE addrK. by apply: cvgB => //; rewrite -cvg_shiftS; exact: cvg_series_cvg_0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex