proposition: Lemma esumB D f g : summable D f -> summable D g -> (forall i, D i -> 0 <= f i) -> (forall i, D i -> 0 <= g i) -> \esum_(i in D) (f \- g)^\+ i - \esum_(i in D) (f \- g)^\- i = \esum_(i in D) f i - \esum_(i in D) g i.
proof: Proof. move=> Df Dg f0 g0. have /eqP : esum D (f \- g)^\+ + esum_posneg D g = esum D (f \- g)^\- + esum_posneg D f. rewrite !ge0_esum_posneg// -!esumD//; last 2 first. by move=> t Dt; rewrite le_maxr lexx orbT. by move=> t Dt; rewrite le_maxr lexx orbT. apply eq_esum => i Di; have [fg|fg] := leP 0 (f i - g i). rewrite max_r 1?leeNl ?oppe0// add0e subeK//. by rewrite fin_num_abs (summable_pinfty Dg). rewrite add0e max_l; last by rewrite leeNr oppe0 ltW. rewrite fin_num_oppeB//; last by rewrite fin_num_abs (summable_pinfty Dg). by rewrite -addeA addeCA addeA subeK// fin_num_abs (summable_pinfty Df). rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first. - rewrite fin_numD; apply/andP; split. rewrite (@eq_esum _ _ _ _ (abse \o (f \- g)^\+))//. by rewrite -summableE; exact/summable_funepos/summableB. by move=> t Dt; rewrite /= gee0_abs. move: Dg; rewrite summableE (@eq_esum _ _ _ _ g)//. by rewrite ge0_esum_posneg// => t Tt; rewrite gee0_abs// g0. by move=> t Tt; rewrite gee0_abs// g0. - rewrite fin_num_adde_defr// ge0_esum_posneg//. rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq; last 2 first. - rewrite ge0_esum_posneg// (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di. by rewrite /= gee0_abs// f0. - rewrite fin_num_adde_defl// ge0_esum_posneg//. rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di. by rewrite /= gee0_abs// g0. by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->. 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