diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4ee12401e3..840c0e85b2 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -20,6 +20,15 @@
 - in `num_topology.v`:
   + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`,
     `at_left_shift`, `at_right_shift`
+- in `esum.v`:
+  + lemmas `pos_esum_ge1`, `le_pos_esum_fine`, `sum_esum_ge`, `le_esum_fine`,
+    `subset_esum`, `esum0`, `esum_if_eq_op_set1`, `esum_neq0`, `esum_ge1`
+  + lemmas `eq_esummable`, `le_esummable`, `esummableZl`, `esummableZr`,
+    `esummableMl`, `esummableMr`, `esummableM`
+  + lemmas `esummable_esum_funepos`, `esummable_esum_funeneg`,
+     `esummable_esum_fin_num`, `esummable_esumN`
+  + lemma `esumE`
+  + lemmas `esummable_esumZ`, `esummable_esumD`, `esummableB`
 
 ### Changed
 
@@ -31,8 +40,32 @@
 
 ### Renamed
 
+- in `esum.v`:
+  + `summable` -> `esummable`
+  + `summable_pinfty` -> `esummable_pinfty`
+  + `summableE` -> `esummableE`
+  + `summableD` -> `esummableD`
+  + `summableN` -> `esummableN`
+  + `summableB` -> `esummableB`
+  + `summable_funepos` -> `esummable_funepos`
+  + `summable_funeneg` -> `esummable_funeneg`
+  + `summable_fine_sum` -> `esummable_fine_sum`
+  + `summable_cvg` -> `esummable_cvg`
+  + `summable_nneseries_lim` -> `esummable_nneseries_lim`
+  + `summable_eseries` -> `esummable_eseries`
+  + `summable_eseries_esum` -> `esummable_eseries_esum`
+
+- in `lebesgue_integrable.v`:
+  + `integrable_summable` -> `integrable_esummable`
+
+- in `lebesgue_integral_nonneg.v`:
+  + `summable_integral_dirac` -> `esummable_integral_dirac`
+
 ### Generalized
 
+- in `esum.v`:
+  + lemmma `le_esum`
+
 ### Deprecated
 
 ### Removed
diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v
index 7283768349..9a77ce3ac5 100644
--- a/experimental_reals/distr.v
+++ b/experimental_reals/distr.v
@@ -362,7 +362,7 @@ Lemma isd_mlet : isdistr mlet.
 Proof.
 split=> [x|J uqJ]; first by apply/ge0_psum.
 rewrite /mlet psum_bigop; first by move=> y x; rewrite mulr_ge0.
-  move=> u; apply/(le_summable (F2 := mu)) => //.
+  move=> u; apply/(le_summable (g := mu)) => //.
   by move=> x; rewrite mulr_ge0 //= ler_piMr ?le1_mu1.
 apply/(le_trans _ (le1_mu mu))/le_psum => //.
 move=> x; rewrite sumr_ge0 /= => [y _|]; first by rewrite mulr_ge0.
@@ -495,10 +495,11 @@ Lemma eq0_dlet (mu : {distr T / R}) (F : T -> {distr U / R}) y :
 Proof.
 unlock dlet; rewrite /= /mlet => /eq0_psum h x /dinsuppP /eqP mu_x.
 have {}/h: summable (fun x => mu x * F x y).
-  apply/(le_summable (F2 := mu)) => // z.
+  apply/(le_summable (g := mu)) => // z.
   by rewrite mulr_ge0 //= ler_piMr // le1_mu1.
 by move/(_ x)/eqP; rewrite mulf_eq0 (negbTE mu_x) /= => /eqP.
 Qed.
+
 End BindTheory.
 
 (* -------------------------------------------------------------------- *)
@@ -515,7 +516,7 @@ rewrite (eq_psum (F2 := fun y => PosSum.psum (S^~ y))) => [x|].
   by rewrite -psumZ //; apply/eq_psum => y /=.
 rewrite interchange_psum.
 + by move=> x; apply/summableZ/summable_mlet.
-+ rewrite {}/S; apply/(le_summable (F2 := mu)) => //.
++ rewrite {}/S; apply/(le_summable (g := mu)) => //.
   move=> x; rewrite ge0_psum /= psumZ ?ler_piMr //.
   apply/(le_trans _ (le1_mu (f1 x)))/le_psum => //.
   by move=> y; rewrite mulr_ge0 //= ler_piMr ?le1_mu1.
@@ -855,7 +856,7 @@ Implicit Types (mu : {distr T / R}) (A B E : pred T).
 
 Lemma summable_pr E mu : summable (fun x => (E x)%:R * mu x).
 Proof.
-apply/(le_summable (F2 := mu)) => [x|]; last by apply/summable_mu.
+apply/(le_summable (g := mu)) => [x|]; last by apply/summable_mu.
   by rewrite mulr_ge0 ?ler0n //= ler_piMl // lern1 leq_b1.
 Qed.
 
diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v
index 83ccb3421a..80b7b2e90c 100644
--- a/experimental_reals/realsum.v
+++ b/experimental_reals/realsum.v
@@ -29,7 +29,7 @@ Local Notation simpm := Monoid.simpm.
 
 (* -------------------------------------------------------------------- *)
 Section Summable.
-Variables (T : choiceType) (R : realType) (f : T -> R).
+Context {T : choiceType} {R : realType} (f : T -> R).
 
 Definition summable := exists (M : R), forall (J : {fset T}),
   \sum_(x : J) `|f (val x)| <= M.
@@ -44,8 +44,8 @@ Qed.
 
 End Summable.
 
-Lemma esum_summableP (T : choiceType) (R : realType) (f : T -> R) :
-  summable f <-> esum.summable [set: T] (EFin \o f).
+Lemma esum_summableP {T : choiceType} {R : realType} (f : T -> R) :
+  summable f <-> esummable [set: T] (EFin \o f).
 Proof.
 have fsbigsum (B : {fset T}) :
     (\sum_(x \in [set` B]) `|f x|%:E)%R = (\sum_(x : B) `|f (\val x)|)%:E.
@@ -53,15 +53,14 @@ have fsbigsum (B : {fset T}) :
   by rewrite sumEFin big_seq_fsetE/= (eq_bigl xpredT)// => x; apply/mem_set => /=.
 split.
   move=> [M fM].
-  rewrite /esum.summable.
-  rewrite ge0_esum// (@le_lt_trans _ _ M%:E) ?ltey//.
+  rewrite /esummable ge0_esum// (@le_lt_trans _ _ M%:E) ?ltey//.
   apply/ereal_supP => _/= [A [/finite_fsetP[B AB] _] <-].
   by rewrite AB fsbigsum; exact: fM.
-rewrite /summable => H.
+rewrite /summable => sf.
 exists (fine (\esum_(x in [set: T]) `|(EFin \o f) x|))%E => J/=.
 rewrite -lee_fin -fsbigsum fineK.
   by rewrite ge0_fin_numE// esum_ge0.
-by rewrite -esum_fset// !ge0_esum//; apply: PosEsum.subset_pos_esum.
+by rewrite -esum_fset// !ge0_esum//; exact: PosEsum.subset_pos_esum.
 Qed.
 
 Module PosSum.
@@ -80,7 +79,7 @@ Definition sum {R : realType} {T : choiceType} (f : T -> R) : R :=
 
 (* -------------------------------------------------------------------- *)
 Section SummableCountable.
-Variable (T : choiceType) (R : realType) (f : T -> R).
+Context {T : choiceType} {R : realType} (f : T -> R).
 
 Lemma summable_countn0 : summable f -> discrete.countable [pred x | f x != 0].
 Proof.
@@ -166,8 +165,7 @@ by move/ubP : (sup_upper_bound hs); apply; exists J.
 Qed.
 
 Lemma psum_sup_seq S : PosSum.psum S =
-  sup [set x | exists2 J : seq T,
-    uniq J & x = \sum_(x <- J) `|S x| ]%classic.
+  sup [set x | exists2 J : seq T, uniq J & x = \sum_(x <- J) `|S x| ]%classic.
 Proof.
 rewrite psum_sup; congr sup; rewrite predeqE => x; split.
   case=> J ->; exists (enum_fset J).
@@ -177,12 +175,10 @@ case=> J uqJ ->; exists [fset x in J].
 by rewrite (big_seq_fset \`|_|).
 Qed.
 
-Lemma eq_summable (S1 S2 : T -> R) :
-  (S1 =1 S2) -> summable S1 -> summable S2.
+Lemma eq_summable (f g : T -> R) : f =1 g -> summable f -> summable g.
 Proof.
-move=> eq_12 [M h]; exists M => J; rewrite (le_trans _ (h J)) //.
-rewrite le_eqVlt; apply/orP; left; apply/eqP/eq_bigr.
-by move=> /= K _; rewrite eq_12.
+move=> fg /esum_summableP sf; apply/esum_summableP.
+by apply: eq_esummable sf => x _; rewrite /= fg.
 Qed.
 
 Lemma eq_summableb (S1 S2 : T -> R) :
@@ -212,12 +208,11 @@ move=> eq_fg; rewrite /sum; congr (_ - _); apply/eq_psum.
 - exact/eq_funrneg.
 Qed.
 
-Lemma le_summable (F1 F2 : T -> R) :
-  (forall x, 0 <= F1 x <= F2 x) -> summable F2 -> summable F1.
+Lemma le_summable (f g : T -> R) :
+  (forall x, 0 <= f x <= g x) -> summable g -> summable f.
 Proof.
-move=> le_F [M leM]; exists M => J; apply/(le_trans _ (leM J)).
-apply/ler_sum => /= j _; case/andP: (le_F (val j)) => h1 h2.
-by rewrite !ger0_norm // (le_trans h1 h2).
+move=> fg /esum_summableP => sg; apply/esum_summableP.
+by apply: le_esummable sg => t _; rewrite /= !lee_fin fg.
 Qed.
 
 Lemma le_psum (F1 F2 : T -> R) :
@@ -355,9 +350,7 @@ End FinSumTh.
 
 (* -------------------------------------------------------------------- *)
 Section PSumGe.
-Context {R : realType} (T : choiceType).
-
-Variable (S : T -> R).
+Context {R : realType} (T : choiceType) (S : T -> R).
 
 Lemma ger_big_psum r : uniq r -> summable S ->
   \sum_(x <- r) `|S x| <= PosSum.psum S.
@@ -386,9 +379,7 @@ End PSumGe.
 
 (* -------------------------------------------------------------------- *)
 Section PSumNatGe.
-Context {R : realType}.
-
-Variable (S : nat -> R) (smS : summable S).
+Context {R : realType} (S : nat -> R) (smS : summable S).
 
 Lemma ger_big_ord_psum n : \sum_(i < n) `|S i| <= PosSum.psum S.
 Proof.
@@ -400,9 +391,7 @@ End PSumNatGe.
 
 (* -------------------------------------------------------------------- *)
 Section PSumCnv.
-Context {R : realType}.
-
-Variable (S : nat -> R).
+Context {R : realType} (S : nat -> R).
 
 Hypothesis ge0_S : (forall n, 0 <= S n).
 Hypothesis smS   : summable S.
@@ -453,16 +442,15 @@ End PSumCnv.
 
 (* -------------------------------------------------------------------- *)
 Section PSumAsLim.
-Context {R : realType} {T : choiceType}.
-
-Variable (S : T -> R) (P : nat -> {fset T}).
+Context {R : realType} {T : choiceType} (S : T -> R) (P : nat -> {fset T}).
 
 Hypothesis ge0_S   : (forall x, 0 <= S x).
 Hypothesis smS     : summable S.
 Hypothesis homo_P  : forall n m, (n <= m)%N -> (P n `<=` P m).
 Hypothesis cover_P : forall x, S x != 0 -> exists n, x \in P n.
 
-Lemma psum_as_lim : PosSum.psum S = fine (nlim (fun n => \sum_(j : P n) (S (val j)))).
+Lemma psum_as_lim :
+  PosSum.psum S = fine (nlim (fun n => \sum_(j : P n) (S (val j)))).
 Proof.
 set v := fun n => _; have hm_v m n: (m <= n)%N -> v m <= v n.
   by move=> le_mn; apply/big_fset_subset/fsubsetP/homo_P.
@@ -523,23 +511,18 @@ Qed.
 Lemma summable0 : summable (fun _ : T => 0 : R).
 Proof. by exists 0 => J; rewrite big1 ?normr0. Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableD (S1 S2 : T -> R) :
-  summable S1 -> summable S2 -> summable (S1 \+ S2).
+Lemma summableD (f g : T -> R) : summable f -> summable g -> summable (f \+ g).
 Proof.
-case=> [M1 h1] [M2 h2]; exists (M1 + M2) => J /=.
-pose M := \sum_(x : J) (`|S1 (val x)| + `|S2 (val x)|).
-rewrite (@le_trans _ _ M) // ?ler_sum // => [K _|].
-  by rewrite ler_normD.
-by rewrite /M big_split lerD ?(h1, h2).
+move=> sf sg; apply/esum_summableP.
+rewrite [X in esummable _ X](_ : _ = (EFin \o f) \+ (EFin \o g))%E//.
+by apply/esummableD; exact/esum_summableP.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableN (S : T -> R) : summable S -> summable (- S).
+Lemma summableN (f : T -> R) : summable f -> summable (- f).
 Proof.
-case=> [M h]; exists M => J; rewrite (le_trans _ (h J)) //.
-rewrite le_eqVlt; apply/orP; left; apply/eqP/eq_bigr.
-by move=> /= K _; rewrite normrN.
+move=> sf; apply/esum_summableP.
+rewrite [X in esummable _ X](_ : _ = \- (EFin \o f))%E//.
+by rewrite -esummableN; exact/esum_summableP.
 Qed.
 
 (* -------------------------------------------------------------------- *)
@@ -568,47 +551,40 @@ move=> sm1; rewrite (@eq_summableb _ _ (S2 \+ S1)) ?summablebDl //.
 by move=> x /=; rewrite addrC.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableZ (S : T -> R) c : summable S -> summable (c \*o S).
+Lemma summableZ (f : T -> R) c : summable f -> summable (c \*o f).
 Proof.
-case=> [M h]; exists (`|c| * M) => J; move/(_ J): h => /=.
-move/(ler_wpM2l (normr_ge0 c)); rewrite mulr_sumr.
-move/(le_trans _); apply; rewrite le_eqVlt; apply/orP.
-by left; apply/eqP/eq_bigr=> j _; rewrite normrM.
+move/esum_summableP => sf; apply/esum_summableP.
+rewrite [X in esummable _ X](_ : _ = (fun x => c%:E * (f x)%:E)%E)//.
+exact: esummableZl.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableZr (S : T -> R) (c : R) :
-  summable S -> summable (c \o* S).
-Proof. by move=> smS; apply/summable_mulrC/summableZ. Qed.
+Lemma summableZr (f : T -> R) (c : R) : summable f -> summable (c \o* f).
+Proof. by move=> smS; exact/summable_mulrC/summableZ. Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableMl (S1 S2 : T -> R) :
-  (exists M, forall x, `|S1 x| <= M) -> summable S2 -> summable (S1 \* S2).
+Lemma summableMl (f g : T -> R) :
+  (exists M, forall x, `|f x| <= M) -> summable g -> summable (f \* g).
 Proof.
-case=> M leM smS2; apply/summable_abs.
-apply/(le_summable (F2 := M \*o \`|S2|)).
-+ by move=> x /=; rewrite normr_ge0 /= normrM ler_wpM2r.
-+ by apply/summableZ/summable_abs.
+case=> M leM smg; apply/summable_abs.
+apply/(le_summable (g := M \*o \`|g|)).
+- by move=> x /=; rewrite normr_ge0 /= normrM ler_wpM2r.
+- by apply/summableZ/summable_abs.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableMr (S1 S2 : T -> R) :
-  (exists M, forall x, `|S2 x| <= M) -> summable S1 -> summable (S1 \* S2).
-Proof. by move=> bd sm; apply/summable_mulrC/summableMl. Qed.
+Lemma summableMr (f g : T -> R) :
+  (exists M, forall x, `|g x| <= M) -> summable f -> summable (f \* g).
+Proof. by move=> bd sm; exact/summable_mulrC/summableMl. Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma summableM (S1 S2 : T -> R) :
-  summable S1 -> summable S2 -> summable (S1 \* S2).
+Lemma summableM (f g : T -> R) : summable f -> summable g -> summable (f \* g).
 Proof.
-move=> smS1 smS2; apply/summableMl => //; exists (PosSum.psum S1).
-by move=> x; apply/ger1_psum.
+move=> sf sg; apply/esum_summableP.
+rewrite [X in esummable _ X](_ : _ = (EFin \o f) \* (EFin \o g))%E//.
+by apply/esummableM; exact/esum_summableP.
 Qed.
 
 Lemma summable_funrpos (f : T -> R) : summable f -> summable f^\+.
 Proof.
-move/summable_abs; apply/le_summable => x.
-by rewrite funrpos_ge0 le_funrpos_norm.
+move=> sf; apply/esum_summableP; rewrite -funerpos.
+exact/esummable_funepos/esum_summableP.
 Qed.
 
 Lemma summable_funrneg (f : T -> R) : summable f -> summable f^\-.
@@ -650,13 +626,13 @@ Qed.
 
 (* -------------------------------------------------------------------- *)
 Lemma summable_sum (F : I -> T -> R) (P : pred I) r :
-    (forall i, P i -> summable (F i))
-  -> summable (fun x => \sum_(i <- r | P i) F i x).
+    (forall i, P i -> summable (F i)) ->
+  summable (fun x => \sum_(i <- r | P i) F i x).
 Proof.
 move=> sm_F; elim: r => [|i r ih].
   by apply/(eq_summable _ summable0) => x; rewrite big_nil.
 pose G x := (F i x) * (P i)%:R + \sum_(i <- r | P i) F i x.
-apply/(eq_summable (S1 := G)) => [x|].
+apply/(eq_summable (f := G)) => [x|].
   by rewrite {}/G big_cons; case: ifP=> Pi; rewrite !Monoid.simpm.
 apply/summableD => //; case/boolP: (P i) => [|_].
   by move/sm_F; apply/eq_summable => x; rewrite mulr1.
@@ -668,13 +644,10 @@ End SummableAlg.
 Lemma esum_sum {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.
+move=> fs; rewrite esumE /sum EFinB.
+rewrite -esum_psum//; first exact: summable_funrpos.
+rewrite -esum_psum//; first exact: summable_funrneg.
+by rewrite funerpos funerneg.
 Qed.
 
 (* -------------------------------------------------------------------- *)
diff --git a/theories/esum.v b/theories/esum.v
index dcedd52ddf..f358d3767c 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -19,7 +19,7 @@ From mathcomp Require Import topology sequences normedtype numfun.
 (*                       function whose codomain is included in the extended  *)
 (*                       reals; it is 0 if I = set0 and sup(\sum_A a) where A *)
 (*                       is a finite set included in I o.w.                   *)
-(*       summable D f := \esum_(x in D) `| f x | < +oo                        *)
+(*      esummable D f := \esum_(x in D) `| f x | < +oo                        *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -38,7 +38,7 @@ Local Open Scope ring_scope.
 Local Open Scope ereal_scope.
 
 Section set_of_fset_in_a_set.
-Variable (T : choiceType).
+Context {T : choiceType}.
 Implicit Type S : set T.
 
 Definition fsets S : set_system T := [set F | finite_set F /\ F `<=` S].
@@ -64,7 +64,7 @@ End set_of_fset_in_a_set.
   define a generic `esum` below, which should be preferred *)
 Module PosEsum.
 Section posesum.
-Variables (R : realFieldType) (T : choiceType).
+Context {R : realFieldType} {T : choiceType}.
 Implicit Types (S : set T) (f g : T -> \bar R).
 
 Definition pos_esum S g := ereal_sup [set \sum_(x \in B) g x | B in fsets S].
@@ -117,13 +117,13 @@ End posesum.
 Arguments eq_pos_esum {R T} S f g.
 
 Section posesum_realType.
-Variables (R : realType) (T : choiceType).
+Context {R : realType} {T : choiceType}.
 Implicit Types (S : set T) (f g : T -> \bar R).
 
 Local Notation "\esum_ ( i 'in' P ) A" := (pos_esum P (fun i => A)).
 
 Lemma subset_pos_esum (I J : set T) (a : T -> \bar R) :
-  (I `<=` J)%classic -> (\esum_(i in I) a i <= \esum_(i in J) a i)%E.
+  I `<=` J -> (\esum_(i in I) a i <= \esum_(i in J) a i)%E.
 Proof.
 move=> IJ; apply: ereal_sup_le => _/= [A [finA AI]] <-.
 by exists A => //; split => //; exact: subset_trans IJ.
@@ -155,13 +155,31 @@ Lemma pos_esum_ge (T1 : choiceType) (I : set T1) (a : T1 -> \bar R) x :
   x <= \esum_(i in I) a i.
 Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed.
 
-Lemma le_pos_esum S f g : (forall i, S i -> f i <= g i) ->
+(* TODO: better name wanted *)
+Lemma pos_esum_ge1 S f x : S x -> f x <= \esum_(i in S) f i.
+Proof.
+move=> Sx; apply: pos_esum_ge; exists [set x]; last by rewrite fsbig_set1.
+by split => //; rewrite sub1set inE.
+Qed.
+
+Lemma le_pos_esum {U : choiceType} (S : set U) (f g : U -> \bar R) :
+  (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 le_pos_esum_fine {U : choiceType} (A : set U) (B : set T)
+    (h : T -> U -> \bar R) :
+  (\esum_(i in A) (fine (\esum_(x in B) h x i))%:E <=
+  \esum_(i in A) (\esum_(x in B) h x i))%E.
+Proof.
+rewrite le_pos_esum // => u Au.
+have := pos_esum_ge0 B (h ^~ u).
+by case: (\esum_(x in B) _).
+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.
@@ -339,66 +357,104 @@ 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).
+Context {R : realFieldType} {T : choiceType}.
+Implicit Types (A : set T) (f g : T -> \bar R).
 
-Definition esum S f := PosEsum.pos_esum S f^\+ - PosEsum.pos_esum S f^\-.
+Definition esum A f := PosEsum.pos_esum A f^\+ - PosEsum.pos_esum A f^\-.
 
 Local Notation "\esum_ ( i 'in' P ) A" := (esum P (fun i => A)).
 
-Lemma eq_esum S f g : (forall i, S i -> f i = g i) ->
-  \esum_(i in S) f i = \esum_(i in S) g i.
+Lemma ge0_esum A f : (forall x, A x -> 0 <= f x) ->
+  \esum_(i in A) f i = ereal_sup [set \sum_(x \in B) f x | B in fsets A].
 Proof.
-by move=> e; congr (_ - _); apply: PosEsum.eq_pos_esum => i /set_mem/e fgi;
-  rewrite !(funeposE,funenegE) fgi.
+move=> ?; rewrite /esum PosEsum.ge0_pos_esum_funepos//.
+by rewrite PosEsum.ge0_pos_esum_funeneg// sube0.
 Qed.
 
-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].
+Lemma esumE A f :
+  \esum_(x in A) f x = \esum_(x in A) f^\+ x - \esum_(x in A) f^\- x.
 Proof.
-move=> ?.
-rewrite /esum PosEsum.ge0_pos_esum_funepos// PosEsum.ge0_pos_esum_funeneg//.
-by rewrite sube0.
+rewrite [in RHS]ge0_esum; first by move=> x _; exact: funepos_ge0.
+by rewrite [in RHS]ge0_esum.
+Qed.
+
+Lemma eq_esum A f g : (forall i, A i -> f i = g i) ->
+  \esum_(i in A) f i = \esum_(i in A) g i.
+Proof.
+by move=> e; congr (_ - _); apply: PosEsum.eq_pos_esum => i /set_mem/e fgi;
+  rewrite !(funeposE,funenegE) fgi.
 Qed.
 
 Lemma esum_set0 f : \esum_(i in set0) f i = 0.
 Proof. by rewrite /esum !PosEsum.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.
+Lemma esumN A f : (forall x, A x -> 0 <= f x) ->
+  \esum_(x in A) - f x = - \esum_(i in A) 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).
+  by move=> t /mem_set At; rewrite funeposN (@ge0_funenegE _ _ A).
 rewrite /PosEsum.pos_esum; congr (- ereal_sup _).
-apply: eq_imagel => B SB; apply: eq_fsbigr => x xB.
+apply: eq_imagel => B AB; apply: eq_fsbigr => x xB.
 rewrite funenegN (@ge0_funeposE _ _ B)// => y By; apply: f0.
-by case: SB => _; exact.
+by case: AB => _; exact.
 Qed.
 
 End esum.
-Arguments eq_esum {R T} S f g.
+Arguments eq_esum {R T} A f g.
 
 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).
+Context {R : realType} {T : choiceType}.
+Implicit Types (D : set T) (f : T -> \bar R).
+
+Lemma sum_esum_ge s (h : T -> R) : uniq s ->
+  (forall x, 0 <= h x)%R ->
+  (\sum_(j <- s) h j)%:E <= \esum_(i in [set: T]) (h i)%:E.
+Proof.
+move=> us f0; rewrite ge0_esum; first by move=> t _; rewrite lee_fin f0.
+apply: PosEsum.pos_esum_ge; exists [set` s] => //.
+by rewrite fsumEFin// fsbig_seq.
+Qed.
 
-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.
+Lemma le_esum D f g : (forall x, D x -> f x <= g x) ->
+  \esum_(i in D) f i <= \esum_(i in D) g i.
 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.
+move=> leD.
+have {}leD : {in D, forall x, f x <= g x} by move=> x /set_mem; exact: leD.
+rewrite /esum leeB//.
+- by apply: PosEsum.le_pos_esum => x /mem_set; exact: funepos_le.
+- by apply: PosEsum.le_pos_esum => x /mem_set; exact: funeneg_le.
 Qed.
 
-Lemma esum_ge0 S f : (forall x, S x -> 0 <= f x) -> 0 <= \esum_(i in S) f i.
+Lemma esum_ge0 D f : (forall x, D x -> 0 <= f x) -> 0 <= \esum_(i in D) 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.
+Lemma le_esum_fine {U : choiceType} (A : set U) (B : set T)
+    (f : T -> U -> \bar R) : (forall x y, 0 <= f x y) ->
+  \esum_(i in A) (fine (\esum_(x in B) f x i))%:E <=
+     \esum_(i in A) (\esum_(x in B) f x i).
+Proof.
+move=> hf.
+rewrite [leLHS]ge0_esum.
+  by move=> i _; rewrite lee_fin; apply: fine_ge0; exact: esum_ge0.
+rewrite [leRHS]ge0_esum; first by move=> i _; exact: esum_ge0.
+under [leLHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum//.
+under [leRHS]PosEsum.eq_pos_esum => i _ do rewrite ge0_esum//.
+exact: PosEsum.le_pos_esum_fine.
+Qed.
+
+Lemma subset_esum (I J : set T) f : (forall x, J x -> 0 <= f x) ->
+  I `<=` J -> \esum_(i in I) f i <= \esum_(i in J) f i.
+Proof.
+move=> f0 IJ.
+have I0f : forall x, I x -> 0 <= f x by move => x /IJ /f0.
+by rewrite !ge0_esum// PosEsum.subset_pos_esum.
+Qed.
+
+Lemma esum_fset D f : finite_set D -> (forall i, D i -> 0 <= f i) ->
+  \esum_(i in D) f i = \sum_(i \in D) f i.
 Proof. by move=> finF f0; rewrite ge0_esum//; exact: PosEsum.pos_esum_fset. Qed.
 
 End esum_realType.
@@ -410,6 +466,10 @@ move=> Df0; rewrite ge0_esum; last exact: PosEsum.pos_esum1.
 by move=> i /Df0 ->.
 Qed.
 
+Lemma esum0 {R : realFieldType} {I : choiceType} (D : set I) :
+  \esum_(i in D) @cst _ (\bar R) 0 i = 0.
+Proof. by rewrite esum1. Qed.
+
 Section esum_cond.
 Context {R : realType} {T : choiceType}.
 Implicit Types (A B : set T) (f : T -> \bar R).
@@ -483,6 +543,11 @@ Lemma esum_ge {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) x :
   x <= \esum_(i in I) f i.
 Proof. by move=> f0 If; rewrite ge0_esum// PosEsum.pos_esum_ge. Qed.
 
+(* TODO: is this lemma really useful? *)
+Lemma esum_if_eq_op_set1 {R : realType} {T : choiceType} (f : T -> \bar R)  x :
+  \esum_(i in [set: T]) (if x == i then f i else 0) = f x.
+Proof. by rewrite esum_if_eq_op esum_set1. 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.
@@ -493,6 +558,19 @@ exists [set x]; first by split => // t ->.
 by rewrite -esum_set1 esum_fset// => i ->; exact: f0.
 Qed.
 
+Lemma esum_neq0 {R : realType} {T : choiceType} (I : set T) (a : T -> \bar R) :
+  \esum_(i in I) a i != 0 -> exists2 i, i \in I & a i != 0.
+Proof.
+apply: contra_neqP => /forall2NP a0; apply: esum1 => t /mem_set It.
+by have [|/negP/negPn/eqP//] := a0 t; rewrite It.
+Qed.
+
+(* TODO: better name wanted *)
+Lemma esum_ge1 {R : realType} {T : choiceType} (I : set T) (f : T -> \bar R) :
+  (forall x, I x -> 0 <= f x) ->
+  forall x, I x -> f x <= \esum_(i in I) f i.
+Proof. by move=> f0 x Ix; rewrite ge0_esum//; exact: PosEsum.pos_esum_ge1. Qed.
+
 Section esumZ.
 Context {R : realType} {T : choiceType} (A : set T) (f : T -> \bar R).
 
@@ -699,7 +777,7 @@ Qed.
 Arguments esum_set_image {R T} a e P.
 
 Section esum_bigcup.
-Variables (R : realType) (T : choiceType) (K : set nat).
+Context {R : realType} {T : choiceType} (K : set nat).
 Implicit Types (J : nat -> set T) (a : T -> \bar R).
 
 Lemma esum_bigcupT J a : trivIset setT J -> (forall x, 0 <= a x) ->
@@ -759,28 +837,44 @@ move=> tF f0; rewrite esum_bigcupT// nneseries_esum//.
 by rewrite fun_true; apply: eq_esum => /= i _.
 Qed.
 
-Definition summable (T : choiceType) (R : realType) (D : set T)
+Definition esummable (T : choiceType) (R : realType) (D : set T)
   (f : T -> \bar R) := (\esum_(x in D) `| f x | < +oo)%E.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable)]
+Notation summable := esummable (only parsing).
 
-Section summable_lemmas.
+Section esummable_lemmas.
 Local Open Scope ereal_scope.
-Variables (T : choiceType) (R : realType).
+Context {T : choiceType} {R : realType}.
 Implicit Types (D : set T) (f : T -> \bar R).
 
-Lemma summable_pinfty D f : summable D f -> forall x, D x -> `| f x | < +oo.
+Lemma esummable_pinfty D f : esummable D f -> forall x, D x -> `| f x | < +oo.
 Proof.
 move=> Dfoo x Dx; apply: le_lt_trans Dfoo.
 rewrite (esumID [set x])// setI1 mem_set// esum_set1// leeDl//.
 exact: esum_ge0.
 Qed.
 
-Lemma summableE D f : summable D f = (\esum_(x in D) `| f x | \is a fin_num).
+Lemma esummableE D f : esummable D f = (\esum_(x in D) `| f x | \is a fin_num).
 Proof.
-rewrite /summable fin_numElt; apply/idP/idP => [->|/andP[]//].
+rewrite /esummable fin_numElt; apply/idP/idP => [->|/andP[]//].
 by rewrite andbT (lt_le_trans (ltNyr 0))//; exact: esum_ge0.
 Qed.
 
-Lemma summableD D f g : summable D f -> summable D g -> summable D (f \+ g).
+Lemma eq_esummable D f g : {in D, f =1 g} -> esummable D f -> esummable D g.
+Proof.
+move => eq_fg;  apply: le_lt_trans.
+by apply: le_esum => t Dt; rewrite eq_fg//; exact/mem_set.
+Qed.
+
+Lemma le_esummable D f g :
+  (forall x, D x -> 0 <= f x <= g x) -> esummable D g -> esummable D f.
+Proof.
+move=> fg; apply: le_lt_trans.
+apply: le_esum => t Dt; have/andP[f0 {}fg] := fg _ Dt.
+by rewrite !gee0_abs// (le_trans f0).
+Qed.
+
+Lemma esummableD D f g : esummable D f -> esummable D g -> esummable D (f \+ g).
 Proof.
 move=> Df Dg; apply: le_lt_trans (lte_add_pinfty Df Dg).
 rewrite -esumD//; do 2 rewrite ge0_esum//.
@@ -788,15 +882,15 @@ rewrite -esumD//; do 2 rewrite ge0_esum//.
 by apply: PosEsum.le_pos_esum => t Dt; exact: lee_abs_add.
 Qed.
 
-Lemma summableN D f : summable D f = summable D (\- f).
+Lemma esummableN D f : esummable D f = esummable D (\- f).
 Proof.
-by rewrite /summable; congr (_ < +oo); apply: eq_esum => t Dt; rewrite abseN.
+by rewrite /esummable; congr (_ < +oo); apply: eq_esum => t Dt; rewrite abseN.
 Qed.
 
-Lemma summableB D f g : summable D f -> summable D g -> summable D (f \- g).
-Proof. by move=> Df; rewrite summableN; exact: summableD. Qed.
+Lemma esummableB D f g : esummable D f -> esummable D g -> esummable D (f \- g).
+Proof. by move=> Df; rewrite esummableN; exact: esummableD. Qed.
 
-Lemma summable_funepos D f : summable D f -> summable D f^\+.
+Lemma esummable_funepos D f : esummable D f -> esummable D f^\+.
 Proof.
 apply: le_lt_trans.
 do 2 rewrite ge0_esum//.
@@ -804,7 +898,7 @@ 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^\-.
+Lemma esummable_funeneg D f : esummable D f -> esummable D f^\-.
 Proof.
 apply: le_lt_trans.
 do 2 rewrite ge0_esum//.
@@ -812,34 +906,80 @@ apply: PosEsum.le_pos_esum => t Dt.
 by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
 Qed.
 
-End summable_lemmas.
+Lemma esummableZl D f c : c \is a fin_num ->
+  esummable D f -> esummable D (fun x => c * f x).
+Proof.
+move=> cfin fy; rewrite /esummable; under eq_esum do rewrite abseM.
+by rewrite esumZ// lte_mul_pinfty// abse_fin_num.
+Qed.
+
+Lemma esummableZr D f c : c \is a fin_num ->
+  esummable D f -> esummable D (fun x => f x * c).
+Proof. by under eq_fun do rewrite muleC; exact: esummableZl. Qed.
+
+Lemma esummableMl D f1 f2 :
+  (exists2 M, forall x, D x -> `|f1 x| <= M & M \is a fin_num) ->
+  esummable D f2 -> esummable D (f1 \* f2).
+Proof.
+move=> [M Df1M Mfin] Df2; apply: le_lt_trans (esummableZl Mfin Df2).
+apply: le_esum => x Dx; rewrite !abseM.
+by rewrite lee_wpmul2r ?abse_ge0// (le_trans (Df1M x Dx) (lee_abs _)).
+Qed.
+
+Lemma esummableMr D f1 f2 :
+  (exists2 M, forall x, D x -> `|f2 x| <= M & M \is a fin_num) ->
+  esummable D f1 -> esummable D (f1 \* f2).
+Proof. by move=> Df2; under eq_fun do rewrite muleC; exact: esummableMl. Qed.
+
+Lemma esummableM D f1 f2 :
+  esummable D f1 -> esummable D f2 -> esummable D (f1 \* f2).
+Proof.
+rewrite esummableE => smS1 smS2; apply/esummableMl => //.
+by exists (\esum_(x in D) `|f1  x|) => //; exact: esum_ge1.
+Qed.
+
+End esummable_lemmas.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_pinfty)]
+Notation summable_pinfty := esummable_pinfty (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableE)]
+Notation summableE := esummableE (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableD)]
+Notation summableD := esummableD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableN)]
+Notation summableN := esummableN (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableB)]
+Notation summableB := esummableB (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_funepos)]
+Notation summable_funepos := esummable_funepos (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_funeneg)]
+Notation summable_funeneg := esummable_funeneg (only parsing).
 
 Import numFieldNormedType.Exports.
 
-Section summable_nat.
+Section esummable_nat.
 Local Open Scope ereal_scope.
-Variable R : realType.
+Context {R : realType}.
 
-Lemma summable_fine_sum r (P : pred nat) (f : (\bar R)^nat) : summable P f ->
+Lemma esummable_fine_sum r (P : pred nat) (f : (\bar R)^nat) : esummable 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.
 rewrite big_mkcond/= big_nat_recr// [in RHS]big_mkcond/= big_nat_recr//=.
 rewrite -!big_mkcond/= ih; case: ifPn => Pr => //; last by rewrite adde0 addr0.
 rewrite fineD//; last first.
-  by rewrite fin_num_abs (summable_pinfty Pf).
-by apply/sum_fin_numP => i ir Pi; rewrite fin_num_abs (summable_pinfty Pf).
+  by rewrite fin_num_abs (esummable_pinfty Pf).
+by apply/sum_fin_numP => i ir Pi; rewrite fin_num_abs (esummable_pinfty Pf).
 Qed.
 
-Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) :
-  (forall i, P i -> 0 <= f i)%E -> summable P f ->
+Lemma esummable_cvg (P : pred nat) (f : (\bar R)^nat) :
+  (forall i, P i -> 0 <= f i)%E -> esummable P f ->
   cvg ((fun n => \sum_(0 <= k < n | P k) fine (f k))%R @ \oo).
 Proof.
 move=> f0 Pf; apply: nondecreasing_is_cvgn.
   by apply: nondecreasing_series => n _ Pn; exact/fine_ge0/f0.
 exists (fine (\sum_(i <oo | P i) `|f i|)) => x /= [n _ <-].
-rewrite summable_fine_sum// -lee_fin fineK//.
-  by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (summable_pinfty Pf).
+rewrite esummable_fine_sum// -lee_fin fineK//.
+  by apply/sum_fin_numP => i ni Pi; rewrite fin_num_abs (esummable_pinfty Pf).
 rewrite fineK//.
   rewrite nneseries_esum// fin_numElt; apply/andP; split.
     by rewrite (@lt_le_trans _ _ 0)// ?lte_ninfty//; exact: esum_ge0.
@@ -849,8 +989,8 @@ apply: le_trans (nneseries_lim_ge n _) => //; apply: lee_sum => i _.
 by rewrite lee_abs.
 Qed.
 
-Lemma summable_nneseries_lim (P : pred nat) (f : (\bar R)^nat) :
-    (forall i, P i -> 0 <= f i)%E -> summable P f ->
+Lemma esummable_nneseries_lim (P : pred nat) (f : (\bar R)^nat) :
+    (forall i, P i -> 0 <= f i)%E -> esummable P f ->
   \sum_(i <oo | P i) f i =
   (lim ((fun n => (\sum_(0 <= k < n | P k) fine (f k))%R) @ \oo))%:E.
 Proof.
@@ -858,11 +998,11 @@ move=> f0 Pf; pose A_ n := (\sum_(0 <= k < n | P k) fine (f k))%R.
 transitivity (lim (EFin \o A_ @ \oo)).
   apply/congr_lim/funext => /= n; rewrite /A_ /= -sumEFin.
   apply eq_bigr => i Pi/=; rewrite fineK//.
-  by rewrite fin_num_abs (@summable_pinfty _ _ P).
-by rewrite EFin_lim//; apply: summable_cvg.
+  by rewrite fin_num_abs (@esummable_pinfty _ _ P).
+by rewrite EFin_lim//; exact: esummable_cvg.
 Qed.
 
-Lemma summable_eseries (f : (\bar R)^nat) (P : pred nat) : summable P f ->
+Lemma esummable_eseries (f : (\bar R)^nat) (P : pred nat) : esummable P f ->
   \sum_(i <oo | P i) (f i) =
   \sum_(i <oo | P i) f^\+ i - \sum_(i <oo | P i) f^\- i.
 Proof.
@@ -874,42 +1014,52 @@ pose A := lim (A_ @ \oo).
 pose B := lim (B_ @ \oo).
 suff: ((fun n => C_ n - (A - B)) @ \oo --> (0 : R^o))%R.
   move=> CAB.
-  rewrite [X in  X - _]summable_nneseries_lim//; first exact/summable_funepos.
-  rewrite [X in _ - X]summable_nneseries_lim//; first exact/summable_funeneg.
+  rewrite [X in  X - _]esummable_nneseries_lim//; first exact/esummable_funepos.
+  rewrite [X in _ - X]esummable_nneseries_lim//; first exact/esummable_funeneg.
   rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first.
     exact: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB).
   apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
   by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge.
 have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R.
   apply: cvgD.
-  - by apply: summable_cvg => //; exact/summable_funepos.
-  - by apply: cvgN; apply: summable_cvg => //; exact/summable_funeneg.
+  - by apply: esummable_cvg => //; exact/esummable_funepos.
+  - by apply: cvgN; apply: esummable_cvg => //; exact/esummable_funeneg.
 move=> /cvgrPdist_lt cvgAB; apply/cvgrPdist_lt => e e0.
 move: cvgAB => /(_ _ e0) [N _/= hN] /=.
 near=> n.
 rewrite distrC subr0.
 have -> : (C_ = A_ \- B_)%R.
   apply/funext => k.
-  rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
+  rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -esummable_fine_sum//.
   apply eq_bigr => i Pi; rewrite -fineB//.
-  - by rewrite fin_num_abs (@summable_pinfty _ _ P)// summable_funepos.
-  - by rewrite fin_num_abs (@summable_pinfty _ _ P)// summable_funeneg.
+  - by rewrite fin_num_abs (@esummable_pinfty _ _ P)// esummable_funepos.
+  - by rewrite fin_num_abs (@esummable_pinfty _ _ P)// esummable_funeneg.
   - by rewrite -[in LHS](funeposBneg f).
 by rewrite distrC; apply: hN; near: n; exists N.
 Unshelve. all: by end_near. Qed.
 
-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^\-.
+Lemma esummable_eseries_esum (f : (\bar R)^nat) (P : pred nat) :
+  esummable P f -> \sum_(i <oo | P i) f i = esum P f^\+ - esum P f^\-.
 Proof.
 move=> Pfoo.
-by rewrite -nneseries_esum// -nneseries_esum// [LHS]summable_eseries.
+by rewrite -nneseries_esum// -nneseries_esum// [LHS]esummable_eseries.
 Qed.
 
-End summable_nat.
+End esummable_nat.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_fine_sum)]
+Notation summable_fine_sum := esummable_fine_sum (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_cvg)]
+Notation summable_cvg := esummable_cvg (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_nneseries_lim)]
+Notation summable_nneseries_lim := esummable_nneseries_lim (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_eseries)]
+Notation summable_eseries := esummable_eseries (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_eseries_esum)]
+Notation summable_eseries_esum := esummable_eseries_esum (only parsing).
 
 Section esumB.
 Local Open Scope ereal_scope.
-Variables (R : realType) (T : choiceType).
+Context {R : realType} {T : choiceType}.
 Implicit Types (D : set T) (f g : T -> \bar R).
 
 Let esum_posneg D f := esum D f^\+ - esum D f^\-.
@@ -922,7 +1072,7 @@ move=> Sa; rewrite /esum_posneg [X in _ - X](_ : _ = 0) ?sube0.
 apply: eq_esum => t St; rewrite funeposE; apply/max_idPl; exact: Sa.
 Qed.
 
-Lemma esumB D f g : summable D f -> summable D g ->
+Lemma esumB D f g : esummable D f -> esummable D g ->
   (forall i, D i -> 0 <= f i) -> (forall i, D i -> 0 <= g i) ->
   \esum_(i in D) (f \- g)^\+ i - \esum_(i in D) (f \- g)^\- i =
   \esum_(i in D) f i - \esum_(i in D) g i.
@@ -934,32 +1084,116 @@ have /eqP : esum D (f \- g)^\+ + esum_posneg D g =
   apply eq_esum => i Di; rewrite funeposE funenegE.
   have [fg|fg] := leP 0 (f i - g i).
     rewrite max_r 1?leeNl ?oppe0// add0e subeK//.
-    by rewrite fin_num_abs (summable_pinfty Dg).
+    by rewrite fin_num_abs (esummable_pinfty Dg).
   rewrite add0e max_l; first by rewrite leeNr oppe0 ltW.
-  rewrite fin_num_oppeB//; first by rewrite fin_num_abs (summable_pinfty Dg).
-  by rewrite -addeA addeCA addeA subeK// fin_num_abs (summable_pinfty Df).
+  rewrite fin_num_oppeB//; first by rewrite fin_num_abs (esummable_pinfty Dg).
+  by rewrite -addeA addeCA addeA subeK// fin_num_abs (esummable_pinfty Df).
 rewrite [X in _ == X -> _]addeC -sube_eq.
 - rewrite fin_numD; apply/andP; split.
     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)//.
+    by rewrite -esummableE; exact/esummable_funepos/esummableB.
+  move: Dg; rewrite esummableE (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))// -?esummableE// => i Di.
   by rewrite /= gee0_abs// f0.
 rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq.
-- rewrite ge0_esum_posneg// (eq_esum _ _ (abse \o f))// -?summableE// => i Di.
+- rewrite ge0_esum_posneg// (eq_esum _ _ (abse \o f))// -?esummableE// => i Di.
   by rewrite /= gee0_abs// f0.
 - rewrite fin_num_adde_defl// ge0_esum_posneg//.
-  rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di.
+  rewrite (@eq_esum _ _ _ _ (abse \o g))// -?esummableE// => i Di.
   by rewrite /= gee0_abs// g0.
 by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
 Qed.
 
 End esumB.
 
+Section esum_summable.
+Context {R : realType} {T : choiceType}.
+Implicit Types (D : set T) (f g : T -> \bar R).
+
+Lemma esummable_esum_funepos D f :
+  esummable D f -> \esum_(t in D) f^\+ t \is a fin_num.
+Proof.
+move=> /esummable_funepos; rewrite esummableE => ffin.
+by rewrite (eq_esum _ _ (fun y => `|f^\+ y|))//= => t Dt; rewrite gee0_abs.
+Qed.
+
+Lemma esummable_esum_funeneg D f :
+  esummable D f -> \esum_(t in D) f^\- t \is a fin_num.
+Proof.
+rewrite esummableN => /esummable_esum_funepos.
+by under eq_esum do rewrite funeposN.
+Qed.
+
+Lemma esummable_esum_fin_num D f :
+  esummable D f -> \esum_(i in D) f i \is a fin_num.
+Proof.
+by move=> sm; rewrite esumE fin_numB; apply/andP; split;
+  [exact: esummable_esum_funepos|exact: esummable_esum_funeneg].
+Qed.
+
+Lemma esummable_esumN D f :
+  esummable D f -> \esum_(i in D) - f i = - \esum_(i in D) f i.
+Proof.
+move=> hs; rewrite [in RHS]esumE oppeB.
+  by rewrite fin_num_adde_defr// esummable_esum_funepos.
+rewrite [in LHS]esumE.
+under eq_esum do rewrite funeposN.
+under [in X in _ - X]eq_esum do rewrite funenegN.
+by rewrite addeC.
+Qed.
+
+Let nonneg_esummable_esumZ D f d : esummable D f -> 0 <= d -> d \is a fin_num ->
+  \esum_(x in D) d * f x = d * \esum_(x in D) f x.
+Proof.
+move=> h d0 dfin.
+have -> : d = (fine d)%:E by rewrite fineK.
+have ? : (0 <= fine d)%R  by rewrite -lee_fin fineK.
+rewrite [in RHS]esumE muleBr//.
+  by rewrite fin_num_adde_defr// esummable_esum_funepos.
+by rewrite -!esumZ// -(ge0_funeposM f)// -(ge0_funenegM f)// -esumE.
+Qed.
+
+Lemma esummable_esumZ D f c : `|c| \is a fin_num -> esummable D f ->
+  \esum_(x in D) c * f x = c * \esum_(x in D) f x.
+Proof.
+move=> cmin Df; have [c0|c0|->] := comparable_ltgtP (comparableT c 0).
+- rewrite -(oppeK c) -(@lte0_abs _ c)//.
+  under [LHS]eq_esum do rewrite mulNe.
+  rewrite esummable_esumN; first exact: esummableZl.
+  by rewrite nonneg_esummable_esumZ// mulNe.
+- by rewrite (nonneg_esummable_esumZ _ (ltW c0))// -abse_fin_num.
+- by rewrite mul0e esum1// => t _; rewrite mul0e.
+Qed.
+
+Lemma esummable_esumD D f g : esummable D f -> esummable D g ->
+  \esum_(x in D) (f x + g x) = \esum_(x in D) f x + \esum_(x in D) g x.
+Proof.
+move=> sm1 sm2.
+rewrite -(funeDB f g) (esumE _ ((f^\+ \+ g^\+) \- (f^\- \+ g^\-))).
+rewrite (@esumB _ _ D (f^\+ \+ g^\+) (f^\- \+ g^\-)).
+  by apply: esummableD => //; exact: esummable_funepos.
+  by apply: esummableD => //; exact: esummable_funeneg.
+  by move=> t _; rewrite adde_ge0.
+  by move=> t _; rewrite adde_ge0.
+rewrite esumD// esumD// [in RHS](esumE _ f) [in RHS](esumE _ g) oppeD.
+  rewrite fin_num_adde_defl// esummable_esum_fin_num//.
+  exact: esummable_funeneg.
+by rewrite addeACA.
+Qed.
+
+Lemma esummable_esumB D f g : esummable D f -> esummable D g ->
+  \esum_(x in D) (f x - g x) = \esum_(x in D) f x - \esum_(x in D) g x.
+Proof.
+move=> sm1 sm2.
+by rewrite esummable_esumD ?esummable_esumN// -esummableN.
+Qed.
+
+End esum_summable.
+
 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.
@@ -970,10 +1204,8 @@ Lemma exchange_esum_ereal_sup (A : set T) :
   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.
++ by move=> x Ax; apply: le_ereal_sup_tmp; exists (f x 0).
+under eq_imagel => B [fin BA] do rewrite fsbig_finite//= ereal_sup_sum//.
 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.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v
index 706a0a57b4..10d9bcf564 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integrable.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v
@@ -887,16 +887,15 @@ End integral_measure_add.
 
 Section subadditive_countable.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variable (mu : {measure set T -> \bar R}).
+Context {d} {T : measurableType d} {R : realType} (mu : {measure set T -> \bar R}).
 
-Lemma integrable_summable (F : (set T)^nat) (g : T -> \bar R):
+Lemma integrable_esummable (F : (set T)^nat) (g : T -> \bar R):
   trivIset setT F -> (forall k, measurable (F k)) ->
   mu.-integrable (\bigcup_k F k) g ->
-  summable [set: nat] (fun i => \int[mu]_(x in F i) g x).
+  esummable [set: nat] (fun i => \int[mu]_(x in F i) g x).
 Proof.
 move=> tF mF fi.
-rewrite /summable -(_ : [set _ | true] = setT); first exact/seteqP.
+rewrite /esummable -(_ : [set _ | true] = setT); first exact/seteqP.
 rewrite -nneseries_esum//.
 have [mf {fi}] := integrableP _ _ _ fi.
 rewrite ge0_integral_bigcup//; first exact: measurableT_comp.
@@ -938,24 +937,25 @@ transitivity ((\sum_(i <oo) \int[mu]_(x in F i) g^\+ x) -
 rewrite [X in X - _]nneseries_esum; first by move=> n _; exact: integral_ge0.
 rewrite [X in _ - X]nneseries_esum; first by move=> n _; exact: integral_ge0.
 rewrite set_true -esumB//=.
-  - apply: integrable_summable => //; apply: integrable_funepos => //.
+  - apply: integrable_esummable => //; apply: integrable_funepos => //.
     exact: bigcup_measurable.
-  - apply: integrable_summable => //; apply: integrable_funeneg => //.
+  - apply: integrable_esummable => //; apply: integrable_funeneg => //.
     exact: bigcup_measurable.
   - by move=> n _; exact: integral_ge0.
   - by move=> n _; exact: integral_ge0.
-rewrite summable_eseries.
-  under [X in summable _ X]eq_fun do rewrite -integralE.
-  by rewrite fun_true; exact: integrable_summable.
+rewrite esummable_eseries.
+  under [X in esummable _ X]eq_fun do rewrite -integralE.
+  by rewrite fun_true; exact: integrable_esummable.
 by congr (_ - _)%E; rewrite nneseries_esum// set_true.
 Qed.
 
 End subadditive_countable.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=integrable_esummable)]
+Notation integrable_summable := integrable_esummable (only parsing).
 
 Section sequence_of_measures.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variable m_ : {measure set T -> \bar R}^nat.
+Context {d} {T : measurableType d} {R : realType} (m_ : {measure set T -> \bar R}^nat).
 Let m := mseries m_ O.
 
 Lemma integral_measure_series (D : set T) (mD : measurable D) (f : T -> \bar R) :
@@ -983,11 +983,11 @@ have fineKp : \sum_(n <oo) `|\int[m_ n]_(x in D) f^\+ x| =
 rewrite nneseries_esum; first by move=> n _; exact/fine_ge0/integral_ge0.
 rewrite nneseries_esum; first by move=> n _; exact/fine_ge0/integral_ge0.
 rewrite -esumB//.
-  - by rewrite /= /summable -nneseries_esum// -fineKp.
-  - by rewrite /summable /= -nneseries_esum// -fineKn; exact: fmoo.
+  - by rewrite /= /esummable -nneseries_esum// -fineKp.
+  - by rewrite /esummable /= -nneseries_esum// -fineKn; exact: fmoo.
   - by move=> n _; exact/fine_ge0/integral_ge0.
   - by move=> n _; exact/fine_ge0/integral_ge0.
-rewrite -summable_eseries_esum.
+rewrite -esummable_eseries_esum.
   apply: (@le_lt_trans _ _ (\esum_(i in (fun=> true))
      `|(fine (\int[m_ i]_(x in D) f x))%:E|)).
     do 2 rewrite ge0_esum//.
@@ -1012,9 +1012,9 @@ End sequence_of_measures.
 
 Section integral_counting.
 Local Open Scope ereal_scope.
-Variable R : realType.
+Context {R : realType}.
 
-Lemma integral_count (a : nat -> \bar R) : summable setT a ->
+Lemma integral_count (a : nat -> \bar R) : esummable [set: nat] a ->
   \int[counting]_t (a t) = \sum_(k <oo) (a k).
 Proof.
 move=> sa.
@@ -1023,10 +1023,10 @@ transitivity (\int[mseries (fun n => \d_ n) O]_t a t).
   by rewrite /= counting_dirac.
 rewrite (@integral_measure_series _ _ R (fun n => \d_ n) setT)//=.
 - move=> n; apply/integrableP; split=> [//|].
-  by rewrite integral_dirac//= diracT mul1e (summable_pinfty sa).
-- by apply: summable_integral_dirac => //; exact: summable_funeneg.
-- by apply: summable_integral_dirac => //; exact: summable_funepos.
-- by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e.
+  by rewrite integral_dirac//= diracT mul1e (esummable_pinfty sa).
+- by apply: esummable_integral_dirac => //; exact: esummable_funeneg.
+- by apply: esummable_integral_dirac => //; exact: esummable_funepos.
+- by apply: eq_eseriesr => i _; rewrite integral_dirac//= diracT mul1e.
 Qed.
 
 End integral_counting.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index 9c8a37166b..e17b6b8827 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -649,17 +649,19 @@ Qed.
 
 End integral_dirac.
 
-Lemma summable_integral_dirac {R : realType} (a : (\bar R)^nat) :
-  summable setT a -> (\sum_(n <oo) `|\int[\d_ n]_x a x| < +oo)%E.
+Lemma esummable_integral_dirac {R : realType} (a : (\bar R)^nat) :
+  esummable [set: nat] a -> (\sum_(n <oo) `|\int[\d_ n]_x a x| < +oo)%E.
 Proof.
 move=> sa.
 apply: (@le_lt_trans _ _ (\sum_(i <oo) `|fine (a i)|%:E))%E.
   apply: lee_nneseries => // n _; rewrite integral_dirac//.
-  move: (@summable_pinfty _ _ _ _ sa n Logic.I).
+  move: (@esummable_pinfty _ _ _ _ sa n Logic.I).
   by case: (a n) => //= r _; rewrite indicE/= mem_set// mul1r.
-move: (sa); rewrite /summable -fun_true -nneseries_esum//; apply: le_lt_trans.
+move: (sa); rewrite /esummable -fun_true -nneseries_esum//; apply: le_lt_trans.
 by apply: lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_integral_dirac)]
+Notation summable_integral_dirac := esummable_integral_dirac (only parsing).
 
 Section integral_measure_sum_nnsfun.
 Local Open Scope ereal_scope.
diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v
index 57526df8eb..e465a7b599 100644
--- a/theories/measure_theory/measure_function.v
+++ b/theories/measure_theory/measure_function.v
@@ -1212,8 +1212,7 @@ rewrite esum_bigcup//.
    apply: (@trivIset_seqDU _ B) => //; exists y.
    by split => //; [exact: YBi|exact: YBj].
 rewrite nneseries_esumT//.
-apply: le_esum => /=; first by move=> i _; exact: esum_ge0.
-move=> // i _.
+apply: le_esum  => /= 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//=.