proposition: Lemma nneseries_split (R : realType) (f : nat -> \bar R) n : (forall k, 0 <= f k) -> \sum_(k <oo) f k = \sum_(k < n) f k + \sum_(n <= k <oo) f k.
proof: Proof. move=> f0; elim: n => [|n ih]; first by rewrite big_ord0 add0e. rewrite big_ord_recr/= -addeA [f n + _](_ : _ = \sum_(n <= k <oo) f k)//. rewrite -lim_shift_cst; last by rewrite (@lt_le_trans _ _ 0). - apply: (@near_eq_lim _ (fun x => f n + _)). exact: is_cvg_ereal_nneg_natsum. by near do rewrite -big_ltn//; exact: nbhs_infty_gt. - exact: is_cvg_ereal_nneg_natsum. - by move=> m; exact: sume_ge0. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau