proposition: Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : (forall i, I i -> 0 <= a i) -> (forall i, I i -> 0 <= b i) -> \esum_(i in I) (a i + b i) = \esum_(i in I) a i + \esum_(i in I) b i.
proof: Proof. move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split. rewrite ub_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=. by rewrite leeD// ereal_sup_ub//=; exists X. wlog : a b ag0 bg0 / \esum_(i in I) a i \isn't a fin_num => [saoo|]; last first. move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye. rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: esum. rewrite leye_eq; apply/eqP/eq_infty => y; rewrite esum_ge//. have : y%:E < \esum_(i in I) a i by rewrite aoo// ltry. move=> /ereal_sup_gt[_ [X [finX XI]] <-] /ltW yle; exists X => //=. rewrite (le_trans yle)// fsbig_split// leeDl// fsume_ge0// => // i. by move=> /XI; exact: bg0. case: (boolP (\esum_(i in I) a i \is a fin_num)) => sa; last exact: saoo. case: (boolP (\esum_(i in I) b i \is a fin_num)) => sb; last first. by rewrite addeC (eq_esum (fun _ _ => addeC _ _)) saoo. rewrite -lee_subr_addr// ub_ereal_sup//= => _ [X [finX XI]] <-. have saX : \sum_(i \in X) a i \is a fin_num. apply: contraTT sa => /fin_numPn[] sa. suff : \sum_(i \in X) a i >= 0 by rewrite sa. by rewrite fsume_ge0// => i /XI/ag0. apply/fin_numPn; right; apply/eqP; rewrite -leye_eq esum_ge//. by exists X; rewrite // sa. rewrite lee_subr_addr// addeC -lee_subr_addr// ub_ereal_sup//= => _ [Y [finY YI]] <-. rewrite lee_subr_addr// addeC esum_ge//; exists (X `|` Y). by split; [rewrite finite_setU|rewrite subUset]. rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset//= ?finite_setU//. - exact/subsetP/subsetUl. - by move=> x; rewrite !inE in_setU andb_orr andNb/= => /andP[_] /[!inE] /YI/ag0. - exact/subsetP/subsetUr. - by move=> x; rewrite !inE in_setU andb_orr andNb/= orbF => /andP[_] /[!inE] /XI/bg0. 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