proposition: Lemma lt_sum_lim_series (R : realFieldType) (f : R ^nat) n : cvg (series f @ \oo) -> (forall d, 0 < f (n + d.*2)%N + f (n + d.*2.+1)%N) -> \sum_(0 <= i < n) f i < lim (series f @ \oo).
proof: Proof. move=> /cvg_ballP cf fn. have fn0 : 0 < f n + f n.+1 by have := fn 0%N; rewrite double0 addn0 addn1. rewrite ltNge; apply: contraPN cf => ffn /(_ _ fn0). have nf_ub N : \sum_(0 <= i < n.+2) f i <= \sum_(0 <= i < N.+1.*2 + n) f i. elim: N => // N /le_trans ->//; rewrite -(addn1 (N.+1)) doubleD addnAC. rewrite [in leRHS]/index_iota subn0 iotaD big_cat. rewrite -[in X in _ <= X + _](subn0 (N.+1.*2 + n)%N) lerDl /= add0n. by rewrite 2!big_cons big_nil addr0 -(addnC n) ltW// -addnS fn. case=> N _ Nfn; have /Nfn/ltr_distlCDr : (N.+1.*2 + n >= N)%N. by rewrite doubleS -addn2 -addnn -2!addnA leq_addr. rewrite addrA => ffnfn. have : lim (series f @ \oo) + f n + f n.+1 <= \sum_(0 <= i < N.+1.*2 + n) f i. apply: (le_trans _ (nf_ub N)). by do 2 rewrite big_nat_recr //=; by rewrite -2!addrA lerD2r. by move/(lt_le_trans ffnfn); rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp