diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1100d1bebb..e470668ba7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -92,6 +92,27 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+- in `realsum.v`:
+  + lemma `esum_psum`
+  + lemma `esumEsum`
+
+- in `constructive_ereal.v`:
+  + definition `esg`
+  + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0`
+
+- in `esum.v`:
+  + lemmas `esum_eq0P`, `esumZ`, `exchange_esum`
+  + lemmas `le_esum`, `esumN`
+  + lemmas `summable_le_esum`, `summable_esum_funepos`, `summable_esumN`,
+    `summableZ`, `summable_esumZ`
+  + lemmas `esum_if_eq_op`
+  + lemmas `exchange_esum_ereal_sup`
+
+- in `ereal.v`:
+  + lemmas `exchange_ereal_sup`, `ge0_ereal_supZl`, `ge0_ereal_supZl_range`
+
+- in `sequences.v`:
+  + lemmas `ereal_supD`, `ereal_sup_sum`
 
 - in `reals.v`:
   + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
@@ -128,12 +149,6 @@
     * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
   + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
 
-### Changed
-
-- moved from `measurable_structure.v` to `classical_sets.v`:
-  + definition `preimage_set_system`
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
-    `preimage_set_system_id`
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
@@ -159,6 +174,10 @@
 - new files `signed_measure.v` and `radon_nikodym.v`
   + with the contents of `charge.v` (deprecated)
 
+- in `esum.v`:
+  + lemma `ge0_esum`
+  + lemma `esum_ge`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -222,6 +241,30 @@
   + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`,
     `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
     `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
+- in `realsum.v`:
+  + the following now use `funrpos` and `funrneg`:
+    * definition `sum`
+    * lemmas `summable_funrpos`, `summable_funrneg`
+  + lemma `sum0` (now uses `cst`)
+
+- moved from `realsum` to `numfun.v`:
+  + now use `funrpos` and `funrneg`:
+    * lemmas `eq_funrpos`, `eq_funrneg`
+    * lemma `fpos0` (renamed to `funrpos_cst0`)
+    * lemma `fneg0` (renamed to `funrneg_cst0`)
+    * lemmas `funrposZ`, `funrnegZ`
+    * lemmas `funrpos_natrM`, `funrneg_natrM`
+    * lemmas `le_funrpos_norm`
+
+- moved from `numfun.v` to `unstable.v`:
+  + notations `nondecreasing_fun`, `nonincreasing_fun`,
+    `decreasing_fun`, `increasing_fun`
+
+- in `esum.v`:
+  + definition `esum`
+  + lemma `esum_fset`
+  + lemma `esum_ge` -> `PosEsum.pos_esum_ge`
+  + lemma `le_esum` -> `PosEsum.le_pos_esum`
 
 ### Renamed
 
@@ -264,6 +307,9 @@
 - in `measure_function.v`:
   + `isFinite` -> `isFinNumFun`
 
+- in `esum.v`:
+  + `esum_sum` -> ` exchange_esum_sum`
+
 ### Generalized
 
 - in `measurable_structure.v`:
@@ -292,6 +338,12 @@
 - in `simple_functions.v`:
   + lemmas `fctD`, `fctN`, `fctM`, `fctZ`
 
+- in `ereal.v`:
+  + lemmas `ge0_mule_fsumr`, `ge0_mule_fsuml`
+
+- in `esum.v`:
+  + lemma `esum_set1`
+
 ### Deprecated
 
 - file `charge.v` (use `measure.v` and/or `lebesgue_integral.v`)
@@ -303,6 +355,13 @@
 - in `measurable_structure.v`:
   + lemmas `measurable_prod_g_measurableType`, `measurable_prod_g_measurableTypeR`
 
+- in `realsum.v`:
+  + definitions `fpos`, `fneg` (use `funrpos`, `funrneg` instead)
+  + lemmas `fnegN`, `fposN`
+  + lemmas `ge0_pos`, `ge0_neg`
+  + lemma `fposBfneg`
+  + lemma `funrpos_le`
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/unstable.v b/classical/unstable.v
index cf8b4ce04a..d1c516f787 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -16,6 +16,10 @@ From mathcomp Require Import vector archimedean interval.
 (* ```                                                                        *)
 (*                 swap x := (x.2, x.1)                                       *)
 (*           map_pair f x := (f x.1, f x.2)                                   *)
+(*    nondecreasing_fun f == the function f is non-decreasing                 *)
+(*    nonincreasing_fun f == the function f is non-increasing                 *)
+(*       increasing_fun f == the function f is (strictly) increasing          *)
+(*       decreasing_fun f == the function f is (strictly) decreasing          *)
 (*          monotonic A f := {in A &, {homo f : x y / x <= y}} \/             *)
 (*                           {in A &, {homo f : x y /~ x <= y}}               *)
 (*   strict_monotonic A f := {in A &, {homo f : x y / x < y}} \/              *)
@@ -197,6 +201,15 @@ rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
 by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
 Qed.
 
+Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n <= m)%O})
+  (at level 10).
+Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O})
+  (at level 10).
+Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O})
+  (at level 10).
+Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O})
+  (at level 10).
+
 Definition monotonic d (T : porderType d) d' (T' : porderType d')
     (pT : predType T) (A : pT) (f : T -> T') :=
   {in A &, nondecreasing f} \/ {in A &, {homo f : x y /~ (x <= y)%O}}.
diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v
index 26f82b3ef8..847698b84e 100644
--- a/experimental_reals/distr.v
+++ b/experimental_reals/distr.v
@@ -1264,5 +1264,3 @@ End Jensen.
 End Jensen.
 
 Notation convex f := (convexon \-inf \+inf f).
-
-(* -------------------------------------------------------------------- *)
diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v
index 267b1b7688..5f0f1732bd 100644
--- a/experimental_reals/realsum.v
+++ b/experimental_reals/realsum.v
@@ -3,12 +3,14 @@
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_boot all_order all_algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
-From mathcomp.classical Require Import boolp.
-From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
-From mathcomp.classical Require Import classical_sets functions.
+From mathcomp Require Import boolp fsbigop classical_sets functions.
+From mathcomp Require Import cardinality.
+From mathcomp Require Import constructive_ereal reals.
+From mathcomp Require Import xfinmap discrete realseq.
+From mathcomp Require Import esum ereal numfun.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -40,108 +42,23 @@ by have := h fset0; rewrite big_pred0 // => -[x]; rewrite in_fset0.
 Qed.
 End Summable.
 
-(* -------------------------------------------------------------------- *)
-Section Sum.
-Context {R : realType} {T : choiceType}.
-
-Implicit Types f g : T -> R.
-
-Definition fpos f := fun x => `|Num.max 0 (f x)|.
-Definition fneg f := fun x => `|Num.min 0 (f x)|.
-
-Lemma eq_fpos f g : f =1 g -> fpos f =1 fpos g.
-Proof. by move=> eq_fg x; rewrite /fpos eq_fg. Qed.
-
-Lemma eq_fneg f g : f =1 g -> fneg f =1 fneg g.
-Proof. by move=> eq_fg x; rewrite /fneg eq_fg. Qed.
-
-Lemma fpos0 x : fpos (fun _ : T => 0) x = 0 :> R.
-Proof. by rewrite /fpos maxxx normr0. Qed.
-
-Lemma fneg0 x : fneg (fun _ : T => 0) x = 0 :> R.
-Proof. by rewrite /fneg minxx normr0. Qed.
-
-Lemma fnegN f : fneg (- f) =1 fpos f.
-Proof. by move=> x; rewrite /fpos /fneg -{1}oppr0 -oppr_max normrN. Qed.
-
-Lemma fposN f : fpos (- f) =1 fneg f.
-Proof. by move=> x; rewrite /fpos /fneg -{1}oppr0 -oppr_min normrN. Qed.
-
-Lemma fposZ f c : 0 <= c -> fpos (c \*o f) =1 c \*o fpos f.
-Proof.
-move=> ge0_c x; rewrite /fpos /= -{1}(mulr0 c).
-by rewrite -maxr_pMr // normrM ger0_norm.
-Qed.
-
-Lemma fnegZ f c : 0 <= c -> fneg (c \*o f) =1 c \*o fneg f.
-Proof.
-move=> ge0_c x; rewrite /= -!fposN; have /=<- := (fposZ (- f) ge0_c x).
-by apply/eq_fpos=> y /=; rewrite mulrN.
-Qed.
-
-Lemma fpos_natrM f (n : T -> nat) x :
-  fpos (fun x => (n x)%:R * f x) x = (n x)%:R * fpos f x.
-Proof.
-rewrite /fpos -[in RHS]normr_nat -normrM.
-by rewrite maxr_pMr ?ler0n // mulr0.
-Qed.
-
-Lemma fneg_natrM f (n : T -> nat) x :
-  fneg (fun x => (n x)%:R * f x) x = (n x)%:R * fneg f x.
-Proof.
-rewrite -[in RHS]fposN -fpos_natrM -fposN.
-by apply/eq_fpos=> y; rewrite mulrN.
-Qed.
-
-Lemma fneg_ge0 f x : (forall x, 0 <= f x) -> fneg f x = 0.
-Proof. by move=> ?; rewrite /fneg min_l ?normr0. Qed.
-
-Lemma fpos_ge0 f x : (forall x, 0 <= f x ) -> fpos f x = f x.
-Proof. by move=> ?; rewrite /fpos max_r ?ger0_norm. Qed.
-
-Lemma ge0_fpos f x : 0 <= fpos f x.
-Proof. by apply/normr_ge0. Qed.
-
-Lemma ge0_fneg f x : 0 <= fneg f x.
-Proof. by apply/normr_ge0. Qed.
-
-Lemma le_fpos_norm f x : fpos f x <= `|f x|.
-Proof.
-rewrite /fpos ger0_norm ?(le_max, lexx) //.
-by rewrite ge_max normr_ge0 ler_norm.
-Qed.
-
-Lemma le_fpos f1 f2 : f1 <=1 f2 -> fpos f1 <=1 fpos f2.
-Proof.
-move=> le_f x; rewrite /fpos !ger0_norm ?le_max ?lexx //.
-by rewrite ge_max lexx /=; case: ltP => //=; rewrite le_f.
-Qed.
-
-Lemma fposBfneg f x : fpos f x - fneg f x = f x.
-Proof.
-rewrite /fpos /fneg maxC.
-case: (leP (f x) 0); rewrite normr0 (subr0, sub0r) => ?.
-  by rewrite ler0_norm ?opprK.
-by rewrite gtr0_norm.
-Qed.
-
-Definition psum f : R :=
+Definition psum {R : realType} {T : choiceType} (f : T -> R) : R :=
   (* We need some ticked `image` operator *)
   let S := [set x | exists J : {fset T}, x = \sum_(x : J) `|f (val x)| ]%classic in
   if `[<summable f>] then sup S else 0.
 
-Definition sum f : R := psum (fpos f) - psum (fneg f).
-End Sum.
+Definition sum {R : realType} {T : choiceType} (f : T -> R) : R :=
+  psum f^\+ - psum f^\-.
 
 (* -------------------------------------------------------------------- *)
 Section SummableCountable.
 Variable (T : choiceType) (R : realType) (f : T -> R).
 
-Lemma summable_countn0 : summable f -> countable [pred x | f x != 0].
+Lemma summable_countn0 : summable f -> discrete.countable [pred x | f x != 0].
 Proof.
 case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > p.+1%:~R^-1].
 set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}.
-  move=> x; rewrite !inE => nz_fx; exists (Num.truncn `|f x|^-1).
+  move=> x; rewrite !inE => nz_fx; apply/asboolP; exists (Num.truncn `|f x|^-1).
   by rewrite inE invf_plt ?unfold_in/= ?normr_gt0 // -normfV ltr_norm_bound.
 apply/(countable_sub le)/cunion_countable=> i /=.
 case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|].
@@ -194,6 +111,7 @@ case/(_ (NPInf M)): cu => K /= /(_ K (leqnn _)).
 rewrite inE/= => /ltW /le_trans /(_ (ler_norm _)).
 by move/le_lt_trans/(_ (bdu _)); rewrite ltxx.
 Qed.
+
 End PosCnv.
 
 (* -------------------------------------------------------------------- *)
@@ -262,7 +180,8 @@ Qed.
 Lemma eq_sum (F1 F2 : T -> R) : F1 =1 F2 -> sum F1 = sum F2.
 Proof.
 move=> eq_fg; rewrite /sum; congr (_ - _); apply/eq_psum.
-  by apply/eq_fpos. by apply/eq_fneg.
+- exact/eq_funrpos.
+- exact/eq_funrneg.
 Qed.
 
 Lemma le_summable (F1 F2 : T -> R) :
@@ -343,6 +262,27 @@ by case=> /= [|J lt_lJ _]; [apply/summable_sup | exists J].
 Qed.
 End SumTh.
 
+Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) :
+    (forall i, 0 <= f i) -> summable f ->
+  \esum_(x in [set: T]) (f x)%:E = (psum f)%:E.
+Proof.
+move => f0 h; apply/eqP; rewrite eq_le; apply/andP; split.
+- rewrite ge0_esum; first by move=> t _; rewrite lee_fin.
+  rewrite ge_ereal_sup//= => x [X [finX _]].
+  rewrite fsumEFin // => <-.
+  rewrite lee_fin fsbig_finite//=.
+  move/finite_fsetP : finX => [J ->].
+  rewrite set_fsetK (le_trans _ (gerfin_psum J h))//.
+  by rewrite -big_fset_seq//= (le_trans _ (ler_norm_sum _ _ _))// ler_norm.
+- rewrite (eq_esum _ _ (fun x => `|f x|%:E)).
+    by move => t _; rewrite ger0_norm.
+  have [nonempty hasub] := summable_sup h.
+  rewrite psum_absE// -ereal_sup_EFin// ge_ereal_sup//= => x [X [Fs ->] <-].
+  rewrite esum_ge//;  exists [set` Fs]%classic => //.
+  rewrite fsumEFin// lee_fin (big_fset_seq (fun x => `|f x|))//=.
+  by rewrite -{1}(set_fsetK Fs) -fsbig_finite.
+Qed.
+
 (* -------------------------------------------------------------------- *)
 Lemma max_sup {R : realType} x (E : set R) :
   (E `&` ubound E)%classic x -> sup E = x.
@@ -632,18 +572,16 @@ move=> smS1 smS2; apply/summableMl => //; exists (psum S1).
 by move=> x; apply/ger1_psum.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summable_fpos (f : T -> R) :
-  summable f -> summable (fpos f).
+Lemma summable_funrpos (f : T -> R) : summable f -> summable f^\+.
 Proof.
-move/summable_abs; apply/le_summable=> x.
-by rewrite ge0_fpos /= le_fpos_norm.
+move/summable_abs; apply/le_summable => x.
+by rewrite funrpos_ge0 le_funrpos_norm.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summable_fneg (f : T -> R) :
-  summable f -> summable (fneg f).
-Proof. by move/summableN/summable_fpos/(eq_summable (fposN _)). Qed.
+Lemma summable_funrneg (f : T -> R) : summable f -> summable f^\-.
+Proof.
+by move/summableN/summable_funrpos; apply: eq_summable => x; rewrite funrposN.
+Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma summable_condl (S : T -> R) (P : pred T) :
@@ -694,6 +632,19 @@ Qed.
 
 End SummableAlg.
 
+Lemma esumEsum {T : choiceType} {R : realType} (f : T -> R) : summable f ->
+  \esum_(x in [set: T]) (f x)%:E = (sum f)%:E.
+Proof.
+move=> hs; rewrite /esum.
+rewrite EFinB; congr (_ - _)%E.
+- rewrite -esum_psum//; first exact: summable_funrpos.
+  rewrite ge0_esum/=; first by move=> x _; rewrite lee_fin.
+  by apply: PosEsum.eq_pos_esum => x _; rewrite funerpos.
+- rewrite -esum_psum//; first exact: summable_funrneg.
+  rewrite ge0_esum/=; first by move=> x _; rewrite lee_fin.
+  by apply: PosEsum.eq_pos_esum => x _; rewrite funerneg.
+Qed.
+
 (* -------------------------------------------------------------------- *)
 Section StdSum.
 Context {R : realType} (T : choiceType) (I : Type).
@@ -1131,27 +1082,29 @@ Implicit Types (S : T -> R).
 Lemma psum_sum S : (forall x, 0 <= S x) -> psum S = sum S.
 Proof.
 move=> ge0_S; rewrite /sum [X in _-X]psum_eq0 ?subr0.
-  by move=> x; rewrite fneg_ge0.
-by apply/eq_psum=> x; rewrite fpos_ge0.
+  by move=> x; rewrite (@ge0_funrnegE _ _ setT) ?in_setT.
+by apply/eq_psum=> x; rewrite (@ge0_funrposE _ _ setT) ?in_setT.
 Qed.
 
-Lemma le_sum S1 S2 :
-  summable S1 -> summable S2 -> (S1 <=1 S2) ->
-    sum S1 <= sum S2.
+Lemma le_sum S1 S2 : summable S1 -> summable S2 -> S1 <=1 S2 ->
+  sum S1 <= sum S2.
 Proof.
 move=> smS1 smS2 leS; rewrite /sum lerB //.
-  apply/le_psum/summable_fpos => // x.
-  by rewrite ge0_fpos /= le_fpos.
-apply/le_psum/summable_fneg => // x.
-rewrite -!fposN ge0_fpos le_fpos // => y.
-by rewrite lerN2.
+- apply/le_psum/summable_funrpos => // x.
+  by rewrite funrpos_ge0/= (@funrpos_le _ _ setT)//= in_setE.
+- apply/le_psum/summable_funrneg => // x.
+  rewrite -!funrposN funrpos_ge0 (@funrpos_le _ _ setT) ?in_setE//= => y _.
+  by rewrite lerN2.
 Qed.
 
-Lemma sum0 : sum (fun _ : T => 0) = 0 :> R.
-Proof. by rewrite /sum !(eq_psum fpos0, eq_psum fneg0) !psum0 subr0. Qed.
+Lemma sum0 : sum (@cst T _ 0) = 0 :> R.
+Proof.
+rewrite /sum !(eq_psum (@funrpos_cst0 _ _), eq_psum (@funrneg_cst0 _ _)).
+by rewrite !psum0 subr0.
+Qed.
 
 Lemma sumN S : sum (- S) = - sum S.
-Proof. by rewrite /sum (eq_psum (fnegN _)) (eq_psum (fposN _)) opprB. Qed.
+Proof. by rewrite /sum funrnegN funrposN opprB. Qed.
 
 Lemma sumZ S c : sum (c \*o S) = c * sum S.
 Proof.
@@ -1159,10 +1112,10 @@ rewrite (eq_sum (F2 := fun x => Num.sg c * (`|c| * S x))).
   by move=> x; rewrite mulrA -numEsg.
 transitivity (Num.sg c * sum (`|c| \*o S)).
   case: sgrP => [_|gt0_c|lt0_c]; rewrite ?Monoid.simpm.
-  + by rewrite (eq_sum (F2 := fun _ => 0)) ?sum0 // => x; rewrite !mul0r.
+  + by rewrite (eq_sum (F2 := cst 0)) ?sum0 // => x; rewrite !mul0r.
   + by apply/eq_sum=> x; rewrite mul1r.
   by rewrite mulN1r -sumN; apply/eq_sum=> x; rewrite !mulN1r.
-rewrite {1}/sum !(eq_psum (fposZ _ _), eq_psum (fnegZ _ _)) //.
+rewrite {1}/sum !(eq_psum (funrposZ _ _), eq_psum (funrnegZ _ _)) //.
 by rewrite !psumZ // -mulrBr mulrA -numEsg.
 Qed.
 
@@ -1171,10 +1124,10 @@ Lemma sumID S (P : pred T) :
     sum (fun x => (P x)%:R * S x) + sum (fun x => (~~ P x)%:R * S x).
 Proof.
 move=> sm_S; rewrite /sum addrACA -[in RHS]opprD; congr (_ - _).
-+ rewrite (psumID P); first by apply/summable_fpos.
-  by congr (_ + _); apply/eq_psum => x; rewrite fpos_natrM.
-+ rewrite (psumID P); first by apply/summable_fneg.
-  by congr (_ + _); apply/eq_psum => x; rewrite fneg_natrM.
++ rewrite (psumID P); first exact/summable_funrpos.
+  by congr (_ + _); apply/eq_psum => x; rewrite funrpos_natrM.
++ rewrite (psumID P); first exact/summable_funrneg.
+  by congr (_ + _); apply/eq_psum => x; rewrite funrneg_natrM.
 Qed.
 
 Lemma sum_finseq S (r : seq T) :
@@ -1183,13 +1136,13 @@ Lemma sum_finseq S (r : seq T) :
 Proof.
 move=> eqr domS; rewrite /sum !(psum_finseq eqr).
 + move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
-  move: xPS; rewrite /fpos normr_eq0.
+  move: xPS; rewrite /funrpos.
   by apply: contra => /eqP ->; rewrite maxxx.
 + move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
-  move: xPS; rewrite /fneg normr_eq0.
-  by apply: contra => /eqP ->; rewrite minxx.
+  move: xPS; rewrite /funrneg.
+  by apply: contra => /eqP ->; rewrite oppr0 maxxx.
 rewrite -sumrB; apply/eq_bigr=> i _.
-by rewrite !ger0_norm ?(ge0_fpos, ge0_fneg) ?fposBfneg.
+by rewrite !ger0_norm// -[in RHS](funrposBneg S).
 Qed.
 
 Lemma sum_seq1 S x : (forall y, S y != 0 -> x == y) -> sum S = S x.
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index cea1c06ff2..fdef6e5f25 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -94,6 +94,7 @@ From mathcomp Require Import mathcomp_extra interval_inference.
 (*  (\prod_(i in A) f i)%E == bigop-like notation in scope %E                 *)
 (*      maxe x y, mine x y == notation for the maximum/minimum of two         *)
 (*                            extended real numbers                           *)
+(*                   esg x == sign of x (0, -1, or +1, as an extended real)   *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Signed extended real numbers                                            *)
@@ -3026,6 +3027,30 @@ Notation mineMr := mine_pMr (only parsing).
 #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMl")]
 Notation mineMl := mine_pMl (only parsing).
 
+Section esg.
+Context {R : realDomainType}.
+Implicit Types x : \bar R.
+
+Definition esg x : \bar R := if x == 0 then 0 else if x < 0 then -1 else 1.
+
+Lemma numEesg x : x = esg x * `| x |.
+Proof.
+rewrite /esg; have [x0|x0|->] := ltgtP x 0.
+- by rewrite lte0_abs// muleNN mul1e.
+- by rewrite gte0_abs// mul1e.
+- by rewrite abse0 mule0.
+Qed.
+
+Lemma gte0_esg x : x < 0 -> esg x = -1.
+Proof. by move=> x0; rewrite /esg lt_eqF// x0. Qed.
+
+Lemma lte0_esg x: 0 < x -> esg x = 1.
+Proof. by move=> x0; rewrite /esg gt_eqF// ltNge (ltW x0). Qed.
+
+Lemma esg0 : esg 0 = 0. Proof. by rewrite /esg eqxx. Qed.
+
+End esg.
+
 Module DualAddTheoryRealDomain.
 
 Section DualERealArithTh_realDomainType.
diff --git a/rocq-mathcomp-experimental-reals.opam b/rocq-mathcomp-experimental-reals.opam
index 83179674dd..237b8e58dd 100644
--- a/rocq-mathcomp-experimental-reals.opam
+++ b/rocq-mathcomp-experimental-reals.opam
@@ -18,7 +18,7 @@ Beware that this still contains a few Admitted."""
 build: [make "-C" "experimental_reals" "-j%{jobs}%"]
 install: [make "-C" "experimental_reals" "install"]
 depends: [
-  "rocq-mathcomp-reals" { = version}
+  "rocq-mathcomp-analysis" { = version}
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
 ]
 
diff --git a/theories/ereal.v b/theories/ereal.v
index 76dfc1b728..df5b8b6d36 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -226,11 +226,14 @@ by move=> i; rewrite in_fset_set// inE; exact: ab.
 Qed.
 
 Lemma ge0_mule_fsumr (T : choiceType) x (F : T -> \bar R) (P : set T) :
-  (forall i : T, 0 <= F i) -> x * (\sum_(i \in P) F i) = \sum_(i \in P) x * F i.
+  (forall i, P i -> 0 <= F i) ->
+  x * (\sum_(i \in P) F i) = \sum_(i \in P) x * F i.
 Proof.
 move=> F0; have [->{x}|x0] := eqVneq x 0%E.
   by rewrite mul0e big1// => ? _; rewrite mul0e.
-rewrite ge0_sume_distrr//; apply: eq_fbigl => y.
+rewrite big_seq ge0_sume_distrr.
+  by move=> t; case: finite_supportP => // X XP _ _ /XP/F0.
+rewrite -big_seq; apply: eq_fbigl => y.
 rewrite !unlock; congr (_ \in fset_set _).
 apply/seteqP; rewrite /preimage; split=> [|] z/= [Pz Fz0];
   split=> //; apply: contra_not Fz0.
@@ -239,7 +242,8 @@ by move=> ->; rewrite mule0.
 Qed.
 
 Lemma ge0_mule_fsuml (T : choiceType) x (F : T -> \bar R) (P : set T) :
-  (forall i : T, 0 <= F i) -> (\sum_(i \in P) F i) * x = \sum_(i \in P) F i * x.
+  (forall i, P i -> 0 <= F i) ->
+  (\sum_(i \in P) F i) * x = \sum_(i \in P) F i * x.
 Proof.
 move=> F0; rewrite muleC ge0_mule_fsumr//.
 by apply: eq_fsbigr => i; rewrite muleC.
@@ -633,6 +637,22 @@ split=> [ge_x y Sy|ge_x _ [y Sy <-]]; rewrite ?oppeK// ?ge_x//.
 by rewrite -[y]oppeK ge_x//; exists y.
 Qed.
 
+Lemma exchange_ereal_sup {X Y : Type} (f : X -> Y -> \bar R)
+    (A : set X) (B : set Y) :
+  ereal_sup [set ereal_sup [set f x y | y in B] | x in A] =
+  ereal_sup [set ereal_sup [set f x y | x in A] | y in B].
+Proof.
+suff suf : forall (U V : Type) (g : U -> V -> \bar R) (C : set U) (D : set V),
+    ereal_sup [set ereal_sup [set g x y | y in D] | x in C] <=
+    ereal_sup [set ereal_sup [set g x y | x in C] | y in D].
+  by apply/le_anti/andP; split; exact: suf.
+move=> U V g C D.
+apply/ereal_supP => _ [x Cx <-]; apply/ereal_supP => _ [y Dy <-].
+apply: le_ereal_sup_tmp; exists (ereal_sup [set g x y | x in C]).
+- by exists y.
+- by apply: le_ereal_sup_tmp; exists (g x y) => //; exists x.
+Qed.
+
 Lemma ereal_sup_gtP S x :
   reflect (exists2 y : \bar R, S y & x < y) (x < ereal_sup S).
 Proof.
@@ -748,6 +768,52 @@ move=> XN0 r_gt0; rewrite !ereal_supEN muleN image_comp/=; congr (- _).
 by under eq_imagel do rewrite /= -muleN; rewrite -image_comp ereal_inf_pZl.
 Qed.
 
+Lemma ge0_ereal_supZl (c : \bar R) X : 0 <= c -> X != set0 ->
+  (forall x, X x -> 0 <= x) ->
+  ereal_sup [set c * x | x in X] = c * ereal_sup X.
+Proof.
+move=> c0 /[dup] Xneq0 /set0P[x Xx] X_ge0.
+case: c c0 => [r|_|//].
+- rewrite lee_fin le_eqVlt => /predU1P[<-|r0].
+  + rewrite mul0e.
+    under eq_imagel do rewrite mul0e.
+    by rewrite ereal_sup_cst.
+  + exact/(ereal_supZl Xneq0)/ltW.
+- have [Xall0|] := pselect (forall a, X a -> a = 0).
+  + rewrite [X in ereal_sup X = _](_ : _ = [set 0]%classic).
+      apply/seteqP; split.
+      * by move=> _ [z Xz <-]; rewrite (Xall0 _ Xz) mule0.
+      * by move=> y /= ->; exists x => //; rewrite (Xall0 _ Xx) mule0.
+    have -> : X = [set 0]%classic.
+      apply/seteqP; split.
+      * by move=> y /Xall0 ->.
+      * by move=> y /= ->; rewrite -(Xall0 _ Xx).
+    by rewrite ereal_sup1 mule0.
+  + rewrite -existsNE => -[y /not_implyP[Xy /eqP]].
+    rewrite neq_lt ltNge X_ge0//= => y0.
+    rewrite gt0_mulye//; first  by rewrite (lt_le_trans y0)// ereal_sup_ubound.
+    by rewrite ereal_supy//=; exists y => //; exact: gt0_mulye.
+Qed.
+
+Section ge0_ereal_supZl_range.
+Context {T : choiceType} (f : T -> nat -> \bar R).
+Hypothesis f_ge0 : forall t n, 0 <= f t n.
+
+Lemma ge0_ereal_supZl_range (c : \bar R) (x : T) : 0 <= c ->
+  c * ereal_sup (range (f x)) = ereal_sup (range (fun n => c * f x n)).
+Proof.
+move=> c0.
+rewrite [X in _ = ereal_sup X](_ : _ = [set c * y | y in range (f x)]%classic).
+  apply/seteqP; split.
+  - by move=> _ [n _ <-]; exists (f x n) => //; exists n.
+  - by move=> _ [_ [n _ <-] <-]; exists n.
+rewrite ge0_ereal_supZl//.
+- by apply/set0P; exists (f x 0%N), 0%N.
+- by move=> _ [n _ <-]; exact: f_ge0.
+Qed.
+
+End ge0_ereal_supZl_range.
+
 End ereal_supZ.
 
 Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
@@ -1541,7 +1607,7 @@ Definition ereal_loc_seq (R : numDomainType) (x : \bar R) (n : nat) :=
   end.
 
 Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
-  ereal_loc_seq x  @ \oo--> ereal_dnbhs x.
+  ereal_loc_seq x  @ \oo --> ereal_dnbhs x.
 Proof.
 move=> P; rewrite /ereal_loc_seq.
 case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first.
diff --git a/theories/esum.v b/theories/esum.v
index 486d54a46f..94352e3682 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -1,5 +1,7 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum finmap.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop reals ereal interval_inference.
 From mathcomp Require Import topology sequences normedtype numfun.
@@ -54,108 +56,154 @@ Qed.
 
 End set_of_fset_in_a_set.
 
-Section esum.
+(**md This module is for internal use. It defines `esum` in the
+  particular case of non-negative functions and is then used to
+  define a generic `esum` below, which should be preferred *)
+Module PosEsum.
+Section posesum.
 Variables (R : realFieldType) (T : choiceType).
-Implicit Types (S : set T) (a : T -> \bar R).
+Implicit Types (S : set T) (f g : T -> \bar R).
 
-Definition esum S a := ereal_sup [set \sum_(x \in A) a x | A in fsets S].
+Definition pos_esum S g := ereal_sup [set \sum_(x \in B) g x | B in fsets S].
 
-Local Notation "\esum_ ( i 'in' P ) A" := (esum P (fun i => A)).
+Local Notation "\esum_ ( i 'in' P ) A" := (pos_esum P (fun i => A)).
 
-Lemma esum_set0 a : \esum_(i in set0) a i = 0.
+Lemma pos_esum_set0 f : \esum_(i in set0) f i = 0.
 Proof.
-rewrite /esum fsets0 [X in ereal_sup X](_ : _ = [set 0%E]) ?ereal_sup1//.
+rewrite /pos_esum fsets0 [X in ereal_sup X](_ : _ = [set 0%E]) ?ereal_sup1//.
 apply/seteqP; split=> [x [_ /= ->]|x]; first by rewrite fsbig_set0.
 by move=> -> /=; exists set0 => //; rewrite fsbig_set0.
 Qed.
 
-End esum.
+Lemma ge0_pos_esum_funeneg S f : (forall x, S x -> 0 <= f x) ->
+  \esum_(i in S) f^\- i = 0.
+Proof.
+move=> a0; rewrite /pos_esum [X in ereal_sup X](_ : _ = [set 0]) ?ereal_sup1//.
+apply/seteqP; split => [/= x /= [A SA <-]|].
+  rewrite fsbig1//= => t At.
+  rewrite (@ge0_funenegE _ _ A)//; last exact/mem_set.
+  by move=> u; case: SA => _ => /[apply] /a0.
+rewrite sub1set inE/=; exists set0; first exact: fsets_set0.
+by rewrite fsbig_set0.
+Qed.
 
-Notation "\esum_ ( i 'in' P ) F" := (esum P (fun i => F)) : ring_scope.
+Lemma eq_pos_esum S f g : {in S, f =1 g} ->
+  \esum_(i in S) f i = \esum_(i in S) g i.
+Proof.
+move=> eq_fg; rewrite /pos_esum; congr ereal_sup.
+apply/seteqP; split => [_/= [B SB <-]|_/= [B SB <-]].
+- exists B => //; apply: eq_fsbigr => i iB.
+  exact/esym/eq_fg/mem_set/SB.2/set_mem.
+- exists B => //; apply: eq_fsbigr => i iB.
+  exact/eq_fg/mem_set/SB.2/set_mem.
+Qed.
 
-Section esum_realType.
+Lemma ge0_pos_esum_funepos S f : (forall x, S x -> 0 <= f x) ->
+  \esum_(i in S) f^\+ i = \esum_(i in S) f i.
+Proof. by move=> a0; apply: eq_pos_esum; exact: ge0_funeposE. Qed.
+
+Lemma pos_esum1 S f : (forall i, S i -> f i = 0) -> \esum_(i in S) f i = 0.
+Proof.
+move=> a0; rewrite /pos_esum (_ : [set _ | _ in _] = [set 0]) ?ereal_sup1//.
+apply/seteqP; split=> x //= => [[X [finX XI]] <-|->].
+  by rewrite fsbig1// => i /XI/a0.
+by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0.
+Qed.
+
+End posesum.
+Arguments eq_pos_esum {R T} S f g.
+
+Section posesum_realType.
 Variables (R : realType) (T : choiceType).
-Implicit Types (a : T -> \bar R).
+Implicit Types (S : set T) (f g : T -> \bar R).
 
-Lemma esum_ge0 (S : set T) a :
-  (forall x, S x -> 0 <= a x) -> 0 <= \esum_(i in S) a i.
+Local Notation "\esum_ ( i 'in' P ) A" := (pos_esum P (fun i => A)).
+
+Lemma pos_esum_ge0 S f : 0 <= \esum_(i in S) f i.
 Proof.
-move=> a0; apply: ereal_sup_ubound.
+rewrite /pos_esum ereal_sup_ubound//.
 by exists set0; [exact: fsets_set0|rewrite fsbig_set0].
 Qed.
 
-Lemma esum_fset (F : set T) a : finite_set F ->
-    (forall i, i \in F -> 0 <= a i) ->
-  \esum_(i in F) a i = \sum_(i \in F) a i.
+Lemma pos_esum_fset S f : finite_set S -> (forall i, S i -> 0 <= f i) ->
+  \esum_(i in S) f i = \sum_(i \in S) f i.
 Proof.
-move=> finF f0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  by apply: ereal_sup_ubound; exists F => //; exact: fsets_self.
+move=> finS f0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
+  by apply: ereal_sup_ubound; exists S => //; exact: fsets_self.
 apply: ge_ereal_sup => /= ? -[F' [finF' F'F] <-].
 apply/lee_fsum_nneg_subset => //; first exact/subsetP.
-by  move=> t; rewrite inE/= => /andP[_] /f0.
+by  move=> t; rewrite inE/= => /andP[_] /set_mem/f0.
 Qed.
 
-Lemma esum_set1 t a : 0 <= a t -> \esum_(i in [set t]) a i = a t.
+Lemma pos_esum_set1 t f : 0 <= f t -> \esum_(i in [set t]) f i = f t.
 Proof.
-by move=> ?; rewrite esum_fset// ?fset_set1// ?fsbig_set1// => t' /[!inE] ->.
+by move=> ?; rewrite pos_esum_fset// ?fset_set1// ?fsbig_set1// => t' ->.
 Qed.
 
-End esum_realType.
-
-Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) :
-  (forall i, D i -> a i = 0) -> \esum_(i in D) a i = 0.
-Proof.
-move=> a0; rewrite /esum (_ : [set _ | _ in _] = [set 0]) ?ereal_sup1//.
-apply/seteqP; split=> x //= => [[X [finX XI]] <-|->].
-  by rewrite fsbig1// => i /XI/a0.
-by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0.
-Qed.
-
-Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x :
-  (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) ->
+Lemma pos_esum_ge (T1 : choiceType) (I : set T1) (a : T1 -> \bar R) x :
+  (exists2 X : set T1, fsets I X & x <= \sum_(i \in X) a i) ->
   x <= \esum_(i in I) a i.
 Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed.
 
-Lemma le_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
-  (forall i, I i -> a i <= b i) ->
-  \esum_(i in I) a i <= \esum_(i in I) b i.
-Proof.
-move=> le_ab; rewrite ge_ereal_sup => //= _ [X [finX XI]] <-; rewrite esum_ge//.
-by exists X => //; apply: lee_fsum => // t /XI /le_ab.
-Qed.
-
-Lemma eq_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
-  (forall i, I i -> a i = b i) ->
-  \esum_(i in I) a i = \esum_(i in I) b i.
-Proof. by move=> e; apply/eqP; rewrite eq_le !le_esum// => i Ii; rewrite e. Qed.
-
-Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
+Lemma le_pos_esum S f g : (forall i, S i -> f i <= g i) ->
+  \esum_(i in S) f i <= \esum_(i in S) g i.
+Proof.
+move=> fg; rewrite ge_ereal_sup => //= _ [X [finX XS]] <-.
+by rewrite pos_esum_ge//; exists X => //; apply: lee_fsum => // t /XS /fg.
+Qed.
+
+Lemma pos_esumZ S f (c : \bar R) : 0 <= c -> (forall t, S t -> 0 <= f t) ->
+  \esum_(t in S) c * f t = c * \esum_(t in S) f t.
+Proof.
+rewrite le_eqVlt => /predU1P[<- _|c0 f0].
+  by rewrite mul0e pos_esum1// => ? _; rewrite mul0e.
+apply/eqP; rewrite eq_le; apply/andP; split.
+- rewrite ge_ereal_sup//= => _ [X [finX XA]] <-.
+  rewrite -ge0_mule_fsumr; first by move=> t /XA /f0.
+  by rewrite (lee_wpmul2l (ltW c0))// pos_esum_ge//; exists X.
+- case: c c0 => [s s0|_|//].
+  + rewrite -lee_pdivlMl// ge_ereal_sup//= => _ [X [finX XI]] <-.
+    rewrite lee_pdivlMl// ge0_mule_fsumr//; first by move=> t /XI /f0.
+    by rewrite pos_esum_ge//; exists X.
+  + have : 0 <= \esum_(x in S) f x by apply: pos_esum_ge0 => ? ?; exact: f0.
+    rewrite [in X in X -> _]le_eqVlt => /predU1P[<-|suma0].
+    * by rewrite mule0 pos_esum_ge0// => ? ?; rewrite mule_ge0.
+    * rewrite gt0_mulye//.
+      have [y [B fsetsTB yE y0]] := ereal_sup_gt suma0.
+      rewrite leye_eq; apply/eqP/eq_infty => r; rewrite pos_esum_ge//.
+      exists B => //; rewrite -ge0_mule_fsumr//.
+        by move=> i Bi; rewrite f0//; case: fsetsTB => _ /(_ _ Bi).
+      by rewrite yE gt0_mulye// leey.
+Qed.
+
+Lemma pos_esumD (T1 : choiceType) (I : set T1) (a b : T1 -> \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.
-move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split.
+move=> ag0 bg0.
+apply/eqP; rewrite eq_le; apply/andP; split.
   rewrite ge_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=.
   by rewrite leeD// ereal_sup_ubound//=; 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//.
+  rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: pos_esum.
+  rewrite leye_eq; apply/eqP/eq_infty => y; rewrite pos_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.
+  by rewrite addeC (eq_pos_esum _ _ _ (fun _ _ => addeC _ _)) saoo.
 rewrite -leeBrDr// ge_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//.
+  apply/fin_numPn; right; apply/eqP; rewrite -leye_eq pos_esum_ge//.
   by exists X; rewrite // sa.
 rewrite leeBrDr// addeC -leeBrDr// ge_ereal_sup//= => _ [Y [finY YI]] <-.
-rewrite leeBrDr// addeC esum_ge//; exists (X `|` Y).
+rewrite leeBrDr// addeC pos_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.
@@ -165,9 +213,8 @@ rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset ?finite_setU//=.
   by move=> /andP[_] /[!inE] /XI/bg0.
 Qed.
 
-Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T)
-    (a : T -> \bar R) :
-  \esum_(i in I) a i = \esum_(i in [set: T]) if i \in I then a i else 0.
+Lemma pos_esum_mkcond {T1 : choiceType} (I : set T1) (a : T1 -> \bar R) :
+  \esum_(i in I) a i = \esum_(i in [set: T1]) if i \in I then a i else 0.
 Proof.
 apply/eqP; rewrite eq_le !ge_ereal_sup//= => _ [X [finX XI]] <-.
   rewrite ereal_sup_ubound//; exists X => //; apply: eq_fsbigr => x /[!inE] Xx.
@@ -178,60 +225,33 @@ rewrite ereal_sup_ubound//=; exists [set` Y].
 by rewrite fsbig_finite// set_fsetK.
 Qed.
 
-Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T)
-    (a : T -> \bar R) :
-  \esum_(i in I `&` J) a i = \esum_(i in I) if i \in J then a i else 0.
-Proof.
-rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
-by rewrite in_setI; case: (i \in I) (i \in J) => [] [].
-Qed.
-
-Lemma esum_mkcondl [R : realType] [T : choiceType] (I J : set T)
-    (a : T -> \bar R) :
-  \esum_(i in I `&` J) a i = \esum_(i in J) if i \in I then a i else 0.
-Proof.
-rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
-by rewrite in_setI; case: (i \in I) (i \in J) => [] [].
-Qed.
-
-Lemma esumID (R : realType) (I : choiceType) (B : set I) (A : set I)
-  (F : I -> \bar R) :
-  (forall i, A i -> F i >= 0) ->
-  \esum_(i in A) F i = (\esum_(i in A `&` B) F i) +
-                        (\esum_(i in A `&` ~` B) F i).
-Proof.
-move=> F0; rewrite !esum_mkcondr -esumD; do ?by move=> i /F0; case: ifP.
-by apply: eq_esum=> i; rewrite in_setC; case: ifP; rewrite /= (adde0, add0e).
-Qed.
-Arguments esumID {R I}.
-
-Lemma esum_sum [R : realType] [T1 T2 : choiceType]
-    (I : set T1) (r : seq T2) (P : pred T2) (a : T1 -> T2 -> \bar R) :
+Lemma pos_esum_sum {T1 T2 : choiceType} (I : set T1) (r : seq T2) (P : pred T2)
+    (a : T1 -> T2 -> \bar R) :
   (forall i j, I i -> P j -> 0 <= a i j) ->
   \esum_(i in I) \sum_(j <- r | P j) a i j =
   \sum_(j <- r | P j) \esum_(i in I) a i j.
 Proof.
 move=> a_ge0; elim: r => [|j r IHr]; rewrite ?(big_nil, big_cons)// -?IHr.
-  by rewrite esum1// => i; rewrite big_nil.
+  by rewrite pos_esum1// => i; rewrite big_nil.
 case: ifPn => Pj; last first.
-  by apply: eq_esum => i Ii; rewrite big_cons (negPf Pj).
+  by apply: eq_pos_esum => i Ii; rewrite big_cons (negPf Pj).
 have aj_ge0 i : I i -> a i j >= 0 by move=> ?; apply: a_ge0.
-rewrite -esumD//; first by move=> i Ii; apply: sume_ge0 => *; apply: a_ge0.
-by apply: eq_esum => i Ii; rewrite big_cons Pj.
+rewrite -pos_esumD//; first by move=> i Ii; apply: sume_ge0 => *; apply: a_ge0.
+by apply: eq_pos_esum => i Ii; rewrite big_cons Pj.
 Qed.
 
-Lemma esum_esum [R : realType] [T1 T2 : choiceType]
-    (I : set T1) (J : T1 -> set T2) (a : T1 -> T2 -> \bar R) :
+Lemma pos_esum_esum {T1 T2 : choiceType} (I : set T1) (J : T1 -> set T2)
+    (a : T1 -> T2 -> \bar R) :
   (forall i j, I i -> J i j -> 0 <= a i j) ->
   \esum_(i in I) \esum_(j in J i) a i j = \esum_(k in I `*`` J) a k.1 k.2.
 Proof.
 move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split.
   apply: ge_ereal_sup => /= _ [X [finX XI]] <-.
-  under eq_fsbigr do rewrite esum_mkcond.
-  rewrite fsbig_finite//= big_seq -esum_sum.
+  under eq_fsbigr do rewrite pos_esum_mkcond.
+  rewrite fsbig_finite//= big_seq -pos_esum_sum.
     move=> i j _ /[!in_fset_set]// /[!inE] /XI Ij.
     by case: ifPn => // /[!inE] /a_ge0-/(_ Ij).
-  under eq_esum do rewrite -big_seq -big_mkcond/=.
+  under eq_pos_esum do rewrite -big_seq -big_mkcond/=.
   apply: ge_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ubound => /=.
   set XYJ := [set z | z \in X `*` Y /\ z.2 \in J z.1].
   have ? : finite_set XYJ.
@@ -246,7 +266,7 @@ move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split.
     by exists y => //; rewrite !inE mem_set// in_fset_set// mem_set.
   move=> [t1]; rewrite !inE andbT/= in_fset_set// inE => Xt1.
   by move=> [t2]; rewrite !inE in_fset_set /XYJ//= =>/andP[/[!inE] ? ?] [-> ->].
-apply: ge_ereal_sup => _ /= [X/= [finX XIJ]] <-; apply: esum_ge.
+apply: ge_ereal_sup => _ /= [X/= [finX XIJ]] <-; apply: pos_esum_ge.
 exists X.`1; first by split=> [|x [y /XIJ[]//]]; exact: finite_set_fst.
 apply: (@le_trans _ _
     (\sum_(i <- fset_set X.`1) \sum_(j <- fset_set X.`2 | j \in J i) a i j)).
@@ -278,10 +298,272 @@ rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply/eq_fbigl => j.
 by rewrite in_fset_set// !inE/= in_setI in_fset_set//; exact: finite_set_snd.
 Qed.
 
+Lemma reindex_pos_esum (T1 T2 : choiceType) (P : set T1) (Q : set T2)
+    (e : T1 -> T2) (a : T2 -> \bar R) : set_bij P Q e ->
+  \esum_(j in Q) a j = \esum_(i in P) a (e i).
+Proof.
+elim/choicePpointed: T1 => T1 in e P *.
+  rewrite !emptyE => /Pbij[{}e ->].
+  by rewrite -[in LHS](image_eq e) image_set0 !pos_esum_set0.
+elim/choicePpointed: T2 => T2 in a e Q *; first by have := no (e point).
+move=> /(@pPbij _ _ _)[{}e ->].
+gen have le_esum : T1 T2 a P Q e /
+    \esum_(j in Q) a j <= \esum_(i in P) a (e i); last first.
+  apply/eqP; rewrite eq_le le_esum//=.
+  rewrite [leRHS](_ : _ = \esum_(j in Q) a (e (e^-1%FUN j))).
+    by apply: eq_pos_esum => i Qi; rewrite invK.
+  by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS.
+rewrite ge_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ubound => //=.
+exists [set` (e^-1 @` (fset_set X))%fset].
+  split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset.
+  by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS.
+rewrite fsbig_finite//= set_fsetK big_imfset => //=.
+  move=> x y; rewrite !in_fset_set// !inE => /XQ ? /XQ ? /(congr1 e).
+  by rewrite !invK ?inE.
+by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE.
+Qed.
+
+End posesum_realType.
+Arguments reindex_pos_esum {R T1 T2} P Q e a.
+
+End PosEsum.
+
+Section esum.
+Variables (R : realFieldType) (T : choiceType).
+Implicit Types (S : set T) (f g : T -> \bar R).
+
+Import PosEsum.
+
+Definition esum S f := pos_esum S f^\+ - pos_esum S f^\-.
+
+Local Notation "\esum_ ( i 'in' P ) A" := (esum P (fun i => A)).
+
+Lemma ge0_esum S f : (forall x, S x -> 0 <= f x) ->
+  \esum_(i in S) f i = ereal_sup [set \sum_(x \in B) f x | B in fsets S].
+Proof.
+by move=> ?; rewrite /esum ge0_pos_esum_funepos// ge0_pos_esum_funeneg// sube0.
+Qed.
+
+Lemma esum_set0 f : \esum_(i in set0) f i = 0.
+Proof. by rewrite /esum !pos_esum_set0 subee. Qed.
+
+Lemma esumN S f : (forall x, S x -> 0 <= f x) ->
+  \esum_(x in S) - f x = - \esum_(i in S) f i.
+Proof.
+move=> f0.
+rewrite [in RHS]ge0_esum// [LHS]/esum [X in X - _ = _]PosEsum.pos_esum1 ?add0r.
+  by move=> t /mem_set At; rewrite funeposN (@ge0_funenegE _ _ S).
+rewrite /PosEsum.pos_esum; congr (- ereal_sup _).
+apply: eq_imagel => B SB; apply: eq_fsbigr => x xB.
+rewrite funenegN (@ge0_funeposE _ _ B)// => y By; apply: f0.
+by case: SB => _; exact.
+Qed.
+
+End esum.
+
+Notation "\esum_ ( i 'in' P ) F" := (esum P (fun i => F)) : ring_scope.
+
+Section esum_realType.
+Variables (R : realType) (T : choiceType).
+Implicit Types (S : set T) (f : T -> \bar R).
+
+Lemma le_esum S f g : (forall x, S x -> 0 <= f x) ->
+  (forall x, S x -> f x <= g x) ->
+  \esum_(x in S) f x <= \esum_(x in S) g x.
+Proof.
+move=> f0 leS; have g0 x : S x -> 0 <= g x.
+  by move=> /[dup] Ax /leS; apply: le_trans; exact: f0 Ax.
+by rewrite !ge0_esum// PosEsum.le_pos_esum.
+Qed.
+
+Lemma esum_ge0 S f : (forall x, S x -> 0 <= f x) -> 0 <= \esum_(i in S) f i.
+Proof. by move=> f0; rewrite ge0_esum// PosEsum.pos_esum_ge0. Qed.
+
+Lemma esum_fset S f : finite_set S -> (forall i, S i -> 0 <= f i) ->
+  \esum_(i in S) f i = \sum_(i \in S) f i.
+Proof. by move=> finF f0; rewrite ge0_esum//; exact: PosEsum.pos_esum_fset. Qed.
+
+End esum_realType.
+
+Lemma esum1 {R : realFieldType} {I : choiceType} (D : set I) (f : I -> \bar R) :
+  (forall i, D i -> f i = 0) -> \esum_(i in D) f i = 0.
+Proof.
+move=> a0; rewrite ge0_esum; last exact: PosEsum.pos_esum1.
+by move=> i /a0 ->.
+Qed.
+
+Lemma eq_esum {R : realFieldType} {T : choiceType} (A : set T)
+    (f g : T -> \bar R) : (forall i, A i -> f i = g i) ->
+  \esum_(i in A) f i = \esum_(i in A) g i.
+Proof.
+move=> e; congr (_ - _).
+- by apply: PosEsum.eq_pos_esum => i /set_mem/e abi; rewrite !funeposE abi.
+- by apply: PosEsum.eq_pos_esum => i /set_mem/e abi; rewrite !funenegE abi.
+Qed.
+Arguments eq_esum {R T} A f g.
+
+Section esum_cond.
+Context {R : realType} {T : choiceType}.
+Implicit Types (A B : set T) (f : T -> \bar R).
+
+Lemma esum_mkcond A f :
+  \esum_(i in A) f i = \esum_(i in [set: T]) if i \in A then f i else 0.
+Proof.
+rewrite /esum; congr (_ - _); rewrite PosEsum.pos_esum_mkcond;
+  congr PosEsum.pos_esum; apply/funext => x/=.
+- by rewrite funepos_restrict.
+- by rewrite funeneg_restrict.
+Qed.
+
+Lemma esum_mkcondr A B f :
+  \esum_(i in A `&` B) f i = \esum_(i in A) if i \in B then f i else 0.
+Proof.
+rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
+by rewrite in_setI; case: (i \in A) (i \in B) => [] [].
+Qed.
+
+Lemma esum_mkcondl A B f :
+  \esum_(i in A `&` B) f i = \esum_(i in B) if i \in A then f i else 0.
+Proof.
+rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
+by rewrite in_setI; case: (i \in A) (i \in B) => [] [].
+Qed.
+
+Lemma esum_if_eq_op f x :
+  \esum_(y in [set: T]) (if x == y then f y else 0) = \esum_(i in [set x]) f i.
+Proof.
+rewrite [RHS]esum_mkcond.
+by under [in RHS]eq_esum do rewrite in_set1 eq_sym.
+Qed.
+
+End esum_cond.
+
+Section esum_set1.
+Context {R : realType} {T : choiceType}.
+Implicit Types (f : T -> \bar R).
+
+Let ge0_esum_set1 t f : 0 <= f t -> \esum_(i in [set t]) f i = f t.
+Proof.
+move=> ?; rewrite ge0_esum; first by move=> x ->.
+exact: PosEsum.pos_esum_set1.
+Qed.
+
+Lemma esum_set1 f x : \esum_(i in [set x]) f i = f x.
+Proof.
+rewrite /esum.
+rewrite (PosEsum.eq_pos_esum _ _ (fun y => if x == y then f^\+ y else 0)).
+  by move=> i /[!inE] ->; rewrite eqxx.
+rewrite [X in _ - X](PosEsum.eq_pos_esum _ _
+    (fun y => if x == y then f^\- y else 0)).
+  by move=> i /[!inE] ->; rewrite eqxx.
+rewrite -[X in X - _]ge0_esum; first by move=> t _; case: ifPn.
+rewrite -[X in _ - X]ge0_esum; first by move=> t _; case: ifPn.
+have [Sx0|Sx0] := comparable_ltP (comparableT (f x) 0)%E.
+- rewrite esum1; first by move => t //= ->; rewrite eqxx funeposE// max_r// ltW.
+  rewrite ge0_esum_set1 eqxx ?funeneg_ge0//.
+  by rewrite funenegE max_l// ?oppeK ?add0e// leeNr oppe0 ltW.
+- rewrite ge0_esum_set1 eqxx ?funepos_ge0//.
+  rewrite esum1; first by move => t ->; rewrite funenegE eqxx max_r// oppe_le0.
+  by rewrite funeposE max_l// sube0.
+Qed.
+
+End esum_set1.
+
+Lemma esum_ge {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) x :
+  (forall i, I i -> 0 <= f i) ->
+  (exists2 X : set T, fsets I X & x <= \sum_(i \in X) f i) ->
+  x <= \esum_(i in I) f i.
+Proof. by move=> f0 If; rewrite ge0_esum// PosEsum.pos_esum_ge. Qed.
+
+Lemma esum_eq0P {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R) :
+  (forall i, A i -> 0 <= f i) ->
+  \esum_(x in A) f x = 0 -> forall x, A x -> f x = 0.
+Proof.
+move=> f0; rewrite ge0_esum// => suma0 x Ax.
+apply/eqP; rewrite eq_le f0//= -suma0 ereal_sup_ubound//=.
+exists [set x]; first by split => // t ->.
+by rewrite -esum_set1 esum_fset// => i ->; exact: f0.
+Qed.
+
+Section esumZ.
+Context {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R).
+
+Let ge0_esumZ c : 0 <= c -> (forall t, A t -> 0 <= f t) ->
+  \esum_(t in A) c * f t = c * \esum_(t in A) f t.
+Proof.
+rewrite le_eqVlt => /predU1P[<- _|c0 f0].
+  by rewrite mul0e esum1// => ? _; rewrite mul0e.
+rewrite [in LHS]ge0_esum; first by move=> x /f0 ax0; rewrite ?mule_ge0// ltW.
+by rewrite ge0_esum//; apply: PosEsum.pos_esumZ => //; exact: ltW.
+Qed.
+
+Lemma esumZ c : (forall x, A x -> 0 <= f x) ->
+  \esum_(x in A) c * f x = c * \esum_(x in A) f x.
+Proof.
+move=> h; rewrite (eq_esum _ _ (fun x => esg c * (`|c| * f x))).
+  by move=> x; rewrite muleA -numEesg.
+transitivity (esg c * \esum_(x in A) `|c| * f x).
+  have [hc|hc|->] := comparable_ltgtP (comparableT c 0).
+  - rewrite {1}lte0_abs// gte0_esg// (eq_esum _ _ (fun x => - (- c * f x))).
+      by move => ?; rewrite mulN1e.
+    rewrite mulN1e -esumN; last by rewrite lte0_abs.
+    by move=> ? ?; rewrite mule_ge0//; exact: h.
+  - rewrite gte0_abs// lte0_esg// mul1e (eq_esum _ _ (fun x => c * f x))//.
+    by move=> ?; rewrite mul1e.
+  - under eq_esum do rewrite esg0 mul0e.
+    by rewrite esg0 mul0e esum1.
+by rewrite (eq_esum _ _ (fun x => `|c| * f x))// ge0_esumZ// muleA -numEesg.
+Qed.
+
+End esumZ.
+
+Lemma esumD {R : realType} {T : choiceType} (I : set T) (f g : T -> \bar R) :
+  (forall i, I i -> 0 <= f i) -> (forall i, I i -> 0 <= g i) ->
+  \esum_(i in I) (f i + g i) = \esum_(i in I) f i + \esum_(i in I) g i.
+Proof.
+move=> f0 g0; rewrite [in LHS]ge0_esum//.
+  by move=> *; rewrite adde_ge0 ?f0 ?g0.
+by do 2 rewrite ge0_esum//; exact: PosEsum.pos_esumD.
+Qed.
+
+Lemma esumID {R : realType} {T : choiceType} (B A : set T) (f : T -> \bar R) :
+  (forall i, A i -> f i >= 0) ->
+  \esum_(i in A) f i = (\esum_(i in A `&` B) f i) +
+                       (\esum_(i in A `&` ~` B) f i).
+Proof.
+move=> f0; rewrite !esum_mkcondr -esumD; do ?by move=> i /f0; case: ifP.
+by apply: eq_esum=> i; rewrite in_setC; case: ifP; rewrite /= (adde0, add0e).
+Qed.
+Arguments esumID {R T}.
+
+Lemma exchange_esum_sum [R : realType] [T1 T2 : choiceType]
+    (I : set T1) (r : seq T2) (P : pred T2) (f : T1 -> T2 -> \bar R) :
+  (forall i j, I i -> P j -> 0 <= f i j) ->
+  \esum_(i in I) \sum_(j <- r | P j) f i j =
+  \sum_(j <- r | P j) \esum_(i in I) f i j.
+Proof.
+move=> f0; rewrite ge0_esum; first by move=> *; apply: sume_ge0 => t /f0; exact.
+rewrite [LHS]PosEsum.pos_esum_sum//; apply: eq_bigr => t Pt.
+by rewrite ge0_esum// => x /f0; exact.
+Qed.
+#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `exchange_esum_sum`")]
+Notation esum_sum := exchange_esum_sum (only parsing).
+
+Lemma esum_esum [R : realType] [T1 T2 : choiceType]
+    (I : set T1) (J : T1 -> set T2) (f : T1 -> T2 -> \bar R) :
+  (forall i j, I i -> J i j -> 0 <= f i j) ->
+  \esum_(i in I) \esum_(j in J i) f i j = \esum_(k in I `*`` J) f k.1 k.2.
+Proof.
+move=> f0; rewrite [RHS]ge0_esum/=; first by move=> [x y]/= [Ix Jxy]; exact: f0.
+rewrite -[RHS]PosEsum.pos_esum_esum// ge0_esum.
+  by move=> x Ix; rewrite esum_ge0// => t /f0; exact.
+apply: PosEsum.eq_pos_esum => x Ix.
+by rewrite ge0_esum// => t /f0; apply; exact/set_mem.
+Qed.
+
 Lemma lee_sum_fset_nat (R : realDomainType)
     (f : (\bar R)^nat) (F : {fset nat}) n (P : pred nat) :
-    (forall i, P i -> 0%E <= f i) ->
-    [set` F] `<=` `I_n ->
+ (forall i, P i -> 0%E <= f i) -> [set` F] `<=` `I_n ->
   \sum_(i <- F | P i) f i <= \sum_(0 <= i < n | P i) f i.
 Proof.
 move=> f0 Fn; rewrite [leRHS](bigID (mem F))/=.
@@ -296,8 +578,7 @@ Qed.
 Arguments lee_sum_fset_nat {R f} F n P.
 
 Lemma lee_sum_fset_lim (R : realType) (f : (\bar R)^nat) (F : {fset nat})
-    (P : pred nat) :
-  (forall i, P i -> 0%E <= f i) ->
+    (P : pred nat) : (forall i, P i -> 0%E <= f i) ->
   \sum_(i <- F | P i) f i <= \sum_(i <oo | P i) f i.
 Proof.
 move=> f0; pose n := (\max_(k <- F) k).+1.
@@ -312,50 +593,49 @@ Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) :
   (forall n, P n -> 0 <= a n) ->
   \sum_(i <oo | P i) a i = \esum_(i in [set x | P x]) a i.
 Proof.
-move=> a0; apply/eqP; rewrite eq_le; apply/andP; split.
-  apply: (lime_le (is_cvg_nneseries_cond (fun n _ => a0 n))); apply: nearW => n.
+move=> a0; rewrite ge0_esum//.
+apply/eqP; rewrite eq_le; apply/andP; split.
+- apply: (lime_le (is_cvg_nneseries_cond (fun n _ => a0 n))); apply: nearW => n.
   apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i]%fset].
     split; first exact: finite_fset.
     by move=> /= k /imfsetP[/= i]; rewrite inE => + ->.
   rewrite fsbig_finite//= set_fsetK big_imfset/=.
     by move=> ? ? ? ? /val_inj.
   by rewrite big_filter big_enum_cond/= big_mkord.
-apply: ge_ereal_sup => _ [/= F [finF PF] <-].
-rewrite fsbig_finite//= -(big_rmcond_in P)/=; last exact: lee_sum_fset_lim.
-by move=> k; rewrite in_fset_set// inE => /PF ->.
+- apply: ge_ereal_sup => _ [/= F [finF PF] <-].
+  rewrite fsbig_finite//= -(big_rmcond_in P)/=; last exact: lee_sum_fset_lim.
+  by move=> k; rewrite in_fset_set// inE => /PF ->.
 Qed.
 
 Lemma nneseries_esumT {R : realType} (a : nat -> \bar R) :
   (forall n, 0 <= a n) -> \sum_(i <oo) a i = \esum_(i in [set: nat]) a i.
 Proof. by move=> a0; rewrite nneseries_esum// set_true. Qed.
 
-Lemma reindex_esum (R : realType) (T T' : choiceType)
-    (P : set T) (Q : set T') (e : T -> T') (a : T' -> \bar R) :
-    set_bij P Q e ->
+Lemma reindex_esum {R : realType} {T T' : choiceType} (P : set T) (Q : set T')
+    (e : T -> T') (a : T' -> \bar R) : set_bij P Q e ->
   \esum_(j in Q) a j = \esum_(i in P) a (e i).
 Proof.
-elim/choicePpointed: T => T in e P *.
-  rewrite !emptyE => /Pbij[{}e ->].
-  by rewrite -[in LHS](image_eq e) image_set0 !esum_set0.
-elim/choicePpointed: T' => T' in a e Q *; first by have := no (e point).
-move=> /(@pPbij _ _ _)[{}e ->].
-gen have le_esum : T T' a P Q e /
-    \esum_(j in Q) a j <= \esum_(i in P) a (e i); last first.
-  apply/eqP; rewrite eq_le le_esum//=.
-  rewrite [leRHS](_ : _ = \esum_(j in Q) a (e (e^-1%FUN j))).
-    by apply: eq_esum => i Qi; rewrite invK ?inE.
-  by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS.
-rewrite ge_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ubound => //=.
-exists [set` (e^-1 @` (fset_set X))%fset].
-  split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset.
-  by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS.
-rewrite fsbig_finite//= set_fsetK big_imfset => //=.
-  move=> x y; rewrite !in_fset_set// !inE => /XQ ? /XQ ? /(congr1 e).
-  by rewrite !invK ?inE.
-by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE.
+move=> PQe; rewrite /esum; congr (_ - _).
+- rewrite (PosEsum.reindex_pos_esum P Q e)//; congr PosEsum.pos_esum.
+  by apply/funext => i; rewrite !funeposE.
+- rewrite (PosEsum.reindex_pos_esum P Q e)//; congr PosEsum.pos_esum.
+  by apply/funext => i; rewrite !funenegE.
 Qed.
 Arguments reindex_esum {R T T'} P Q e a.
 
+Lemma exchange_esum [R : realType] [T U : choiceType] A B
+    (f : T -> U -> \bar R): (forall i j, 0 <= f i j) ->
+  \esum_(x in A) \esum_(y in B) f x y = \esum_(y in B) \esum_(x in A) f x y.
+Proof.
+move=> f0; rewrite !esum_esum//=.
+rewrite (reindex_esum (fun z => A z.1 /\ B z.2) (fun z => B z.1 /\ A z.2)
+  swap)//=.
+split.
+- by move=> [i j]/= [].
+- by move=> [i1 i2] [j1 j2] /[!inE] -[Ai1 Bi2] [Aj1 Bj2] [-> ->].
+- by move=> [i j]/= [Bi Aj]; exists (j, i).
+Qed.
+
 Section nneseries_interchange.
 Local Open Scope ereal_scope.
 
@@ -495,7 +775,9 @@ Qed.
 Lemma summableD D f g : summable D f -> summable D g -> summable D (f \+ g).
 Proof.
 move=> Df Dg; apply: le_lt_trans (lte_add_pinfty Df Dg).
-by rewrite -esumD//; apply le_esum => t Dt; exact: lee_abs_add.
+rewrite -esumD//; do 2 rewrite ge0_esum//.
+  by move=> x Dx; rewrite adde_ge0.
+by apply: PosEsum.le_pos_esum => t Dt; exact: lee_abs_add.
 Qed.
 
 Lemma summableN D f : summable D f = summable D (\- f).
@@ -508,13 +790,17 @@ Proof. by move=> Df; rewrite summableN; exact: summableD. Qed.
 
 Lemma summable_funepos D f : summable D f -> summable D f^\+.
 Proof.
-apply: le_lt_trans; apply: le_esum => t Dt.
+apply: le_lt_trans.
+do 2 rewrite ge0_esum//.
+apply: PosEsum.le_pos_esum => t Dt.
 by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl.
 Qed.
 
 Lemma summable_funeneg D f : summable D f -> summable D f^\-.
 Proof.
-apply: le_lt_trans; apply: le_esum => t Dt.
+apply: le_lt_trans.
+do 2 rewrite ge0_esum//.
+apply: PosEsum.le_pos_esum => t Dt.
 by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
 Qed.
 
@@ -526,7 +812,7 @@ Section summable_nat.
 Local Open Scope ereal_scope.
 Variable R : realType.
 
-Lemma summable_fine_sum r (P : pred nat) (f : nat -> \bar R) : summable P f ->
+Lemma summable_fine_sum r (P : pred nat) (f : (\bar R)^nat) : summable P f ->
   (\sum_(0 <= k < r | P k) fine (f k))%R = fine (\sum_(0 <= k < r | P k) f k).
 Proof.
 move=> Pf; elim: r => [|r ih]; first by rewrite !big_nil.
@@ -549,7 +835,8 @@ rewrite summable_fine_sum// -lee_fin fineK//.
 rewrite fineK//.
   rewrite nneseries_esum// fin_numElt; apply/andP; split.
     by rewrite (@lt_le_trans _ _ 0)// ?lte_ninfty//; exact: esum_ge0.
-  by apply: le_lt_trans Pf; apply le_esum.
+  apply: le_lt_trans Pf => /=.
+  by rewrite ge0_esum.
 apply: le_trans (nneseries_lim_ge n _) => //; apply: lee_sum => i _.
 by rewrite lee_abs.
 Qed.
@@ -567,7 +854,7 @@ transitivity (lim (EFin \o A_ @ \oo)).
 by rewrite EFin_lim//; apply: summable_cvg.
 Qed.
 
-Lemma summable_eseries (f : nat -> \bar R) (P : pred nat) : summable P f ->
+Lemma summable_eseries (f : (\bar R)^nat) (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.
@@ -603,7 +890,7 @@ have -> : (C_ = A_ \- B_)%R.
 by rewrite distrC; apply: hN; near: n; exists N.
 Unshelve. all: by end_near. Qed.
 
-Lemma summable_eseries_esum  (f : nat -> \bar R) (P : pred nat) :
+Lemma summable_eseries_esum (f : (\bar R)^nat) (P : pred nat) :
   summable P f -> \sum_(i <oo | P i) f i = esum P f^\+ - esum P f^\-.
 Proof.
 move=> Pfoo.
@@ -645,18 +932,17 @@ have /eqP : esum D (f \- g)^\+ + esum_posneg D g =
   by rewrite -addeA addeCA addeA subeK// fin_num_abs (summable_pinfty Df).
 rewrite [X in _ == X -> _]addeC -sube_eq.
 - rewrite fin_numD; apply/andP; split.
-    rewrite (@eq_esum _ _ _ _ (abse \o (f \- g)^\+))//.
+    rewrite (eq_esum _ _ (abse \o (f \- g)^\+))//.
       by move=> t Dt; rewrite /= gee0_abs.
     by rewrite -summableE; exact/summable_funepos/summableB.
-  move: Dg; rewrite summableE (@eq_esum _ _ _ _ g)//.
+  move: Dg; rewrite summableE (eq_esum _ _ g)//.
     by move=> t Tt; rewrite gee0_abs// g0.
   by rewrite ge0_esum_posneg// => t Tt; rewrite gee0_abs// g0.
 - rewrite fin_num_adde_defr// ge0_esum_posneg//.
-  rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
+  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.
-- rewrite ge0_esum_posneg//.
-  rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
+- 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.
@@ -665,3 +951,24 @@ by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
 Qed.
 
 End esumB.
+
+Section exchange_esum_ereal_sup.
+Context {R : realType} {T : choiceType} {f : T -> nat -> \bar R}.
+Hypothesis f_ge0 : forall t n, 0 <= f t n.
+Hypothesis f_nd : forall x, nondecreasing_seq (f x).
+
+Lemma exchange_esum_ereal_sup (A : set T) :
+  \esum_(i in A) ereal_sup (range (f i)) =
+  ereal_sup (range (fun n => \esum_(x in A) f x n)).
+Proof.
+rewrite ge0_esum.
+  by move=> x Ax; apply: le_ereal_sup_tmp; exists (f x 0).
+under eq_imagel.
+  move=> B [fin BA]; rewrite fsbig_finite//= ereal_sup_sum//.
+  over.
+rewrite exchange_ereal_sup; congr ereal_sup; apply: eq_imagel => n _.
+rewrite ge0_esum//; congr ereal_sup.
+by apply: eq_imagel => B [finB BA]; rewrite fsbig_finite.
+Qed.
+
+End exchange_esum_ereal_sup.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v
index 0c67532994..ca929f029f 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integrable.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v
@@ -984,7 +984,8 @@ rewrite -esumB//.
 rewrite -summable_eseries_esum.
   apply: (@le_lt_trans _ _ (\esum_(i in (fun=> true))
      `|(fine (\int[m_ i]_(x in D) f x))%:E|)).
-    by apply: le_esum => k _; rewrite -EFinB -fineB// -?integralE//;
+    do 2 rewrite ge0_esum//.
+    by apply: PosEsum.le_pos_esum => k _; rewrite -EFinB -fineB// -?integralE//;
       [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num].
   rewrite -nneseries_esum; first by [].
   apply: (@le_lt_trans _ _
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v
index d4395d5ee9..917f991730 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v
@@ -148,7 +148,8 @@ Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f.
 Proof.
 have [->|r0] := eqVneq r 0%R.
   by rewrite mul0e (eq_sintegral (cst 0%R)) ?sintegral0// => x/=; rewrite mul0r.
-rewrite !sintegralET ge0_mule_fsumr; first exact: nnsfun_mulemu_ge0.
+rewrite !sintegralET ge0_mule_fsumr.
+  by move=> s ?; rewrite nnsfun_mulemu_ge0.
 rewrite (reindex_fsbigT ( *%R r))/=.
   by exists ( *%R r^-1); [exact: mulKf|exact: mulVKf].
 by apply: eq_fsbigr => x; rewrite preimage_cstM// [(_ / r)%R]mulrC mulKf// muleA.
diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v
index df4cefd622..644b3fe713 100644
--- a/theories/lebesgue_integral_theory/radon_nikodym.v
+++ b/theories/lebesgue_integral_theory/radon_nikodym.v
@@ -893,7 +893,7 @@ rewrite ge0_integral_fsum//; first by move=> m y Ey; exact: nnfun_muleindic_ge0.
 transitivity (\int[mu]_(x in E) (\sum_(y \in range (h n))
     (y * \1_(h n @^-1` [set y]) x)%:E * g x)).
   under [RHS]eq_integral => x xE.
-    rewrite -ge0_mule_fsuml => [y|]; first exact: nnfun_muleindic_ge0.
+    rewrite -ge0_mule_fsuml => [y ?|]; first exact: nnfun_muleindic_ge0.
     rewrite fsumEFin // -(fimfunE _ x); over.
   by [].
 rewrite ge0_integral_fsum//.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 327961a2ff..2371ea646d 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -306,8 +306,9 @@ move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans.
   rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD.
   by case: ltP => //; rewrite lee_fin subr_le0.
 rewrite nneseries_esum//; first by move=> *; rewrite adde_ge0//= ?lee_fin.
-rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=.
-rewrite fsbig_finite//= set_fsetK//.
+rewrite esum_ge//=; first by move=> n _; rewrite adde_ge0.
+exists [set` X] => //.
+rewrite fsbig_finite// ?set_fsetK//= fsbig_finite//= set_fsetK//.
 rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=.
 do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW.
   by rewrite addrAC.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index cd14543440..a99ea011a4 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -473,7 +473,8 @@ apply: (@le_trans _ _ (\sum_(i <- X) (wlength f `](b i).1, (b i).2]%classic) +
   rewrite addeC -big_split/=; apply: lee_sum => k _.
   by rewrite !(EFinB, wlength_itv_bnd)// addeA subeK.
 rewrite -big_split/= nneseries_esum//; first by move=> k _; rewrite adde_ge0.
-rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite//= set_fsetK.
+rewrite esum_ge//=; first by move=> n _; rewrite adde_ge0.
+exists [set` X] => //; rewrite fsbig_finite//= set_fsetK.
 rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX.
 by rewrite AE leeD2l// lee_fin lerBlDl natrX De.
 Qed.
diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v
index d2e8cea15a..1db2fac757 100644
--- a/theories/measure_theory/dirac_measure.v
+++ b/theories/measure_theory/dirac_measure.v
@@ -102,7 +102,7 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A ->
 Proof.
 move=> infA; apply/eqyP => r r0.
 have [B BA Br] := infinite_set_fset (Num.truncn r).+1 infA.
-apply: esum_ge; exists [set` B] => //.
+rewrite ge0_esum//; apply: PosEsum.pos_esum_ge; exists [set` B] => //.
 apply: (@le_trans _ _ (Num.truncn r).+1%:R%:E).
   by rewrite lee_fin ltW// truncnS_gt.
 move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.
diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v
index 7f1bd77611..018f27c0e8 100644
--- a/theories/measure_theory/measure_extension.v
+++ b/theories/measure_theory/measure_extension.v
@@ -623,7 +623,7 @@ pose g i := (f^-1%FUN i).2; exists g; first split.
 rewrite !nneseries_esumT//= /measure.
 transitivity (\esum_(i in setT) \sum_(X0 \in decomp (F i)) mu X0); last first.
   by apply: eq_esum => /= k _; rewrite fsbig_finite//; exact: decomp_finite_set.
-rewrite -(eq_esum (fun _ _ => esum_fset _ _))//.
+rewrite -(eq_esum _ _ _ (fun _ _ => esum_fset _ _))//.
   by move=> ? _; exact: decomp_finite_set.
 rewrite esum_esum//= (reindex_esum K setT f) => //=.
 by apply: eq_esum => i Ki; rewrite /g funK ?inE.
diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v
index d8a4ac0721..01b441b15e 100644
--- a/theories/measure_theory/measure_function.v
+++ b/theories/measure_theory/measure_function.v
@@ -1206,13 +1206,15 @@ rewrite esum_bigcup//.
    move=> /(decomp_neq0 DUBiN0) [y Yy].
    apply: (@trivIset_seqDU _ B) => //; exists y.
    by split => //; [exact: YBi|exact: YBj].
-rewrite nneseries_esumT// le_esum// => i _.
+rewrite nneseries_esumT//.
+apply: le_esum => /=; first by move=> i _; exact: esum_ge0.
+move=> // i _.
 rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j).
   by rewrite esum_fset//; exact: decomp_finite_set.
 rewrite -SetRing.Rmu_fin_bigcup//=.
-  exact: decomp_finite_set.
-  exact: decomp_triv.
-  by move=> ?; exact: decomp_measurable.
+- exact: decomp_finite_set.
+- exact: decomp_triv.
+- by move=> ?; exact: decomp_measurable.
 rewrite -[leRHS]SetRing.RmuE// le_measure//; last by rewrite cover_decomp.
 - rewrite inE; apply: fin_bigcup_measurable; first exact: decomp_finite_set.
   move=> j /mem_set jdec; apply: sub_gen_smallest.
diff --git a/theories/numfun.v b/theories/numfun.v
index 534f7ce698..7946c95f0c 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -16,10 +16,6 @@ From mathcomp Require Import topology normedtype sequences.
 (* zero) ring) and theorems such as Tietze's extension theorem.               *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*     nondecreasing_fun f == the function f is non-decreasing                *)
-(*     nonincreasing_fun f == the function f is non-increasing                *)
-(*        increasing_fun f == the function f is (strictly) increasing         *)
-(*        decreasing_fun f == the function f is (strictly) decreasing         *)
 (*     itv_partition a b s == s is a partition of the interval `[a, b]        *)
 (*      itv_partitionL s c == the left side of splitting a partition at c     *)
 (*      itv_partitionR s c == the right side of splitting a partition at c    *)
@@ -57,15 +53,6 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n <= m)%O})
-  (at level 10).
-Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O})
-  (at level 10).
-Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O})
-  (at level 10).
-Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O})
-  (at level 10).
-
 Lemma nondecreasing_funN {R : numDomainType} a b (f : R -> R) :
   {in `[a, b] &, nondecreasing_fun f} <->
   {in `[a, b] &, nonincreasing_fun (\- f)}.
@@ -806,6 +793,45 @@ move=> fg x Dx; rewrite /funrneg /Num.max; case: ifPn => gx; case: ifPn => fx//.
 - by rewrite lerN2; exact: fg.
 Qed.
 
+Lemma eq_funrpos f g : f =1 g -> f^\+ =1 g^\+.
+Proof. by move=> eq_fg x; rewrite /funrpos eq_fg. Qed.
+
+Lemma eq_funrneg f g : f =1 g -> f^\- =1 g^\-.
+Proof. by move=> eq_fg x; rewrite /funrneg eq_fg. Qed.
+
+Lemma funrpos_cst0 x : (fun _ : T => 0)^\+ x = 0 :> R.
+Proof. by rewrite /funrpos maxxx. Qed.
+
+Lemma funrneg_cst0 x : (fun _ : T => 0)^\- x = 0 :> R.
+Proof. by rewrite /funrneg oppr0 maxxx. Qed.
+
+Lemma funrposZ f c : 0 <= c -> (c \*o f)^\+ =1 c \*o f^\+.
+Proof. by move=> ge0_c x; rewrite /= ge0_funrposM. Qed.
+
+Lemma funrnegZ f c : 0 <= c -> (c \*o f)^\- =1 c \*o f^\-.
+Proof.
+move=> ge0_c x; rewrite /= -!funrposN; have /= <- := funrposZ (- f) ge0_c x.
+by apply/eq_funrpos=> y /=; rewrite mulrN.
+Qed.
+
+Lemma funrpos_natrM f (n : T -> nat) x :
+  (fun x => (n x)%:R * f x)^\+ x = (n x)%:R * f^\+ x.
+Proof.
+by rewrite /funrpos -[in RHS]normr_nat maxr_pMr// mulr0 ger0_norm.
+Qed.
+
+Lemma funrneg_natrM f (n : T -> nat) x :
+  (fun x => (n x)%:R * f x)^\- x = (n x)%:R * f^\- x.
+Proof.
+rewrite -[in RHS]funrposN -funrpos_natrM -funrposN.
+by apply/eq_funrpos=> y; rewrite mulrN.
+Qed.
+
+Lemma le_funrpos_norm f x : f^\+ x <= `|f x|.
+Proof.
+by rewrite -/((Num.Def.normr \o f) x) -funrposDneg lerDl funrneg_ge0.
+Qed.
+
 End funrposneg_lemmas.
 #[global]
 Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core.
@@ -958,6 +984,12 @@ move=> fg x Dx; rewrite !funenegE /maxe; case: ifPn => gx; case: ifPn => fx //.
 - by rewrite leeN2; exact: fg.
 Qed.
 
+Lemma funepos_cst0 t : (@cst T _ 0)^\+ t = 0 :> \bar R.
+Proof. by rewrite funeposE maxxx. Qed.
+
+Lemma funeneg_cst0 t : (@cst T _ 0)^\- t = 0 :> \bar R.
+Proof. by rewrite funenegE oppe0 maxxx. Qed.
+
 End funposneg_lemmas.
 #[deprecated(since="mathcomp-analysis 1.15.0", note="use `-funeDB` instead")]
 Notation funeD_posD := funeDB (only parsing).
diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v
index a13264227b..4d6ec3844f 100644
--- a/theories/probability_theory/bernoulli_distribution.v
+++ b/theories/probability_theory/bernoulli_distribution.v
@@ -136,7 +136,7 @@ apply/funext => U; rewrite /bernoulli_prob; case: ifPn => [p01|]; last first.
 rewrite measure_addE/= /mscale/=.
 have := @subsetT _ U; rewrite setT_bool => UT.
 have [->|->|->|->] /= := subset_set2 UT.
-- rewrite -esum_fset//=; first by move=> b; rewrite lee_fin bernoulli_pmf_ge0.
+- rewrite -esum_fset//=.
   by rewrite esum_set0 2!measure0 2!mule0 adde0.
 - rewrite -esum_fset//=; first by move=> b; rewrite lee_fin bernoulli_pmf_ge0.
   rewrite esum_set1/= ?lee_fin// 2!diracE mem_set//= memNset//= mule0 adde0.
diff --git a/theories/sequences.v b/theories/sequences.v
index 9207b9ecb9..12c37d35ea 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1488,6 +1488,60 @@ apply: nondecreasing_cvgn.
   by apply: ereal_sup_ubound; exists (m + N)%N.
 Unshelve. all: by end_near. Qed.
 
+Section ereal_supD.
+Context {R : realType}.
+Local Open Scope ereal_scope.
+
+Lemma ereal_supD (u v : nat -> \bar R) :
+  (forall n, 0 <= u n) -> (forall n, 0 <= v n) ->
+  nondecreasing u -> nondecreasing v ->
+  ereal_sup (range u) + ereal_sup (range v) =
+  ereal_sup (range (fun n => u n + v n)).
+Proof.
+move=> u0 v0 ndu ndv.
+have u_ge0 : 0 <= ereal_sup (range u).
+  by rewrite (le_trans (u0 0%N))// ereal_sup_ubound//; exists 0%N.
+have v_ge0 : 0 <= ereal_sup (range v).
+  by rewrite (le_trans (v0 0%N))// ereal_sup_ubound//; exists 0%N.
+have ndsum : nondecreasing (fun n => u n + v n).
+  by move=> n m nm; apply: leeD; [exact: ndu | exact: ndv].
+have cuv_add : (fun n => u n + v n) @ \oo -->
+    ereal_sup (range u) + ereal_sup (range v).
+  apply: cvgeD.
+  - by apply: ge0_adde_def; rewrite inE.
+  - exact: ereal_nondecreasing_cvgn.
+  - exact: ereal_nondecreasing_cvgn.
+have : (fun n => u n + v n) @ \oo --> ereal_sup (range (fun n => u n + v n)).
+  exact: ereal_nondecreasing_cvgn.
+exact: cvg_unique cuv_add.
+Qed.
+
+Section ereal_sup_sum.
+Context {T : choiceType} (f : T -> nat -> \bar R).
+Hypothesis f_ge0 : forall t n, 0 <= f t n.
+Hypothesis f_nd : forall x, nondecreasing_seq (f x).
+
+Lemma ereal_sup_sum (l : seq T) :
+  \sum_(x <- l) ereal_sup (range (f x)) =
+  ereal_sup (range (fun n => \sum_(x <- l) f x n)).
+Proof.
+elim: l => [|x xs ih].
+- rewrite big_nil.
+  under eq_fun do rewrite big_nil.
+  by rewrite ereal_sup_cst//; apply/set0P; exists 0%N.
+- rewrite big_cons ih.
+  under [in RHS]eq_fun do rewrite big_cons.
+  apply: ereal_supD.
+  + by move=> n; exact: f_ge0.
+  + by move=> n; apply: sume_ge0 => y _; exact: f_ge0.
+  + by move=> n m nm; exact: f_nd.
+  + by move=> n m nm; apply: lee_sum => y _; exact: f_nd.
+Qed.
+
+End ereal_sup_sum.
+
+End ereal_supD.
+
 Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
   nondecreasing_seq u_ -> cvgn u_.
 Proof. by move=> ?; apply/cvg_ex; eexists; exact: ereal_nondecreasing_cvgn. Qed.