diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c934f4375f..9808769294 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -92,6 +92,23 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+- in `realsum.v`:
+  + lemma `esum_psum`
+  + lemma `sum_sum`
+
+- in `esum.v`:
+  + lemmas `esum_eq0P`, `esumZ`, `esum_esum'`
+  + definition `esg`
+  + lemmas `numEsg`, `gte0_esg`, `lte0_esg`, `esg0`
+  + lemmas `ge0_funeneg`, `ge0_funepos`, `funepos_cst0`, `funeneg_cst0`,
+    `le_funepos`
+  + definition `sum`
+  + lemmas `sum0`, `eq_sum`, `esum_unit`, `sum_unit`
+  + lemmas `esum_sum'`, `sum_ge0`, `le_sum`, `sumN`, `sumZ`
+  + lemmas `summable_le_sum`, `summable_esum_funepos`, `summable_sumN`,
+    `summableZ`, `summable_sumZ`
+  + lemmas `ereal_sup_comm`
+  + lemmas `esupZl`, `esupZl_range`, `esup_add`, `ereal_sup_sum`, `esum_esup_comm`
 
 ### Changed
 
@@ -182,6 +199,18 @@
   + 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`:
+  + now use `funrpos` and `funrneg`:
+    * lemmas `eq_fpos`, `eq_fneg`
+    * lemma `fpos0` (renamed to `funrpos_cst0`)
+    * lemma `fneg0` (renamed to `funrneg_cst0`)
+    * lemmas `fposZ`, `fnegZ`
+    * lemmas `fpos_natrM`, `fneg_natrM`
+    * lemmas `fneg_ge0`, `fpos_ge0`
+    * lemmas `le_fpos_norm`, `le_fpos`
+    * definition `sum`
+    * lemmas `summable_fpos`, `summable_fneg`
+  + lemma `sum0` (now uses `cst`)
 
 ### Renamed
 
@@ -263,6 +292,12 @@
 - 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`
+
 ### Infrastructure
 
 ### Misc
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..c04c913ef0 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.classical Require Import classical_sets functions cardinality.
+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.
+Lemma fnegZ f c : 0 <= c -> (c \*o f)^\- =1 c \*o 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).
+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 ge0_fpos f x : 0 <= fpos f x.
-Proof. by apply/normr_ge0. 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_fneg f x : 0 <= fneg 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 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,14 +102,14 @@ 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.
 
 (* -------------------------------------------------------------------- *)
 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 >]]}.
@@ -194,6 +166,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.
 
 (* -------------------------------------------------------------------- *)
@@ -343,6 +316,33 @@ 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, 0 <= S i) -> summable S ->
+  \esum_(x in [set: T]) (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 _]].
+  rewrite fsumEFin // => <-.
+  rewrite lee_fin fsbig_finite//=.
+  move/cardinality.finite_fsetP : finX => [J ->].
+  rewrite set_fsetK (le_trans _ (gerfin_psum J h))//.
+  rewrite -(@big_fset_seq R _ _ T J S)//= (le_trans _ (ler_norm_sum _ _ _))//.
+  exact: ler_norm.
+- rewrite (@eq_esum _ _ _ _ (fun x => `| S 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 => `|S x|))//=.
+  by rewrite -{1}(set_fsetK Fs) -fsbig_finite.
+Qed.
+
+End Esum.
+
 (* -------------------------------------------------------------------- *)
 Lemma max_sup {R : realType} x (E : set R) :
   (E `&` ubound E)%classic x -> sup E = x.
@@ -634,16 +634,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 +695,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 _ _ _ ((fun x => (S x)%:E)^\+%E) (fun x => (S^\+ x)%:E)).
+  by move=> t _; rewrite funeposE -fine_max.
+rewrite (@eq_esum _ _ _ ((fun x => (S x)%:E)^\-%E) (fun x => (S^\- x)%:E)).
+  by move=> t _; rewrite funenegE 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 +1161,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 +1181,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 +1205,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..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/esum.v b/theories/esum.v
index 486d54a46f..5e1382d117 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.
@@ -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,361 @@ by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
 Qed.
 
 End esumB.
+
+(* TODO: This should go to ereal.v or constructive_ereal.v *)
+Section Ereal.
+Context {R : realType}.
+Implicit Types x : \bar R.
+
+Definition esg x : \bar R :=
+  if x == 0 then 0 else if x < 0 then -1 else 1.
+
+Lemma numEsg 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 Ereal.
+
+Section Sum.
+Context {R : realType} {T : choiceType}.
+Implicit Types (f : T -> \bar R) (x y : \bar R).
+
+Lemma ge0_funeneg f t : (forall t, 0 <= f t) -> f^\- t = 0.
+Proof. by move => ?; rewrite funenegE max_r// ?lerN0 oppe_le0. Qed.
+
+Lemma ge0_funepos f t : (forall t, 0 <= f t) -> f^\+ t = f t.
+Proof. by move=> ?; rewrite funeposE max_l. 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.
+
+Lemma le_funepos f1 f2 : (forall t, f1 t <= f2 t) ->
+  (forall t, f1^\+ t <= f2^\+ t).
+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 => if x == y then S^\+ y else 0)).
+  move=> i ?.
+  by rewrite !funeposE; case: ifPn => //; rewrite maxxx.
+rewrite [X in _ - X](@eq_esum _ _ _ _ (fun y => if x == y then S^\- y else 0)).
+  move => i ?.
+  by rewrite !funenegE; case: ifPn => //; rewrite oppe0 maxxx.
+rewrite !esum_unit.
+case: (comparable_ltP (comparableT (S x) 0)%E) => Sx0.
+- rewrite esum1.
+    by move => t //= ->; rewrite funeposE max_r// ltW.
+  rewrite esum_set1 ?funeneg_ge0//.
+  by rewrite funenegE max_l ?oppeK ?add0e// oppe_ge0 ltW.
+- rewrite esum_set1 ?funepos_ge0// esum1.
+    by move => t //= ->; rewrite funenegE max_r// oppe_le0.
+  by rewrite funeposE max_l// sube0.
+Qed.
+
+Section SumTheoryP.
+
+Lemma esum_sum' S : (forall x, 0 <= S x) -> 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_esum_funepos S :
+  summable [set: T] S -> \esum_(t in [set: T]) S^\+ t \is a fin_num.
+Proof.
+move => /summable_funepos.
+rewrite summableE.
+rewrite (@eq_esum _ _ _ (fun y : T => S^\+ y) (fun y : T => `|S^\+ y|)) //=.
+by move => ??; rewrite gee0_abs.
+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.
+exact: summable_esum_funepos.
+Qed.
+
+Lemma summableZ c S : `|c| \is a fin_num ->
+  summable [set: T] (fun x : T =>  S x) ->
+  summable [set: T] (fun x : T => `|c| * S x).
+Proof.
+rewrite /summable => cfin Soo.
+rewrite (@eq_esum _ _ _ _ (fun x => `|c| * `|S x|)).
+  by move=> t ?; rewrite abseM abse_id.
+by rewrite esumZ// lte_mul_pinfty.
+Qed.
+
+Lemma summable_sumZ S c :
+`|c| \is a fin_num -> summable [set : T] S -> sum (fun x => c * S x) = c * sum S.
+Proof.
+move => hf 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 -summable_sumN; last by rewrite lte0_abs.
+    exact: summableZ.
+  + 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.
+  rewrite (@eq_esum _ _ _ _ (fun x => `|c| * S^\+ x)).
+    by move=> i _ //=; rewrite -(@fineK _ `|c|) // ge0_funeposM.
+  rewrite (@eq_esum _ _ _ (fun x => `|c| * S x)^\- (fun x => `|c| * S^\- x)).
+    by move=> t _ //=; rewrite -(@fineK _ `|c|) // ge0_funenegM.
+  rewrite !esumZ// -muleBr//=.
+    rewrite adde_defC fin_num_adde_defl//.
+    exact: summable_esum_funepos.
+  by rewrite muleA -numEsg.
+Qed.
+
+End SumTheoryS.
+
+End SumTheory.
+
+(* TODO: move *)
+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/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.