proposition: Lemma summable_eseries (f : nat -> \bar R) (P : pred nat) : summable P f -> \sum_(i <oo | P i) (f i) = \sum_(i <oo | P i) f^\+ i - \sum_(i <oo | P i) f^\- i.
proof: Proof. move=> Pf. pose A_ n := (\sum_(0 <= k < n | P k) fine (f^\+ k))%R. pose B_ n := (\sum_(0 <= k < n | P k) fine (f^\- k))%R. pose C_ n := fine (\sum_(0 <= k < n | P k) f k). pose A := lim (A_ @ \oo). pose B := lim (B_ @ \oo). suff: ((fun n => C_ n - (A - B)) @ \oo --> (0 : R^o))%R. move=> CAB. rewrite [X in X - _]summable_nneseries_lim//; last exact/summable_funepos. rewrite [X in _ - X]summable_nneseries_lim//; last exact/summable_funeneg. rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first. by apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB) => //; exact: cvg_cst. apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=. by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge. have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R. apply: cvgD. - by apply: summable_cvg => //; exact/summable_funepos. - by apply: cvgN; apply: summable_cvg => //; exact/summable_funeneg. move=> /cvgrPdist_lt cvgAB; apply/cvgrPdist_lt => e e0. move: cvgAB => /(_ _ e0) [N _/= hN] /=. near=> n. rewrite distrC subr0. have -> : (C_ = A_ \- B_)%R. apply/funext => k. rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//. apply eq_bigr => i Pi; rewrite -fineB//. - by rewrite [in LHS](funeposneg f). - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos. - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg. by rewrite distrC; apply: hN; near: n; exists N. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun