fix

Author: affeldt-aist

experimental_reals/realsum.v

@@ -267,21 +267,21 @@ Lemma esum_psum {R : realType} {T : choiceType} (f : T -> R) :
     (forall i, 0 <= f i) -> summable f ->
   \esum_(x in [set: T]) (f x)%:E = (psum f)%:E.
 Proof.
-move => f0 h; apply/eqP; rewrite eq_le; apply/andP; split.
+move=> f0 sumf; apply/eqP; rewrite eq_le; apply/andP; split.
 - rewrite ge0_esum; first by move=> t _; rewrite lee_fin.
-  rewrite ge_ereal_sup//= => x [X [finX _]].
-  rewrite fsumEFin // => <-.
+  rewrite ge_ereal_sup//= => x [A [finA _]].
+  rewrite fsumEFin// => <-.
   rewrite lee_fin fsbig_finite//=.
-  move/finite_fsetP : finX => [J ->].
-  rewrite set_fsetK (le_trans _ (gerfin_psum J h))//.
+  move/finite_fsetP : finA => [J ->].
+  rewrite set_fsetK (le_trans _ (gerfin_psum J sumf))//.
   by rewrite -big_fset_seq//= (le_trans _ (ler_norm_sum _ _ _))// ler_norm.
 - rewrite (eq_esum _ _ (fun x => `|f x|%:E)).
     by move => t _; rewrite ger0_norm.
-  have [nonempty hasub] := summable_sup h.
-  rewrite psum_absE// -ereal_sup_EFin// ge_ereal_sup//= => x [X [Fs ->] <-].
-  rewrite esum_ge//;  exists [set` Fs]%classic => //.
-  rewrite fsumEFin// lee_fin (big_fset_seq (fun x => `|f x|))//=.
-  by rewrite -{1}(set_fsetK Fs) -fsbig_finite.
+  have [nonempty hasub] := summable_sup sumf.
+  rewrite psum_absE// -ereal_sup_EFin// ge_ereal_sup//= => x [r [J ->] <-].
+  rewrite esum_ge//; exists [set` J]%classic => //.
+  rewrite fsumEFin// lee_fin (big_fset_seq (Num.Def.normr \o f))//=.
+  by rewrite -[in leLHS](set_fsetK J) -fsbig_finite.
 Qed.
 
 (* -------------------------------------------------------------------- *)
@@ -636,8 +636,7 @@ End SummableAlg.
 Lemma esumEsum {T : choiceType} {R : realType} (f : T -> R) : summable f ->
   \esum_(x in [set: T]) (f x)%:E = (sum f)%:E.
 Proof.
-move=> hs; rewrite /esum.
-rewrite EFinB; congr (_ - _)%E.
+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.

theories/esum.v

@@ -332,20 +332,27 @@ Section esum.
 Variables (R : realFieldType) (T : choiceType).
 Implicit Types (S : set T) (f g : T -> \bar R).
 
-Import PosEsum.
-
-Definition esum S f := pos_esum S f^\+ - pos_esum S f^\-.
+Definition esum S f := PosEsum.pos_esum S f^\+ - PosEsum.pos_esum S 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.
+Proof.
+by move=> e; congr (_ - _); apply: PosEsum.eq_pos_esum => i /set_mem/e fgi;
+  rewrite !(funeposE,funenegE) fgi.
+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].
 Proof.
-by move=> ?; rewrite /esum ge0_pos_esum_funepos// ge0_pos_esum_funeneg// sube0.
+move=> ?.
+rewrite /esum PosEsum.ge0_pos_esum_funepos// PosEsum.ge0_pos_esum_funeneg//.
+by rewrite sube0.
 Qed.
 
 Lemma esum_set0 f : \esum_(i in set0) f i = 0.
-Proof. by rewrite /esum !pos_esum_set0 subee. Qed.
+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.
@@ -360,6 +367,7 @@ by case: SB => _; exact.
 Qed.
 
 End esum.
+Arguments eq_esum {R T} S f g.
 
 Notation "\esum_ ( i 'in' P ) F" := (esum P (fun i => F)) : ring_scope.
 
@@ -388,19 +396,9 @@ End esum_realType.
 Lemma esum1 {R : realFieldType} {I : choiceType} (D : set I) (f : I -> \bar R) :
   (forall i, D i -> f i = 0) -> \esum_(i in D) f i = 0.
 Proof.
-move=> a0; rewrite ge0_esum; last exact: PosEsum.pos_esum1.
-by move=> i /a0 ->.
-Qed.
-
-Lemma eq_esum {R : realFieldType} {T : choiceType} (A : set T)
-    (f g : T -> \bar R) : (forall i, A i -> f i = g i) ->
-  \esum_(i in A) f i = \esum_(i in A) g i.
-Proof.
-move=> e; congr (_ - _).
-- by apply: PosEsum.eq_pos_esum => i /set_mem/e abi; rewrite !funeposE abi.
-- by apply: PosEsum.eq_pos_esum => i /set_mem/e abi; rewrite !funenegE abi.
+move=> Df0; rewrite ge0_esum; last exact: PosEsum.pos_esum1.
+by move=> i /Df0 ->.
 Qed.
-Arguments eq_esum {R T} A f g.
 
 Section esum_cond.
 Context {R : realType} {T : choiceType}.