diff --git a/_CoqProject b/_CoqProject
index 431cbb08bc..ce426735af 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ experimental_reals/discrete.v
 experimental_reals/realseq.v
 experimental_reals/realsum.v
 experimental_reals/distr.v
+experimental_reals/edistr.v
 reals_stdlib/Rstruct.v
 reals_stdlib/nsatz_realtype.v
 
diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v
index 26f82b3ef8..2bbac0aae7 100644
--- a/experimental_reals/distr.v
+++ b/experimental_reals/distr.v
@@ -8,6 +8,7 @@ From mathcomp Require Import all_ssreflect_compat all_algebra.
 From mathcomp.classical Require Import boolp classical_sets mathcomp_extra.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete.
 From mathcomp Require Import realseq realsum.
+From mathcomp Require Import fsbigop.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -1266,3 +1267,231 @@ End Jensen.
 Notation convex f := (convexon \-inf \+inf f).
 
 (* -------------------------------------------------------------------- *)
+
+Section mono.
+  Context
+    {R : realType}
+    {T : choiceType}
+    {f : nat -> distr R T}
+    (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f n x <= f m x)).
+
+  Lemma cvg_f: forall x, exists l, ncvg (fun n => f n x) l%:E.
+  Proof.
+    move=> x; apply: ncvg_mono_bnd; first by move=> *; apply: hmono.
+    apply/asboolP/nboundedP => /=; exists 2%:R => //.
+    move=> n; rewrite ger0_norm ?ge0_mu //; apply: (@le_lt_trans _ _ 1%:R).
+    - by apply: le1_mu1.
+    by apply: ltr_nat.
+  Qed.
+
+  Lemma cvg_l : exists l, forall x, ncvg (fun n => f n x) (l x)%:E.
+  Proof.
+     have wtn: forall x, exists l, `[< ncvg (fun n => f n x) l%:E >].
+     - by move=> x; apply/exists_asboolP/asboolP/cvg_f.
+     exists (fun x => xchoose (wtn x)) => x.
+     by apply/asboolP/(xchooseP (wtn x)).
+  Qed.
+End mono.
+
+Section mono_sum.
+  Context
+    {R : realType}
+    {T : choiceType}
+    {f : nat -> distr R T}
+    (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f n x <= f m x)).
+
+  Lemma mono_psum_Efn (E: T -> R):
+    (forall m, 0 <= E m)%R ->
+    (forall n, summable (fun x => E x * f n x)) ->
+    forall m n, (m <= n)%N ->
+                psum (fun x => E x * f m x) <= psum (fun x => E x * f n x).
+  Proof.
+    move=> hE smb_Efn m n le_mn.
+    apply /le_psum /smb_Efn.
+    move => x; rewrite mulr_ge0 //=.
+    by apply: ler_pM  => //; apply: hmono.
+  Qed.
+
+  Lemma ncvg_lp (E: T -> R) r:
+    (forall m, 0 <= E m)%R ->
+    (forall n, summable (fun x => E x * f n x)) ->
+    (forall n : nat, psum (fun x => E x * f n x) <= r) ->
+    exists lp, ncvg (fun n => psum (fun x => E x * f n x)) lp%:E.
+  Proof.
+    move => He smb_Efn h.
+    have hr : (0 <= r)%R.
+    - apply: (le_trans (y:= psum (fun x => E x * f 0 x))).
+       - by apply: ge0_psum.
+       by apply: h.
+    apply: ncvg_mono_bnd ; first by apply: mono_psum_Efn.
+    apply/asboolP/nboundedP => /=.
+    exists (r + 1).
+      - by apply ltr_wpDl.
+      move => n; rewrite ger0_norm 1?ge0_psum //; apply/(le_lt_trans (y := r)).
+       - apply h.
+       by apply ltr_pwDr.
+  Qed.
+
+  Lemma sum_dlim_r [E : T -> R]  [r : R]:
+    summable E ->
+    (forall m, 0 <= E m)%R ->
+    (forall (n : nat), psum (fun x : T => E x * f n x) <= r)%R ->
+    (psum (fun x : T => E x * (\dlim_(n) f n) x) <= r)%R.
+  Proof.
+    move => smb_E hE h.
+    have [l cvgfx]:= @cvg_l R T f hmono.
+    have ge0_l: forall x, 0 <= l x.
+     - by move=> x; apply: (ncvg_geC _ (cvgfx x)) => n; apply: ge0_mu.
+    have cvgEfx: forall x, ncvg (fun n => E x * f n x) (E x * l x)%:E.
+     - by move=> x; apply/ncvgZ.
+    rewrite (@eq_psum _ _ _ (fun x => fine (nlim (fun n => E x * f n x)))).
+     - move => x /=;  rewrite dlimE (nlimE (cvgfx x)) /=.
+       by have /(ncvgZ (c := E x)) /nlimE -> /= := cvgfx x.
+    rewrite (@eq_psum _ _ _ (fun x => E x * l x)).
+     - by move=> x /=; have /(ncvgZ (c := E x)) /nlimE -> := cvgfx x.
+    apply: psum_le => J uqJ.
+    have ncvgJ:  ncvg (fun n => \sum_(j <- J) E j * f n j) (\sum_(j <- J) E j * (l j))%:E.
+     - by apply: (ncvg_mono_sum cvgEfx).
+    have smb_Efn: forall n, summable (fun x => E x * f n x).
+      - move=> n; apply summableM.
+        exact: smb_E.
+        apply summable_mu.
+     have [lp ncvg_lp] := @ncvg_lp _ r hE smb_Efn h.
+     have le1_lp: lp <= r.
+       - apply: (@ncvg_leC _ r _ _ _ ncvg_lp).
+         exact : h.
+     apply: (le_trans (y :=fine (nlim (fun n : nat => \sum_(j <- J) E j * f n j)))).
+      - rewrite (nlimE ncvgJ)  /=; apply: ler_sum => x _.
+        rewrite ger0_norm; auto.
+        by apply mulr_ge0.
+      rewrite (nlimE ncvgJ) /=.
+      apply (le_trans (y:= lp)).
+       - apply: (ncvg_le _ ncvg_lp ncvgJ) => n.
+         apply/(le_trans _): (ger_big_psum uqJ (smb_Efn n)).
+         by apply/ler_sum => x _; apply/ler_norm.
+       exact: le1_lp.
+  Qed.
+
+  Lemma sum_dlim (E : pred T) :
+    psum (fun x : T => (E x)%:R * (\dlim_(n) f n) x) =
+      fine (nlim (fun n => psum (fun x : T => (E x)%:R * f n x))).
+  Proof.
+   have [l cvgfx]:= @cvg_l R T f hmono.
+   have cvgEfx: forall x, ncvg (fun n => (E x)%:R * f n x) ((E x)%:R * l x)%:E.
+   - by move=> x; apply/ncvgZ.
+   have ge0_l: forall x, 0 <= l x.
+   - by move=> x; apply: (ncvg_geC _ (cvgfx x)) => n; apply: ge0_mu.
+   transitivity (psum (fun x => fine (nlim (fun n => (E x)%:R * f n x)))).
+   - apply: eq_psum => x /=; rewrite dlimE (nlimE (cvgfx x)) /=.
+     by have /(ncvgZ (c := (E x)%:R)) /nlimE -> /= := cvgfx x.
+   transitivity (psum (fun x => (E x)%:R * l x)); first apply: eq_psum.
+   - by move=> x /=; have /(ncvgZ (c := (E x)%:R)) /nlimE -> := cvgfx x.
+   have smb_Efn: forall n, summable (fun x => (E x)%:R * f n x).
+   - by move=> n; apply: (summable_pr E (f n)).
+   have le1_psum_Efn: forall n, psum (fun x => (E x)%:R * f n x) <= 1.
+   - by move=> n; apply/le1_pr.
+   have hE: forall x : T, 0 <= (E x)%:R. by auto.
+   have [lp ncvg_lp] := @ncvg_lp _ _ (hE R) smb_Efn le1_psum_Efn.
+   have le1_lp: lp <= 1.
+   - by move/ncvg_leC: ncvg_lp; apply; apply/le1_psum_Efn.
+   have smb_Ef: summable (fun x => (E x)%:R * l x).
+   - exists 1 => J; rewrite -(finmap.big_seq_fsetE _ _ predT (fun x => `|(E x)%:R * l x|)) /=.
+     apply: (le_trans (y := \sum_(x <- finmap.enum_fset J) (l x))).
+     - apply: ler_sum => /= j _; rewrite ger0_norm 1?mulr_ge0 //.
+       by apply: ler_piMl => //; case: (E _).
+     have: ncvg (fun n => \sum_(x <- finmap.enum_fset J) (f n x)) (\sum_(x <- finmap.enum_fset J) l x)%:E.
+     - by apply: ncvg_mono_sum.
+     move/ncvg_leC => /(_ 1); apply => n /=.
+     have /gerfin_psum := summable_mu (f n) => /(_ J).
+     move/le_trans => /= /(_ _ (le1_mu (f n))); apply/le_trans.
+     by rewrite finmap.big_seq_fsetE; apply: ler_sum => j _ /=; apply/ler_norm.
+   apply/eqP; rewrite eq_le; apply/andP; split.
+     - apply: psum_le => J uqJ.
+       have ncvgJ:
+       ncvg (fun n => \sum_(j <- J) (E j)%:R * f n j) (\sum_(j <- J) (E j)%:R * (l j))%:E.
+     - by apply: (ncvg_mono_sum cvgEfx).
+     apply: (le_trans (y := fine (nlim (fun n => \sum_(j <- J) (E j)%:R * f n j)))); last first.
+     - rewrite (nlimE ncvgJ) (nlimE ncvg_lp) /=.
+       apply: (ncvg_le _ ncvg_lp ncvgJ) => n.
+       apply/(le_trans _): (ger_big_psum uqJ (smb_Efn n)).
+       by apply/ler_sum => x _; apply/ler_norm.
+     rewrite (nlimE ncvgJ) /=; apply: ler_sum => x _.
+     by rewrite ger0_norm // mulr_ge0.
+   - rewrite (nlimE ncvg_lp) /=; apply: (ncvg_leC _ ncvg_lp) => n.
+     apply: le_psum => // x; rewrite mulr_ge0 //=.
+     apply: ler_pM => //; apply: (ncvg_homo_le _ (cvgfx x)).
+     by move=> *; apply: hmono.
+  Qed.
+
+End mono_sum.
+
+From mathcomp Require Import ereal esum.
+
+Section mono_esum.
+  Context
+    {R : realType}
+    {T : choiceType}
+    {f : nat -> distr R T}
+    (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f n x <= f m x)).
+
+  Lemma mono_esum_Efn (E: T -> \bar R):
+    (forall m, 0 <= E m)%E ->
+    forall m n, (m <= n)%N ->
+           (esum [set:T] (fun x => E x * (f m x)%:E) <=
+              esum [set:T] (fun x => E x * (f n x)%:E))%E.
+  Proof.
+    move=> hE m n le_mn.
+    apply /esum.le_esum.
+    move => ??; rewrite lee_pmul => //=.
+    - rewrite lee_tofin //.
+    - rewrite lee_tofin //; exact: hmono.
+  Qed.
+
+  Lemma ncvg_dlim a : ncvg (fun n : nat => f n a) ((\dlim_(n) f n) a)%:E.
+  Proof.
+    case : (dlimP (fun n => f n) a) => [l _ _ h | habs] //.
+    exfalso; apply habs.
+    apply dcvg_homo => n m hnm b.
+    by rewrite hmono.
+  Qed.
+
+  Lemma ereal_sup_sup a :
+    ereal_sup (range (fun n => (f n a)%:E)) = (sup ([set r | exists n, r = (f n a) ]))%:E.
+  Proof.
+    rewrite -ereal_sup_EFin.
+      - exists 1%R => r //= [n ->]; exact: le1_mu1.
+      - exists (f 0%N a);  exists 0%N  => //.
+      - congr ereal_sup.
+        apply /seteqP; split.
+        - by move => p [n _ hn]; exists (f n a) => //; exists n.
+        - by move => x [_ [n ->] <- ] //=; exists n.
+  Qed.
+
+  Lemma distr_lub_sup a :
+    ((dlim f) a)%:E = ereal_sup (range (fun n => (f n a)%:E)).
+  Proof.
+    unfold image.
+    rewrite ereal_sup_sup.
+    apply /ereal_eqP /eqP /esym; apply :nlim_sup.
+    - by move => n m h; rewrite hmono.
+    - exact: ncvg_dlim.
+  Qed.
+
+  Lemma esum_dlim_r [E : T -> \bar R]  [r : \bar R]:
+    (forall m, 0 <= E m)%E ->
+    (forall (n : nat), esum [set:T] (fun x : T => E x * (f n x)%:E) <= r)%E ->
+    (esum [set:T] (fun x : T => E x * ((\dlim_(n) f n) x)%:E) <= r)%E.
+  Proof.
+    move => hE h.
+    rewrite (@esum.eq_esum _ _ _ _ (fun x => ereal_sup (range (fun n =>  E x * (f n x)%:E)%E))).
+    - move => ??; rewrite distr_lub_sup.
+      rewrite (@esupZl_range R T (fun a b => (f b a)%:E)) //.
+      move => ??; rewrite lee_tofin //.
+    rewrite esum_esup_comm //.
+    - by move => ??; rewrite mule_ge0 // lee_tofin.
+    - by move => ????; rewrite lee_pmul // ?lee_tofin // hmono.
+    rewrite ge_ereal_sup//= => x [n s] <-.
+    apply h.
+  Qed.
+
+End mono_esum.
diff --git a/experimental_reals/edistr.v b/experimental_reals/edistr.v
new file mode 100644
index 0000000000..a06c99220f
--- /dev/null
+++ b/experimental_reals/edistr.v
@@ -0,0 +1,110 @@
+From mathcomp Require Import all_boot all_order all_algebra.
+From mathcomp.classical Require Import boolp fsbigop.
+From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
+From mathcomp.classical Require Import classical_sets functions.
+From mathcomp.experimental_reals Require Import realsum distr.
+From mathcomp.analysis Require Import esum ereal.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Unset SsrOldRewriteGoalsOrder.
+
+Import Order.TTheory GRing.Theory Num.Theory.
+
+Local Open Scope fset_scope.
+Local Open Scope ring_scope.
+
+(* -------------------------------------------------------------------- *)
+Reserved Notation "\Ee_[ mu ] f" (at level 2, format "\Ee_[ mu ]  f").
+
+Section Esp.
+  Context {R : realType} {T : choiceType}.
+
+  Implicit Types (mu : {distr T / R}) (f : T -> \bar R).
+
+  Definition espe  mu f := sum (fun x => mule (f x) ((mu x)%:E)).
+
+  Notation "\Ee_[ mu ] f" := (espe mu f).
+End Esp.
+
+Section PrCoreTheory.
+  Context {R : realType} {T : choiceType}.
+
+  Implicit Types (mu : {distr T / R}) (A B E : pred T).
+
+  Lemma exp_dunit (f : T -> \bar R) (x : T) :
+    espe (dunit x) f = f x.
+  Proof.
+    rewrite /espe.
+    rewrite (@eq_sum _ _ _ (fun y : T => if x == y then f y else 0%R)%E).
+    + move => x0. rewrite dunit1E.
+      by case (x == x0) => //=; rewrite ?mule1 ?mule0.
+    by rewrite sum_unit.
+  Qed.
+
+  Lemma exp_cst mu r : (espe mu (fun _ => r) = (\P_[mu] predT)%:E * r)%E.
+  Proof.
+    rewrite pr_predT psum_sum /espe //.
+    rewrite sumZ.
+    - move => ?. rewrite lee_fin //.
+    by rewrite sum_sum // muleC.
+  Qed.
+
+  Lemma exp0 mu : espe mu (fun _ => 0) = 0.
+  Proof. by rewrite exp_cst mule0. Qed.
+
+  Lemma exp_dlet {U: choiceType} mu (nu : T -> {distr U / R}) F :
+    (forall x, 0%:E <= F x)%E ->
+    espe (dlet nu mu) F = espe mu (fun x => espe (nu x) F).
+  Proof.
+    move => HF.
+    have pos : (forall (i : T) (j : U), (0%R <= F j * ((mu i)%:E * (nu i j)%:E))%E).
+    - move => i j; rewrite mule_ge0 //.
+      by rewrite mule_ge0 // lee_tofin.
+    rewrite /espe.
+    rewrite (eq_sum
+               (S1:=fun x : U => (F x * ((\dlet_(i <- mu) nu i) x)%:E)%E)
+               (S2:=fun x : U => (F x * esum [set:T] (fun y : T => (mu y * nu y x)%:E)))%E).
+    - move => x; rewrite dletE.
+      congr ( _ * _)%E.
+      rewrite -esum_psum //.
+      - by move => i; rewrite mulr_ge0.
+      - apply/(le_summable (F2 := mu)) => //.
+        by move=> x0; rewrite mulr_ge0 //= ler_piMr ?le1_mu1.
+    symmetry.
+    rewrite (eq_sum
+               (S1:=(fun x : T => (sum (fun x0 : U => F x0 * (nu x x0)%:E) * (mu x)%:E)%E))
+               (S2:=(fun x : T => (esum [set:U] (fun x0 : U => F x0 * ((mu x)%:E * (nu x x0)%:E))%E)))).
+    - move => x; rewrite muleC.
+      rewrite -sumZ.
+      - move => x1; rewrite mule_ge0 //=.
+      - exact:  (ge0_mu (nu x) x1).
+      rewrite (eq_sum
+               (S1:=(fun x0 : U => (mu x)%:E * (F x0 * (nu x x0)%:E))%E)
+               (S2:=(fun x0 : U => F x0 * ((mu x)%:E * (nu x x0)%:E))%E)) //.
+      - by move => ?; rewrite muleCA.
+    rewrite esum_sum' //.
+    rewrite esum_sum'.
+     - by move => ?; rewrite esum_ge0 //.
+   rewrite esum_esum' //.
+   rewrite esum_sum'.
+   - move => ?; rewrite mule_ge0 // esum_ge0 //.
+     by move => ??; rewrite  lee_tofin //  mulr_ge0.
+   rewrite {1}(eq_esum
+              (b:= fun x => (F x * (\esum_(y in [set: T]) (mu y * nu y x)%:E))%E)) //.
+   - move => ??. rewrite esumZ //.
+     by move => ?; rewrite  mule_ge0 // lee_tofin.
+  Qed.
+
+  Lemma expZ mu F c :
+    (forall x, 0%:E <= F x)%E ->
+    espe mu (fun x => mule c (F x)) = mule c (espe mu F).
+  Proof.
+    move => h.
+    rewrite -sumZ.
+    + by move => x; rewrite mule_ge0 // lee_tofin.
+    by apply/eq_sum=> x; rewrite muleA.
+  Qed.
+
+End PrCoreTheory.
diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v
index 267b1b7688..33de9a937a 100644
--- a/experimental_reals/realsum.v
+++ b/experimental_reals/realsum.v
@@ -3,12 +3,13 @@
 (* 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.classical Require Import boolp fsbigop.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
+From mathcomp.analysis Require Import esum ereal numfun.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -46,83 +47,54 @@ 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 -> f^\+ =1 g^\+.
+Proof. by move=> eq_fg x; rewrite /funrpos eq_fg. Qed.
 
-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 -> f^\- =1 g^\-.
+Proof. by move=> eq_fg x; rewrite /funrneg 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 funrpos_cst0 x : (fun _ : T => 0)^\+ x = 0 :> R.
+Proof. by rewrite /funrpos maxxx. Qed.
 
-Lemma fpos0 x : fpos (fun _ : T => 0) x = 0 :> R.
-Proof. by rewrite /fpos maxxx normr0. Qed.
+Lemma funrneg_cst0 x : (fun _ : T => 0)^\- x = 0 :> R.
+Proof. by rewrite /funrneg oppr0 maxxx. Qed.
 
-Lemma fneg0 x : fneg (fun _ : T => 0) x = 0 :> R.
-Proof. by rewrite /fneg minxx normr0. Qed.
+Lemma fposZ f c : 0 <= c -> (c \*o f)^\+ =1 c \*o f^\+.
+Proof. by move=> ge0_c x; rewrite /= ge0_funrposM. 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.
+Lemma fnegZ f c : 0 <= c -> (c \*o f)^\- =1 c \*o f^\-.
 Proof.
-move=> ge0_c x; rewrite /= -!fposN; have /=<- := (fposZ (- f) ge0_c x).
+move=> ge0_c x; rewrite /= -!funrposN; 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.
+  (fun x => (n x)%:R * f x)^\+ x = (n x)%:R * f^\+ x.
 Proof.
-rewrite /fpos -[in RHS]normr_nat -normrM.
-by rewrite maxr_pMr ?ler0n // mulr0.
+by rewrite /funrpos -[in RHS]normr_nat maxr_pMr// mulr0 ger0_norm.
 Qed.
 
 Lemma fneg_natrM f (n : T -> nat) x :
-  fneg (fun x => (n x)%:R * f x) x = (n x)%:R * fneg f x.
+  (fun x => (n x)%:R * f x)^\- x = (n x)%:R * f^\- x.
 Proof.
-rewrite -[in RHS]fposN -fpos_natrM -fposN.
+rewrite -[in RHS]funrposN -fpos_natrM -funrposN.
 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 fneg_ge0 f x : (forall x, 0 <= f x) -> f^\- x = 0.
+Proof. by move=> ?; rewrite /funrneg max_r// oppr_le0. Qed.
 
-Lemma ge0_fpos f x : 0 <= fpos f x.
-Proof. by apply/normr_ge0. Qed.
+Lemma fpos_ge0 f x : (forall x, 0 <= f x ) -> f^\+ x = f x.
+Proof. by move=> ?; rewrite /funrpos max_l. 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|.
+Lemma le_fpos_norm f x : f^\+ x <= `|f x|.
 Proof.
-rewrite /fpos ger0_norm ?(le_max, lexx) //.
-by rewrite ge_max normr_ge0 ler_norm.
+by rewrite -/((Num.Def.normr \o f) x) -funrposDneg lerDl funrneg_ge0.
 Qed.
 
-Lemma le_fpos f1 f2 : f1 <=1 f2 -> fpos f1 <=1 fpos f2.
+Lemma le_fpos f1 f2 : f1 <=1 f2 -> f1^\+ <=1 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.
+by move=> le_f x; rewrite (@funrpos_le _ _ setT)// inE.
 Qed.
 
 Definition psum f : R :=
@@ -130,7 +102,7 @@ Definition psum f : R :=
   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).
+Definition sum f : R := psum f^\+ - psum f^\-.
 End Sum.
 
 (* -------------------------------------------------------------------- *)
@@ -194,6 +166,18 @@ case/(_ (NPInf M)): cu => K /= /(_ K (leqnn _)).
 rewrite inE/= => /ltW /le_trans /(_ (ler_norm _)).
 by move/le_lt_trans/(_ (bdu _)); rewrite ltxx.
 Qed.
+
+Lemma ncvg_mono_sum {T : eqType} [f : nat -> T -> R] [l : T -> R] [J : seq T] :
+  (forall x, ncvg (fun n => f n x) (l x)%:E) ->
+  ncvg (fun n => \sum_(x <- J) f n x) (\sum_(x <- J) l x)%:E.
+Proof.
+move=> hcvg; elim: J => //= [|j J ih].
+- rewrite big_nil; apply/(@ncvg_eq _ (fun _ => 0))/ncvgC.
+  by move=> n /=; rewrite big_nil.
+- rewrite big_cons; have := ncvgD (hcvg j) ih; apply/ncvg_eq.
+  by move=> n /=; rewrite big_cons.
+Qed.
+
 End PosCnv.
 
 (* -------------------------------------------------------------------- *)
@@ -343,6 +327,47 @@ by case=> /= [|J lt_lJ _]; [apply/summable_sup | exists J].
 Qed.
 End SumTh.
 
+(* -------------------------------------------------------------------- *)
+Section Esum.
+
+  Context {R : realType} {T : choiceType}.
+
+  Lemma esum_psum (S: T -> R) :
+    (forall i : T, 0%R <= S i) ->
+    summable S ->
+    esum [set:T] (fun x => (S x)%:E) = (psum S)%:E.
+  Proof.
+    move => Sg0 h; apply/eqP; rewrite eq_le; apply/andP; split.
+    - rewrite ge_ereal_sup//=  => x [] X []  finX XT.
+      rewrite fsumEFin // => <-.
+      rewrite lee_fin.
+      rewrite fsbig_finite //=.
+      revert finX.
+      rewrite cardinality.finite_fsetP.
+      move => []  J ->.
+      rewrite cardinality.set_fsetK.
+      apply: (le_trans _ (gerfin_psum J  h)).
+      rewrite -(@big_fset_seq R _ _ T J S)  //=.
+      apply: (le_trans _ (ler_norm_sum _ _ _)).
+      exact : ler_norm.
+    - rewrite (eq_esum (b:= fun x => `| S x |%:E)%E).
+    - by move => ??; rewrite  ger0_norm.
+      have [H1 H3] := (summable_sup h).
+      rewrite psum_absE //.
+      rewrite -(ereal_sup_EFin H3 H1).
+      rewrite ge_ereal_sup//= => x [] X []  Fs XT <-.
+      rewrite esum_ge //.
+      exists ([set` Fs]%classic) => //.
+      rewrite fsumEFin //.
+      rewrite lee_fin.
+      rewrite XT.
+      rewrite (@big_fset_seq R _ _ T _ (fun x => `|S x|))  //=.
+      rewrite -{1}(cardinality.set_fsetK Fs).
+      by rewrite -fsbig_finite.
+  Qed.
+
+End Esum.
+
 (* -------------------------------------------------------------------- *)
 Lemma max_sup {R : realType} x (E : set R) :
   (E `&` ubound E)%classic x -> sup E = x.
@@ -634,16 +659,17 @@ Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma summable_fpos (f : T -> R) :
-  summable f -> summable (fpos f).
+  summable f -> summable f^\+.
 Proof.
-move/summable_abs; apply/le_summable=> x.
-by rewrite ge0_fpos /= le_fpos_norm.
+by move/summable_abs; apply/le_summable => x; rewrite funrpos_ge0 le_fpos_norm.
 Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma summable_fneg (f : T -> R) :
-  summable f -> summable (fneg f).
-Proof. by move/summableN/summable_fpos/(eq_summable (fposN _)). Qed.
+  summable f -> summable f^\-.
+Proof.
+by move/summableN/summable_fpos; apply: eq_summable => x; rewrite funrposN.
+Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma summable_condl (S : T -> R) (P : pred T) :
@@ -694,6 +720,25 @@ Qed.
 
 End SummableAlg.
 
+(* -------------------------------------------------------------------- *)
+Section Sum_Sum.
+  Context {T: choiceType} {R : realType}.
+
+  Lemma sum_sum (S: T -> R) :
+    summable S ->
+    esum.sum (fun x => (S x)%:E) = (sum S)%:E.
+  Proof.
+    move => hs. rewrite /esum.sum /sum.
+    rewrite (eq_esum (a:= (fun x => (S x)%:E)^\+%E) (b:= fun x => (S^\+ x)%:E)).
+    - by move => ??; rewrite funeposE -fine_max//=.
+      rewrite (eq_esum (a:= (fun x => (S x)%:E)^\-%E) (b:= fun x => (S^\- x)%:E)).
+    - by move => ??; rewrite funenegE /funrneg EFin_max.
+    rewrite esum_psum //; first exact : summable_fpos.
+    by rewrite esum_psum //; exact : summable_fneg.
+  Qed.
+
+End Sum_Sum.
+
 (* -------------------------------------------------------------------- *)
 Section StdSum.
 Context {R : realType} (T : choiceType) (I : Type).
@@ -1141,17 +1186,19 @@ Lemma le_sum S1 S2 :
 Proof.
 move=> smS1 smS2 leS; rewrite /sum lerB //.
   apply/le_psum/summable_fpos => // x.
-  by rewrite ge0_fpos /= le_fpos.
+  by rewrite funrpos_ge0/= le_fpos.
 apply/le_psum/summable_fneg => // x.
-rewrite -!fposN ge0_fpos le_fpos // => y.
+rewrite -!funrposN funrpos_ge0 le_fpos // => 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.
+by rewrite /sum !(eq_psum funrpos_cst0, eq_psum funrneg_cst0) !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,7 +1206,7 @@ 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 _ _)) //.
@@ -1183,13 +1230,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/rocq-mathcomp-experimental-reals.opam b/rocq-mathcomp-experimental-reals.opam
index 83179674dd..234d011a17 100644
--- a/rocq-mathcomp-experimental-reals.opam
+++ b/rocq-mathcomp-experimental-reals.opam
@@ -19,6 +19,7 @@ build: [make "-C" "experimental_reals" "-j%{jobs}%"]
 install: [make "-C" "experimental_reals" "install"]
 depends: [
   "rocq-mathcomp-reals" { = version}
+  "rocq-mathcomp-analysis" { = "dev"}
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
 ]
 
diff --git a/theories/esum.v b/theories/esum.v
index 486d54a46f..02450134e8 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -1,5 +1,7 @@
 (* mathcomp analysis (c) 2017 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.
@@ -100,6 +102,16 @@ Proof.
 by move=> ?; rewrite esum_fset// ?fset_set1// ?fsbig_set1// => t' /[!inE] ->.
 Qed.
 
+Lemma esum_eq0P (A : set T) a : (forall i, A i -> 0 <= a i) ->
+  \esum_(x in A) a x = 0 ->
+  forall x, A x -> a x = 0.
+Proof.
+move=> a0 suma0 x Ax.
+apply/eqP; rewrite eq_le a0//= -suma0 ereal_sup_ubound//=.
+exists [set x]; first by split => // t ->.
+by rewrite -esum_set1 ?a0// esum_fset// => i /[!inE] ->; exact: a0.
+Qed.
+
 End esum_realType.
 
 Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) :
@@ -129,6 +141,28 @@ Lemma eq_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
   \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.
 
+(* TODO: generalize setT to any set *)
+Lemma esumZ [R : realType] [T : choiceType] (a : T -> \bar R)
+    (c : \bar R) : 0 <= c -> (forall t, 0 <= a t) ->
+  \esum_(t in [set: T]) c * a t = c * \esum_(t in [set: T]) a t.
+Proof.
+rewrite le_eqVlt => /predU1P[<- _|c0 a0].
+  by rewrite esum1 ?mul0e// => ? _; rewrite mul0e.
+apply/eqP; rewrite eq_le; apply/andP; split.
+- rewrite ge_ereal_sup//= => _ [X [finX _]] <-.
+  by rewrite -ge0_mule_fsumr// (lee_wpmul2l (ltW c0))// esum_ge//; exists X.
+- case: c c0 => [s s0|_|//].
+  + rewrite -lee_pdivlMl// ge_ereal_sup//= => _ [X [finX XI]] <-.
+    by rewrite lee_pdivlMl// ge0_mule_fsumr// esum_ge//; exists X.
+  + have : 0 <= \esum_(x in setT) a x by apply: esum_ge0 => ? _; exact: a0.
+    rewrite [in X in X -> _]le_eqVlt => /predU1P[<-|suma0].
+    + by rewrite mule0 esum_ge0// => ? _; rewrite mule_ge0.
+    + rewrite gt0_mulye//.
+      have [y [A fsetsTA yE y0]] := ereal_sup_gt suma0.
+      rewrite leye_eq; apply/eqP/eq_infty => r; rewrite esum_ge//.
+      by exists A => //; rewrite -ge0_mule_fsumr// yE gt0_mulye// leey.
+Qed.
+
 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.
@@ -356,6 +390,19 @@ by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE
 Qed.
 Arguments reindex_esum {R T T'} P Q e a.
 
+(* TODO: rename *)
+Lemma esum_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.
 
@@ -665,3 +712,334 @@ by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
 Qed.
 
 End esumB.
+
+
+(* This should go to ereal*)
+Section Ereal.
+  Context {R : realType}.
+
+  Definition esg (x: \bar R) : \bar R :=
+    (if x == 0 then 0 else if x < 0 then -1 else 1)%E.
+
+  Lemma numEsg (x : \bar R): (x = esg x * `|x|)%E.
+  Proof.
+    rewrite /esg.
+    case (comparable_ltgtP (comparableT x 0)%E) => h.
+    + by rewrite (lt_eqF h) h lte0_abs // muleNN mul1e.
+    + by rewrite (gt_eqF h) (lt_gtF h) gte0_abs // mul1e.
+    + by rewrite h eq_refl mul0e.
+  Qed.
+
+  Lemma gte0_esg (x : \bar R): (x < 0 -> esg x = -1)%E.
+  Proof.
+    by move => h; rewrite /esg (lt_eqF h) h.
+  Qed.
+
+  Lemma lte0_esg (x : \bar R): (0 < x -> esg x = 1)%E.
+  Proof.
+     by move => h; rewrite /esg (gt_eqF h) (lt_gtF h).
+  Qed.
+
+  Lemma esg0 : (esg 0 = 0)%E.
+  Proof.
+     by rewrite /esg eq_refl.
+  Qed.
+
+End Ereal.
+
+
+Section Sum.
+  Context {R : realType} {T : choiceType}.
+
+  Implicit Types f (* g *) : T -> \bar R.
+
+  Lemma min_l (x y : \bar R) : (x <= y -> mine x y = x)%E. Proof. by case: comparableP. Qed.
+
+  Lemma min_r (x y : \bar R) : (y <= x -> mine x y = y)%E. Proof. by case: comparableP. Qed.
+
+  Lemma max_l (x y : \bar R) : (y <= x -> maxe x y = x)%E. Proof. by case: comparableP. Qed.
+
+  Lemma max_r (x y : \bar R) : (x <= y -> maxe x y = y)%E. Proof. by case: comparableP. Qed.
+
+  Lemma ge0_funeneg f x : (forall x, 0 <= f x)%E -> f^\- x = 0.
+  Proof. by move => ?; rewrite funenegE max_r// ?lerN0 oppe_le0. Qed.
+
+  Lemma ge0_funepos f x : (forall x, 0 <= f x)%E -> f^\+ x = f x.
+  Proof. by move=> ?; rewrite funeposE max_l. Qed.
+
+  Lemma funepos_cst0 x : (@cst T _ 0)^\+ x = 0 :> \bar R.
+  Proof. by rewrite funeposE maxxx. Qed.
+
+  Lemma funeneg_cst0 x : (@cst T _ 0)^\- x = 0 :> \bar R.
+  Proof. by rewrite funenegE oppe0 maxxx. Qed.
+
+  Lemma le_funepos f1 f2 : ((forall x, f1 x <= f2 x) -> (forall x, f1^\+ x <= f2^\+ x))%E.
+  Proof. by move=> le_f x; rewrite (@funepos_le _ _ setT)// inE. Qed.
+
+  Definition sum f : \bar R := esum [set: T] f^\+ - esum [set: T] f^\-.
+End Sum.
+
+Section SumTheory.
+  Context {R : realType} {T : choiceType}.
+  Implicit Types (S : T -> \bar R).
+
+Lemma sum0 : @sum R _ (@cst T _ 0) = 0.
+Proof.
+by rewrite /sum !esum1 ?subee// => r _; rewrite ?[LHS](funepos_cst0,funeneg_cst0).
+Qed.
+
+  Lemma eq_sum S1 S2: S1 =1 S2 -> sum S1 = sum S2.
+  Proof.
+    move=> eq_fg; rewrite /sum; congr (_ - _).
+    by apply: eq_esum => t _; rewrite !funeposE eq_fg.
+    by apply: eq_esum => t _; rewrite !funenegE eq_fg.
+  Qed.
+
+(* TODO: rename *)
+Lemma esum_unit S x :
+  \esum_(y in [set: T]) (if x == y then S y else 0) = \esum_(i in [set x]) S i.
+Proof.
+rewrite [RHS]esum_mkcond.
+by under [in RHS]eq_esum do rewrite in_set1 eq_sym.
+Qed.
+
+  Lemma sum_unit S x : sum (fun y => if x == y then S y else 0) = S x.
+  Proof.
+    rewrite /sum.
+    rewrite (@eq_esum _ _ _ _ (fun y : T => if x == y then S^\+ y else 0%R)).
+    + move=> i ?.
+      by rewrite !funeposE; case: ifPn => //; rewrite maxxx.
+    rewrite [X in _ - X](@eq_esum _ _ _ _ (fun y : T => if x == y then S^\- y else 0%R)).
+    + move =>  i ?.
+      by rewrite !funenegE; case: ifPn => //; rewrite oppe0 maxxx.
+    rewrite !esum_unit.
+    case (comparable_ltP (comparableT (S x) 0)%E) => h;last first.
+    + rewrite esum_set1 ?funepos_ge0//.
+      rewrite esum1.
+      + by move => i //= ->; rewrite funenegE max_r// oppe_le0.
+      by rewrite funeposE max_l// sube0.
+    rewrite esum1.
+    + by move => i //= ->; rewrite funeposE max_r// ltW.
+    rewrite esum_set1.
+    + by rewrite funeneg_ge0.
+    by rewrite funenegE max_l ?oppeK ?add0e// oppe_ge0 ltW.
+  Qed.
+
+  Section SumTheoryP.
+
+  Lemma esum_sum' S : (forall x, 0 <= S x)%E -> sum S = \esum_(i in [set: T]) S i.
+  Proof.
+    move=> ge0_S; rewrite /sum (@esum1 R T [set: T] S^\-) ?sube0.
+      by move=> x ?; rewrite ge0_funeneg.
+    by under eq_esum do rewrite ge0_funepos//.
+  Qed.
+
+Lemma sum_ge0 S : (forall x, 0 <= S x) -> 0 <= sum S.
+Proof. by move=> ge0_S; rewrite esum_sum' // esum_ge0. Qed.
+
+Lemma le_sum S1 S2: (forall x, 0 <= S1 x) -> (forall x, S1 x <= S2 x) ->
+  sum S1 <= sum S2.
+Proof.
+move=> pS1 leS.
+have pS2 x : 0 <= S2 x by rewrite (le_trans _ (leS _)).
+rewrite /sum leeB//.
+- by apply: le_esum => t _; rewrite !ge0_funepos.
+- by apply: le_esum => t _; rewrite !ge0_funeneg.
+Qed.
+
+Lemma sumN S : (forall x, 0 <= S x) -> sum (\- S ) = - sum S.
+Proof.
+move=> S0; rewrite /sum [X in X - _ = _]esum1 ?add0r.
+  by move=> t _; rewrite funeposN ge0_funeneg.
+rewrite [X in _ = - (_ - X)]esum1 ?sube0.
+  by move=> t _; rewrite ge0_funeneg.
+by under eq_esum do rewrite funenegN.
+Qed.
+
+Lemma sumZ S c : (forall x, 0 <= S x) -> sum (fun x => c * S x) = c * sum S.
+Proof.
+move=> h.
+rewrite (@eq_sum _ (fun x => esg c * (`|c| * S x))).
+  by move=> x; rewrite muleA -numEsg.
+transitivity (esg c * sum (fun x => `|c| * S x)).
+- have [hc|hc|->] := comparable_ltgtP (comparableT c 0).
+  + rewrite {1}lte0_abs// gte0_esg// (@eq_sum _ (fun x => - (- c * S x))).
+      by move => ?; rewrite mulN1e.
+    rewrite mulN1e -sumN; last by rewrite lte0_abs.
+    by move=> ?; rewrite mule_ge0.
+  + rewrite gte0_abs// lte0_esg// mul1e (@eq_sum _ (fun x => c * S x))//.
+    by move=> ?; rewrite mul1e.
+  + under eq_sum do rewrite esg0 mul0e.
+    by rewrite esg0 mul0e sum0.
+- rewrite {1}/sum (@eq_esum _ _ _ _ (fun x => `|c| * S x))//.
+     by move=> ? _; rewrite ge0_funepos // => x; rewrite mule_ge0.
+  rewrite (@eq_esum _ _ _ (_^\-) (@cst T _ 0)).
+    by move => ? _; rewrite ge0_funeneg // => x; rewrite mule_ge0.
+  by rewrite (@esum1 _ _ _ (cst 0))// sube0 esumZ// muleA -numEsg esum_sum'.
+Qed.
+
+  End SumTheoryP.
+
+  Section SumTheoryS.
+
+Lemma summable_le_sum S1 S2 : summable [set : T] S2 ->
+  (forall x, S1 x <= S2 x) -> sum S1 <= sum S2.
+Proof.
+move=> smS2 leS; rewrite /sum leeB//.
+  by apply: le_esum => ? ?; exact: le_funepos.
+apply le_esum => t _.
+by rewrite -!funeposN; apply: le_funepos => ?; rewrite leeN2.
+Qed.
+
+Lemma summable_sumN S : summable [set : T] S -> sum (\- S ) = - sum S.
+Proof.
+  move => hs.
+  rewrite /sum funenegN funeposN addeC oppeB //= adde_defC.
+  apply : fin_num_adde_defl.
+  have := (summable_funepos hs).
+  rewrite summableE.
+  rewrite (@eq_esum _ _ _ (fun y : T => S^\+ y) (fun y : T => `|S^\+ y|)) //=.
+  by move => ??; rewrite gee0_abs.
+Qed.
+
+  End SumTheoryS.
+
+End SumTheory.
+
+Lemma ereal_sup_comm {R:realType} {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 key : forall (X' Y' : Type) (g : X' -> Y' -> \bar R) (C : set X') (D : set Y'),
+      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].
+  apply: le_anti. apply/andP; split; [exact: key | exact: (key _ _ (fun y x => f x y) B A)].
+  move=> X' Y' g C D.
+  apply/ereal_supP => _ [x hx <-].
+  apply/ereal_supP => _ [y hy <-].
+  apply: le_ereal_sup_tmp; exists (ereal_sup [set g x0 y | x0 in C]).
+  - exists y => //.
+  - apply: le_ereal_sup_tmp; exists (g x y); [exists x => // | exact: le_refl].
+Qed.
+
+
+Section mono_esum.
+  Context
+    {R : realType}
+    {T : choiceType}
+    {f : T -> nat -> \bar R}
+    {fpos : forall t n, 0 <= f t n}
+    (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f x n <= f x m)).
+
+Lemma esupZl (c : \bar R) (X : set \bar R):
+  0 <= c ->
+  X != set0 ->
+  (forall x, X x -> 0 <= x) ->
+  ereal_sup [ set c * x | x in X ] = c * ereal_sup X.
+Proof.
+move=> cpos Xne Xpos.
+  have /set0P [x Xx] := Xne.
+  case: c cpos => [r|_|//].
+  - move=> hr.
+    case: (eqVneq r 0%R) => [-> | rne0].
+    + rewrite mul0e.
+      under eq_imagel => a _ do rewrite mul0e.
+      rewrite ereal_sup_cst //.
+      exact: ereal_supZl Xne hr.
+  - case: (boolp.pselect (forall a, X a -> a = 0)) => [hall | hnall].
+    + have -> : [set +oo * x | x in X] = [set 0]. {
+         apply/seteqP; split.
+         + by move=> _ [z Xz <-]; rewrite (hall _ Xz) mule0 //.
+         + by move=> y /= ->; exists x => //; rewrite (hall _ Xx) mule0.
+       }
+       have -> : X = [set 0]. {
+         apply/seteqP; split.
+         + by move=> y Xy; rewrite (hall _ Xy)=> //.
+         + by move=> y /= ->; rewrite -(hall _ Xx) //.
+       }
+       by rewrite ereal_sup1 mule0.
+     + move: hnall; rewrite -boolp.existsNE.
+       move => [y /boolp.not_implyP [Xy hy] ].
+       have ygt0: 0 < y by rewrite lt_def Xpos // andbT; apply/eqP.
+       rewrite gt0_mulye //.
+       - apply: (lt_le_trans ygt0); exact: ereal_sup_ubound.
+       apply: ereal_supy. exists y => //. exact: gt0_mulye.
+Qed.
+
+  Lemma esupZl_range (c : \bar R) (x : T) (cpos : 0 <= c) :
+    (c * ereal_sup (range (f x)) =
+     ereal_sup (range (fun n => c * f x n)))%E.
+  Proof.
+    have seteq :
+      [set c * y | y in range (f x)] = range (fun n => c * f x n).
+      apply/seteqP; split.
+      - by move=> _ [_ [n _ <-] <-]; exists n.
+      - by move=> _ [n _ <-]; exists (f x n) => //; exists n.
+    rewrite -seteq esupZl //.
+    - by apply/set0P; exists (f x 0%N), 0%N.
+    - by move=> _ [n _ <-]; exact: fpos.
+  Qed.
+
+  Lemma esup_add (u v : nat -> \bar R) :
+    (forall n, 0 <= u n) -> (forall n, 0 <= v n) ->
+    nondecreasing_seq u -> nondecreasing_seq 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 su_ge0 : 0 <= ereal_sup (range u).
+      by rewrite (le_trans (u0 0%N))// ereal_sup_ubound//; exists 0%N.
+    have sv_ge0 : 0 <= ereal_sup (range v).
+      by rewrite (le_trans (v0 0%N))// ereal_sup_ubound//; exists 0%N.
+    have ndsum : nondecreasing_seq (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 cuv_sup :
+      (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 cuv_sup.
+  Qed.
+
+  Lemma ereal_sup_sum (A : {fset T}) :
+    \sum_(x <- A) ereal_sup (range (f x)) =
+      ereal_sup (range (fun n => \sum_(x <- A) f x n)).
+  Proof.
+    have key (l : seq T) :
+        \sum_(x <- l) ereal_sup (range (f x)) =
+          ereal_sup (range (fun n => \sum_(x <- l) f x n)).
+      elim: l => [|x xs IH].
+      - rewrite big_nil.
+        under eq_fun => n do rewrite big_nil.
+        by rewrite ereal_sup_cst//; apply/set0P; exists 0%N.
+      - rewrite big_cons IH.
+        under [in RHS]eq_fun => n do rewrite big_cons.
+        apply: esup_add.
+        + by move=> n; exact: fpos.
+        + by move=> n; apply: sume_ge0 => y _; exact: fpos.
+        + by move=> n m nm; exact: hmono.
+        + by move=> n m nm; apply: lee_sum => y _; exact: hmono.
+    exact: key.
+  Qed.
+
+Lemma esum_esup_comm :
+  \esum_(i in [set: T]) ereal_sup (range (f i)) =
+  ereal_sup (range (fun n => \esum_(x in [set:T]) f x n)).
+Proof.
+rewrite /esum.
+under eq_imagel => A [fin ?] do rewrite fsbig_finite// ereal_sup_sum//.
+rewrite ereal_sup_comm.
+congr ereal_sup.
+apply: eq_imagel => n _.
+congr ereal_sup.
+apply: eq_imagel  => A [finA _].
+by rewrite fsbig_finite.
+Qed.
+
+End mono_esum.