Module mathcomp.analysis.esum

From mathcomp Require Import boot order 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.

# Summation over classical sets This file provides a definition of sum over classical sets and a few lemmas in particular for the case of sums of non-negative terms. ``` fsets S == the set of finite sets (fset) included in S \esum_(i in I) f i == summation of non-negative extended real numbers over classical sets; I is a classical set and f is a 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 ```

Reserved Notation "\esum_ ( i 'in' P ) F"
(at level 41, F at level 41, format "\esum_ ( i 'in' P ) F").

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Local Open Scope ereal_scope.

Section set_of_fset_in_a_set.
Variable ( : choiceType).
Implicit Type S : set T.

Definition : set_system T := [set | finite_set F /\ F `<=` S].

Lemma : fsets S set0

Proof.

by split. Qed.

Lemma : fsets [set: T] = finite_set.

Proof.

by apply/funext=> ?; apply/propext; split => // -[]. Qed.

Lemma ( : set T) : finite_set F -> fsets F F.

Proof.

by move=> finF; split. Qed.

Lemma : fsets set0 = [set set0].

Proof.

rewrite predeqE => A; split => [|->]; last exact: fsets_set0.
by rewrite /fsets/= subset0 => -[].
Qed.

End set_of_fset_in_a_set.

This module is for internal use. It defines `esum` in the particular case of non-negative functions and is then used to define a generic `esum` below, which should be preferred

Module .
Section posesum.
Variables ( : realFieldType) ( : choiceType).
Implicit Types (S : set T) (f g : T -> \bar R).

Definition := ereal_sup [set \sum_( \in B) g x | in fsets S].

Local Notation := (pos_esum P (fun => A)).

Lemma : \esum_( in set0) f i = 0.

Proof.

rewrite /pos_esum fsets0 [X in ereal_sup X](_ : _ = [set 0%E]) ?ereal_sup1//.
apply/seteqP; split=> [x [_ /= ->]|x]; first by rewrite fsbig_set0.
by move=> -> /=; exists set0 => //; rewrite fsbig_set0.
Qed.

Lemma : (forall , S x -> 0 <= f x) ->
\esum_( in S) f^\- i = 0.

Proof.

move=> a0; rewrite /pos_esum [X in ereal_sup X](_ : _ = [set 0]) ?ereal_sup1//.
apply/seteqP; split => [/= x /= [A SA <-]|].
  rewrite fsbig1//= => t At.
  rewrite (@ge0_funenegE _ _ A)//; last exact/mem_set.
  by move=> u; case: SA => _ => /[apply] /a0.
rewrite sub1set inE/=; exists set0; first exact: fsets_set0.
by rewrite fsbig_set0.
Qed.

Lemma : {in S, f =1 g} ->
\esum_( in S) f i = \esum_( in S) g i.

Proof.

move=> eq_fg; rewrite /pos_esum; congr ereal_sup.
apply/seteqP; split => [_/= [B SB <-]|_/= [B SB <-]].
- exists B => //; apply: eq_fsbigr => i iB.
exact/esym/eq_fg/mem_set/SB.2/set_mem.
- exists B => //; apply: eq_fsbigr => i iB.
exact/eq_fg/mem_set/SB.2/set_mem.
Qed.

Lemma : (forall , S x -> 0 <= f x) ->
\esum_( in S) f^\+ i = \esum_( in S) f i.

Proof.

by move=> a0; apply: eq_pos_esum; exact: ge0_funeposE. Qed.

Lemma : (forall , S i -> f i = 0) -> \esum_( in S) f i = 0.

Proof.

move=> a0; rewrite /pos_esum (_ : [set _ | _ in _] = [set 0]) ?ereal_sup1//.
apply/seteqP; split=> x //= => [[X [finX XI]] <-|->].
by rewrite fsbig1// => i /XI/a0.
by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0.
Qed.

End posesum.
Arguments eq_pos_esum {R T} S f g.

Section posesum_realType.
Variables ( : realType) ( : choiceType).
Implicit Types (S : set T) (f g : T -> \bar R).

Local Notation := (pos_esum P (fun => A)).

Lemma ( : set T) ( : T -> \bar R) :
(I `<=` J)%classic -> (\esum_( in I) a i <= \esum_( in J) a i)%E.

Proof.

move=> IJ; apply: ereal_sup_le => _/= [A [finA AI]] <-.
by exists A => //; split => //; exact: subset_trans IJ.
Qed.

Lemma : 0 <= \esum_( in S) f i.

Proof.

rewrite /pos_esum ereal_sup_ubound//.
by exists set0; [exact: fsets_set0|rewrite fsbig_set0].
Qed.

Lemma : finite_set S -> (forall , S i -> 0 <= f i) ->
\esum_( in S) f i = \sum_( \in S) f i.

Proof.

move=> finS f0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
by apply: ereal_sup_ubound; exists S => //; exact: fsets_self.
apply: ge_ereal_sup => /= ? -[F' [finF' F'F] <-].
apply/lee_fsum_nneg_subset => //; first exact/subsetP.
by move=> t; rewrite inE/= => /andP[_] /set_mem/f0.
Qed.

Lemma : 0 <= f t -> \esum_( in [set t]) f i = f t.

Proof.

by move=> ?; rewrite pos_esum_fset// ?fset_set1// ?fsbig_set1// => t' ->.
Qed.

Lemma ( : choiceType) ( : set T1) ( : T1 -> \bar R) :
(exists2 : set T1, fsets I X & x <= \sum_( \in X) a i) ->
x <= \esum_( in I) a i.

Proof.

by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed.

Lemma : (forall , S i -> f i <= g i) ->
\esum_( in S) f i <= \esum_( 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 ( : \bar R) : 0 <= c -> (forall , S t -> 0 <= f t) ->
\esum_( in S) c * f t = c * \esum_( in S) f t.

Proof.

rewrite le_eqVlt => /predU1P[<- _|c0 f0].
  by rewrite mul0e pos_esum1// => ? _; rewrite mul0e.
apply/eqP; rewrite eq_le; apply/andP; split.
- rewrite ge_ereal_sup//= => _ [X [finX XA]] <-.
  rewrite -ge0_mule_fsumr; first by move=> t /XA /f0.
  by rewrite (lee_wpmul2l (ltW c0))// pos_esum_ge//; exists X.
- case: c c0 => [s s0|_|//].
  + rewrite -lee_pdivlMl// ge_ereal_sup//= => _ [X [finX XI]] <-.
    rewrite lee_pdivlMl// ge0_mule_fsumr//; first by move=> t /XI /f0.
    by rewrite pos_esum_ge//; exists X.
  + have : 0 <= \esum_( in S) f x by apply: pos_esum_ge0 => ? ?; exact: f0.
    rewrite [in X in X -> _]le_eqVlt => /predU1P[<-|suma0].
    * by rewrite mule0 pos_esum_ge0// => ? ?; rewrite mule_ge0.
    * rewrite gt0_mulye//.
      have [y [B fsetsTB yE y0]] := ereal_sup_gt suma0.
      rewrite leye_eq; apply/eqP/eq_infty => r; rewrite pos_esum_ge//.
      exists B => //; rewrite -ge0_mule_fsumr//.
        by move=> i Bi; rewrite f0//; case: fsetsTB => _; exact.
      by rewrite yE gt0_mulye// leey.
Qed.

Lemma ( : choiceType) ( : set T1) ( : T1 -> \bar R) :
(forall , I i -> 0 <= a i) -> (forall , I i -> 0 <= b i) ->
\esum_( in I) (a i + b i) = \esum_( in I) a i + \esum_( in I) b i.

Proof.

move=> ag0 bg0.
apply/eqP; rewrite eq_le; apply/andP; split.
  rewrite ge_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=.
  by rewrite leeD// ereal_sup_ubound//=; exists X.
wlog : a b ag0 bg0 / \esum_( in I) a i \isn't a fin_num => [saoo|]; last first.
  move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye.
  rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: pos_esum.
  rewrite leye_eq; apply/eqP/eq_infty => y; rewrite pos_esum_ge//.
  have : y%:E < \esum_( in I) a i by rewrite aoo// ltry.
  move=> /ereal_sup_gt[_ [X [finX XI]] <-] /ltW yle; exists X => //=.
  rewrite (le_trans yle)// fsbig_split// leeDl// fsume_ge0// => // i.
  by move=> /XI; exact: bg0.
case: (boolP (\esum_( in I) a i \is a fin_num)) => sa; last exact: saoo.
case: (boolP (\esum_( in I) b i \is a fin_num)) => sb; last first.
  by rewrite addeC (eq_pos_esum _ _ _ (fun _ _ => addeC _ _)) saoo.
rewrite -leeBrDr// ge_ereal_sup//= => _ [X [finX XI]] <-.
have saX : \sum_( \in X) a i \is a fin_num.
  apply: contraTT sa => /fin_numPn[] sa.
    suff : \sum_( \in X) a i >= 0 by rewrite sa.
    by rewrite fsume_ge0// => i /XI/ag0.
  apply/fin_numPn; right; apply/eqP; rewrite -leye_eq pos_esum_ge//.
  by exists X; rewrite // sa.
rewrite leeBrDr// addeC -leeBrDr// ge_ereal_sup//= => _ [Y [finY YI]] <-.
rewrite leeBrDr// addeC pos_esum_ge//; exists (X `|` Y).
  by split; [rewrite finite_setU|rewrite subUset].
rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset ?finite_setU//=.
- exact/subsetP/subsetUl.
- by move=> x; rewrite !inE in_setU andb_orr andNb => /andP[_] /[!inE] /YI/ag0.
- exact/subsetP/subsetUr.
- move=> x; rewrite !inE in_setU andb_orr andNb/= orbF.
  by move=> /andP[_] /[!inE] /XI/bg0.
Qed.

Lemma { : choiceType} ( : set T1) ( : T1 -> \bar R) :
\esum_( in I) a i = \esum_( in [set: T1]) if i \in I then a i else 0.

Proof.

apply/eqP; rewrite eq_le !ge_ereal_sup//= => _ [X [finX XI]] <-.
  rewrite ereal_sup_ubound//; exists X => //; apply: eq_fsbigr => x /[!inE] Xx.
  by rewrite ifT// inE; exact: XI.
rewrite -big_mkcond/= big_fset_condE/=; set Y := [fset _ | _ in _ & _]%fset.
rewrite ereal_sup_ubound//=; exists [set` Y].
  by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE.
by rewrite fsbig_finite// set_fsetK.
Qed.

Lemma { : choiceType} ( : set T1) ( : seq T2) ( : pred T2)
    ( : T1 -> T2 -> \bar R) :
  (forall , I i -> P j -> 0 <= a i j) ->
  \esum_( in I) \sum_( <- r | P j) a i j =
  \sum_( <- r | P j) \esum_( in I) a i j.

Proof.

move=> a_ge0; elim: r => [|j r IHr]; rewrite ?(big_nil, big_cons)// -?IHr.
by rewrite pos_esum1// => i; rewrite big_nil.
case: ifPn => Pj; last first.
by apply: eq_pos_esum => i Ii; rewrite big_cons (negPf Pj).
have aj_ge0 i : I i -> a i j >= 0 by move=> ?; apply: a_ge0.
rewrite -pos_esumD//; first by move=> i Ii; apply: sume_ge0 => *; apply: a_ge0.
by apply: eq_pos_esum => i Ii; rewrite big_cons Pj.
Qed.

Lemma { : choiceType} ( : set T1) ( : T1 -> set T2)
    ( : T1 -> T2 -> \bar R) :
  (forall , I i -> J i j -> 0 <= a i j) ->
  \esum_( in I) \esum_( in J i) a i j = \esum_( in I `*`` J) a k.1 k.2.

Proof.

move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split.
  apply: ge_ereal_sup => /= _ [X [finX XI]] <-.
  under eq_fsbigr do rewrite pos_esum_mkcond.
  rewrite fsbig_finite//= big_seq -pos_esum_sum.
    move=> i j _ /[!in_fset_set]// /[!inE] /XI Ij.
    by case: ifPn => // /[!inE] /a_ge0-/(_ Ij).
  under eq_pos_esum do rewrite -big_seq -big_mkcond/=.
  apply: ge_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ubound => /=.
  set XYJ := [set | z \in X `*` Y /\ z.2 \in J z.1].
  have ? : finite_set XYJ.
    apply: sub_finite_set (finite_setX finX finY) => z/=.
    by rewrite /XYJ/= in_setX => -[/andP[] /[!inE]].
  exists XYJ => /=; first by split => //= z; rewrite /XYJ/= 2!inE=> -[[/XI]].
  rewrite [in RHS]fsbig_finite//= (exchange_big_dep xpredT)// pair_big_dep_cond.
  rewrite fsbig_finite//; apply: eq_fbigl => -[/= x y]; rewrite in_fset_set//.
  apply/idP/imfset2P.
    rewrite /XYJ !inE/= !inE/= -andA => -[Xx [Yy Jxy]].
    exists x; first by rewrite !inE in_fset_set// mem_set.
    by exists y => //; rewrite !inE mem_set// in_fset_set// mem_set.
  move=> [t1]; rewrite !inE andbT/= in_fset_set// inE => Xt1.
  by move=> [t2]; rewrite !inE in_fset_set /XYJ//= =>/andP[/[!inE] ? ?] [-> ->].
apply: ge_ereal_sup => _ /= [X/= [finX XIJ]] <-; apply: pos_esum_ge.
exists X.`1; first by split=> [|x [y /XIJ[]//]]; exact: finite_set_fst.
apply: (@le_trans _ _
    (\sum_( <- fset_set X.`1) \sum_( <- fset_set X.`2 | j \in J i) a i j)).
  rewrite pair_big_dep_cond//=; set Y := Imfset.imfset2 _ _ _ _.
  rewrite [leRHS](big_fsetID _ (mem X))/=.
  rewrite (_ : [fset x | in Y & x \in X] = Y `&` fset_set X)%fset.
    by apply/fsetP => x; rewrite 2!inE/= in_fset_set.
  rewrite (fsetIidPr _); last first.
    rewrite fsbig_finite// leeDl// big_seq sume_ge0//=.
    move=> [x y] /imfsetP[[x1 y1]] /[!inE] /andP[] /imfset2P[x2]/= /[!inE].
    rewrite andbT in_fset_set; first exact: finite_set_fst.
    move=> /[!inE] x2X [y2] /[!inE] /andP[] /[!in_fset_set].
      exact: finite_set_snd.
    move=> /[!inE] y2X y2J [-> ->] _ [-> ->]; rewrite a_ge0//.
    by move: x2X => [y3 /XIJ []].
  apply/fsubsetP => -[i j]; rewrite in_fset_set// inE => Xij; apply/imfset2P.
  exists i => /=.
    rewrite !inE/= in_fset_set//; first exact: finite_set_fst.
    by rewrite andbT mem_set//; move/fst_set_fst : Xij.
  exists j => //; rewrite !inE/= in_fset_set; first exact: finite_set_snd.
  rewrite mem_set/=; first by move/snd_set_snd : Xij.
  by rewrite mem_set//; move/XIJ : Xij => [].
rewrite -fsbig_finite; first exact: finite_set_fst.
apply lee_fsum=> [|i Xi]; first exact: finite_set_fst.
rewrite ereal_sup_ubound //=; have ? : finite_set (X.`2 `&` J i).
  by apply: finite_setI; left; exact: finite_set_snd.
exists (X.`2 `&` J i) => //.
rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply/eq_fbigl => j.
by rewrite in_fset_set// !inE/= in_setI in_fset_set//; exact: finite_set_snd.
Qed.

Lemma ( : choiceType) ( : set T1) ( : set T2)
( : T1 -> T2) ( : T2 -> \bar R) : set_bij P Q e ->
\esum_( in Q) a j = \esum_( in P) a (e i).

Proof.

elim/choicePpointed: T1 => T1 in e P *.
  rewrite !emptyE => /Pbij[{}e ->].
  by rewrite -[in LHS](image_eq e) image_set0 !pos_esum_set0.
elim/choicePpointed: T2 => T2 in a e Q *; first by have := no (e point).
move=> /(@pPbij _ _ _)[{}e ->].
gen have le_esum : T1 T2 a P Q e /
    \esum_( in Q) a j <= \esum_( in P) a (e i); last first.
  apply/eqP; rewrite eq_le le_esum//=.
  rewrite [leRHS](_ : _ = \esum_( in Q) a (e (e^-1%FUN j))).
    by apply: eq_pos_esum => i Qi; rewrite invK.
  by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS.
rewrite ge_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ubound => //=.
exists [set` (e^-1 @` (fset_set X))%fset].
  split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset.
  by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS.
rewrite fsbig_finite//= set_fsetK big_imfset => //=.
  move=> x y; rewrite !in_fset_set// !inE => /XQ ? /XQ ? /(congr1 e).
  by rewrite !invK ?inE.
by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE.
Qed.

End posesum_realType.
Arguments reindex_pos_esum {R T1 T2} P Q e a.

End PosEsum.

Section esum.
Variables ( : realFieldType) ( : choiceType).
Implicit Types (S : set T) (f g : T -> \bar R).

Definition := PosEsum.pos_esum S f^\+ - PosEsum.pos_esum S f^\-.

Local Notation := (esum P (fun => A)).

Lemma : (forall , S i -> f i = g i) ->
\esum_( in S) f i = \esum_( 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 : (forall , S x -> 0 <= f x) ->
\esum_( in S) f i = ereal_sup [set \sum_( \in B) f x | in fsets S].

Proof.

move=> ?.
rewrite /esum PosEsum.ge0_pos_esum_funepos// PosEsum.ge0_pos_esum_funeneg//.
by rewrite sube0.
Qed.

Lemma : \esum_( in set0) f i = 0.

Proof.

by rewrite /esum !PosEsum.pos_esum_set0 subee. Qed.

Lemma : (forall , S x -> 0 <= f x) ->
\esum_( in S) - f x = - \esum_( in S) f i.

Proof.

move=> f0.
rewrite [in RHS]ge0_esum// [LHS]/esum [X in X - _ = _]PosEsum.pos_esum1 ?add0r.
by move=> t /mem_set At; rewrite funeposN (@ge0_funenegE _ _ S).
rewrite /PosEsum.pos_esum; congr (- ereal_sup _).
apply: eq_imagel => B SB; apply: eq_fsbigr => x xB.
rewrite funenegN (@ge0_funeposE _ _ B)// => y By; apply: f0.
by case: SB => _; exact.
Qed.

End esum.
Arguments eq_esum {R T} S f g.

Notation := (esum P (fun => F)) : ring_scope.

Section esum_realType.
Variables ( : realType) ( : choiceType).
Implicit Types (S : set T) (f : T -> \bar R).

Lemma : (forall , S x -> 0 <= f x) ->
(forall , S x -> f x <= g x) ->
\esum_( in S) f x <= \esum_( in S) g x.

Proof.

move=> f0 leS; have g0 x : S x -> 0 <= g x.
by move=> /[dup] Ax /leS; apply: le_trans; exact: f0 Ax.
by rewrite !ge0_esum// PosEsum.le_pos_esum.
Qed.

Lemma : (forall , S x -> 0 <= f x) -> 0 <= \esum_( in S) f i.

Proof.

by move=> f0; rewrite ge0_esum// PosEsum.pos_esum_ge0. Qed.

Lemma : finite_set S -> (forall , S i -> 0 <= f i) ->
\esum_( in S) f i = \sum_( \in S) f i.

Proof.

by move=> finF f0; rewrite ge0_esum//; exact: PosEsum.pos_esum_fset. Qed.

End esum_realType.

Lemma { : realFieldType} { : choiceType} ( : set I) ( : I -> \bar R) :
(forall , D i -> f i = 0) -> \esum_( in D) f i = 0.

Proof.

move=> Df0; rewrite ge0_esum; last exact: PosEsum.pos_esum1.
by move=> i /Df0 ->.
Qed.

Section esum_cond.
Context { : realType} { : choiceType}.
Implicit Types (A B : set T) (f : T -> \bar R).

Lemma :
\esum_( in A) f i = \esum_( in [set: T]) if i \in A then f i else 0.

Proof.

rewrite /esum; congr (_ - _); rewrite PosEsum.pos_esum_mkcond;
congr PosEsum.pos_esum; apply/funext => x/=.
- by rewrite funepos_restrict.
- by rewrite funeneg_restrict.
Qed.

Lemma :
\esum_( in A `&` B) f i = \esum_( in A) if i \in B then f i else 0.

Proof.

rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
by rewrite in_setI; case: (i \in A) (i \in B) => [] [].
Qed.

Lemma :
\esum_( in A `&` B) f i = \esum_( in B) if i \in A then f i else 0.

Proof.

rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
by rewrite in_setI; case: (i \in A) (i \in B) => [] [].
Qed.

Lemma :
\esum_( in [set: T]) (if x == y then f y else 0) = \esum_( in [set x]) f i.

Proof.

rewrite [RHS]esum_mkcond.
by under [in RHS]eq_esum do rewrite in_set1 eq_sym.
Qed.

End esum_cond.

Section esum_set1.
Context { : realType} { : choiceType}.
Implicit Types (f : T -> \bar R).

Let : 0 <= f t -> \esum_( in [set t]) f i = f t.

Proof.

move=> ?; rewrite ge0_esum; first by move=> x ->.
exact: PosEsum.pos_esum_set1.
Qed.

Lemma : \esum_( in [set x]) f i = f x.

Proof.

rewrite /esum.
rewrite (PosEsum.eq_pos_esum _ _ (fun => if x == y then f^\+ y else 0)).
  by move=> i /[!inE] ->; rewrite eqxx.
rewrite [X in _ - X](PosEsum.eq_pos_esum _ _
    (fun => if x == y then f^\- y else 0)).
  by move=> i /[!inE] ->; rewrite eqxx.
rewrite -[X in X - _]ge0_esum; first by move=> t _; case: ifPn.
rewrite -[X in _ - X]ge0_esum; first by move=> t _; case: ifPn.
have [Sx0|Sx0] := comparable_ltP (comparableT (f x) 0)%E.
- rewrite esum1; first by move => t //= ->; rewrite eqxx funeposE// max_r// ltW.
  rewrite ge0_esum_set1 eqxx ?funeneg_ge0//.
  by rewrite funenegE max_l// ?oppeK ?add0e// leeNr oppe0 ltW.
- rewrite ge0_esum_set1 eqxx ?funepos_ge0//.
  rewrite esum1; first by move => t ->; rewrite funenegE eqxx max_r// oppe_le0.
  by rewrite funeposE max_l// sube0.
Qed.

End esum_set1.

Lemma { : realType} { : choiceType} ( : set T) ( : T -> \bar R) :
  (forall , I i -> 0 <= f i) ->
  (exists2 : set T, fsets I X & x <= \sum_( \in X) f i) ->
  x <= \esum_( in I) f i.

Proof.

by move=> f0 If; rewrite ge0_esum// PosEsum.pos_esum_ge. Qed.

Lemma { : realType} { : choiceType} ( : set T) ( : T -> \bar R) :
(forall , A i -> 0 <= f i) ->
\esum_( in A) f x = 0 -> forall , A x -> f x = 0.

Proof.

move=> f0; rewrite ge0_esum// => suma0 x Ax.
apply/eqP; rewrite eq_le f0//= -suma0 ereal_sup_ubound//=.
exists [set x]; first by split => // t ->.
by rewrite -esum_set1 esum_fset// => i ->; exact: f0.
Qed.

Section esumZ.
Context { : realType} { : choiceType} ( : set T) ( : T -> \bar R).

Let : 0 <= c -> (forall , A t -> 0 <= f t) ->
\esum_( in A) c * f t = c * \esum_( in A) f t.

Proof.

rewrite le_eqVlt => /predU1P[<- _|c0 f0].
by rewrite mul0e esum1// => ? _; rewrite mul0e.
rewrite [in LHS]ge0_esum; first by move=> x /f0 ax0; rewrite ?mule_ge0// ltW.
by rewrite ge0_esum//; apply: PosEsum.pos_esumZ => //; exact: ltW.
Qed.

Lemma : (forall , A x -> 0 <= f x) ->
\esum_( in A) c * f x = c * \esum_( in A) f x.

Proof.

move=> h; rewrite (eq_esum _ _ (fun => esg c * (`|c| * f x))).
  by move=> x; rewrite muleA -numEesg.
transitivity (esg c * \esum_( in A) `|c| * f x).
  have [hc|hc|->] := comparable_ltgtP (comparableT c 0).
  - rewrite {1}lte0_abs// gte0_esg// (eq_esum _ _ (fun => - (- c * f x))).
      by move => ?; rewrite mulN1e.
    rewrite mulN1e -esumN; last by rewrite lte0_abs.
    by move=> ? ?; rewrite mule_ge0//; exact: h.
  - rewrite gte0_abs// lte0_esg// mul1e (eq_esum _ _ (fun => c * f x))//.
    by move=> ?; rewrite mul1e.
  - under eq_esum do rewrite esg0 mul0e.
    by rewrite esg0 mul0e esum1.
by rewrite (eq_esum _ _ (fun => `|c| * f x))// ge0_esumZ// muleA -numEesg.
Qed.

End esumZ.

Lemma { : realType} { : choiceType} ( : set T) ( : T -> \bar R) :
(forall , I i -> 0 <= f i) -> (forall , I i -> 0 <= g i) ->
\esum_( in I) (f i + g i) = \esum_( in I) f i + \esum_( in I) g i.

Proof.

move=> f0 g0; rewrite [in LHS]ge0_esum//.
by move=> *; rewrite adde_ge0 ?f0 ?g0.
by do 2 rewrite ge0_esum//; exact: PosEsum.pos_esumD.
Qed.

Lemma { : realType} { : choiceType} ( : set T) ( : T -> \bar R) :
  (forall , A i -> f i >= 0) ->
  \esum_( in A) f i = (\esum_( in A `&` B) f i) +
                       (\esum_( in A `&` ~` B) f i).

Proof.

move=> f0; rewrite !esum_mkcondr -esumD; do ?by move=> i /f0; case: ifP.
by apply: eq_esum=> i; rewrite in_setC; case: ifP; rewrite /= (adde0, add0e).
Qed.

Arguments esumID {R T}.

Lemma [ : realType] [ : choiceType]
    ( : set T1) ( : seq T2) ( : pred T2) ( : T1 -> T2 -> \bar R) :
  (forall , I i -> P j -> 0 <= f i j) ->
  \esum_( in I) \sum_( <- r | P j) f i j =
  \sum_( <- r | P j) \esum_( in I) f i j.

Proof.

move=> f0; rewrite ge0_esum; first by move=> *; apply: sume_ge0 => t /f0; exact.
rewrite [LHS]PosEsum.pos_esum_sum//; apply: eq_bigr => t Pt.
by rewrite ge0_esum// => x /f0; exact.
Qed.

#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `exchange_esum_sum`")]
Notation := exchange_esum_sum (only parsing).

Lemma [ : realType] [ : choiceType]
    ( : set T1) ( : T1 -> set T2) ( : T1 -> T2 -> \bar R) :
  (forall , I i -> J i j -> 0 <= f i j) ->
  \esum_( in I) \esum_( in J i) f i j = \esum_( in I `*`` J) f k.1 k.2.

Proof.

move=> f0; rewrite [RHS]ge0_esum/=; first by move=> [x y]/= [Ix Jxy]; exact: f0.
rewrite -[RHS]PosEsum.pos_esum_esum// ge0_esum.
by move=> x Ix; rewrite esum_ge0// => t /f0; exact.
apply: PosEsum.eq_pos_esum => x Ix.
by rewrite ge0_esum// => t /f0; apply; exact/set_mem.
Qed.

Lemma ( : realDomainType)
( : (\bar R)^nat) ( : {fset nat}) ( : pred nat) :
(forall , P i -> 0%E <= f i) -> [set` F] `<=` `I_n ->
\sum_( <- F | P i) f i <= \sum_(0 <= < n | P i) f i.

Proof.

move=> f0 Fn; rewrite [leRHS](bigID (mem F))/=.
suff -> : \sum_(0 <= < n | P i && (i \in F)) f i = \sum_( <- F | P i) f i.
by rewrite leeDl ?sume_ge0// => i /andP[/f0].
rewrite -big_filter -[RHS]big_filter; apply: perm_big.
rewrite uniq_perm ?filter_uniq ?index_iota ?iota_uniq ?fset_uniq//.
move=> i; rewrite ?mem_filter.
case: (boolP (P i)) => //= Pi; case: (boolP (i \in F)) => //= Fi.
by rewrite mem_iota leq0n add0n subn0/=; apply: Fn.
Qed.

Arguments lee_sum_fset_nat {R f} F n P.

Lemma ( : realType) ( : (\bar R)^nat) ( : {fset nat})
( : pred nat) : (forall , P i -> 0%E <= f i) ->
\sum_( <- F | P i) f i <= \sum_( <oo | P i) f i.

Proof.

move=> f0; pose n := (\max_( <- F) k).+1.
rewrite (le_trans (lee_sum_fset_nat F n _ _ _))//; last first.
by apply: nneseries_lim_ge => i _; exact: f0.
move=> k /= kF; rewrite /n big_seq_fsetE/=.
by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax.
Qed.

Arguments lee_sum_fset_lim {R f} F P.

Lemma ( : realType) ( : nat -> \bar R) ( : pred nat) :
(forall , P n -> 0 <= a n) ->
\sum_( <oo | P i) a i = \esum_( in [set | P x]) a i.

Proof.

move=> a0; rewrite ge0_esum//.
apply/eqP; rewrite eq_le; apply/andP; split.
- apply: (lime_le (is_cvg_nneseries_cond (fun _ => a0 n))); apply: nearW => n.
  apply: ereal_sup_ubound; exists [set` [fset val i | in 'I_n & P i]%fset].
    split; first exact: finite_fset.
    by move=> /= k /imfsetP[/= i]; rewrite inE => + ->.
  rewrite fsbig_finite//= set_fsetK big_imfset/=.
    by move=> ? ? ? ? /val_inj.
  by rewrite big_filter big_enum_cond/= big_mkord.
- apply: ge_ereal_sup => _ [/= F [finF PF] <-].
  rewrite fsbig_finite//= -(big_rmcond_in P)/=; last exact: lee_sum_fset_lim.
  by move=> k; rewrite in_fset_set// inE => /PF ->.
Qed.

Lemma { : realType} ( : nat -> \bar R) :
(forall , 0 <= a n) -> \sum_( <oo) a i = \esum_( in [set: nat]) a i.

Proof.

by move=> a0; rewrite nneseries_esum// set_true. Qed.

Lemma { : realType} { : choiceType} ( : set T) ( : set T')
( : T -> T') ( : T' -> \bar R) : set_bij P Q e ->
\esum_( in Q) a j = \esum_( in P) a (e i).

Proof.

move=> PQe; rewrite /esum; congr (_ - _).
- rewrite (PosEsum.reindex_pos_esum P Q e)//; congr PosEsum.pos_esum.
by apply/funext => i; rewrite !funeposE.
- rewrite (PosEsum.reindex_pos_esum P Q e)//; congr PosEsum.pos_esum.
by apply/funext => i; rewrite !funenegE.
Qed.

Arguments reindex_esum {R T T'} P Q e a.

Lemma [ : realType] [ : choiceType]
( : T -> U -> \bar R): (forall , 0 <= f i j) ->
\esum_( in A) \esum_( in B) f x y = \esum_( in B) \esum_( in A) f x y.

Proof.

move=> f0; rewrite !esum_esum//=.
rewrite (reindex_esum (fun => A z.1 /\ B z.2) (fun => 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.

Let ( : realType) ( : nat -> nat -> \bar R)
  ( : pred nat) : (forall , 0 <= a i j) ->
  \sum_( <oo | P i) \sum_( <oo | Q j) a i j =
  \esum_( in P `*` Q) a i.1 i.2.

Proof.

move=> a0; rewrite -(@esum_esum _ _ _ P (fun=> Q))//.
rewrite nneseries_esum//; first by move=> n _; exact: nneseries_ge0.
rewrite (_ : [set | P x] = P); first by apply/seteqP; split.
by apply eq_esum => i Pi; rewrite nneseries_esum.
Qed.

Lemma ( : realType) ( : nat -> nat -> \bar R)
  ( : pred nat) : (forall , 0 <= a i j) ->
  \sum_( <oo | P i) \sum_( <oo | Q j) a i j =
  \sum_( <oo | Q j) \sum_( <oo | P i) a i j.

Proof.

move=> a0; rewrite !nneseries_esum_prod//.
rewrite (reindex_esum (Q `*` P) _ (fun => (x.2, x.1)))//; split=> //=.
by move=> [i j] [/=].
by move=> [i1 i2] [j1 j2] /= _ _ [] -> ->.
by move=> [i1 i2] [Pi1 Qi2] /=; exists (i2, i1).
Qed.

End nneseries_interchange.

Lemma ( : realType) ( : choiceType)
    ( : set T) ( : T -> T') ( : T' -> \bar R) :
    set_inj P e ->
  \esum_( in e @` P) a j = \esum_( in P) a (e i).

Proof.

by move=> /inj_bij; apply: reindex_esum. Qed.

Arguments esum_image {R T T'} P e a.

Lemma ( : realType) ( : choiceType) ( : T -> \bar R)
    ( : nat -> T) ( : pred nat) :
    (forall , P n -> 0 <= a (e n)) ->
    set_inj P e ->
  \esum_( in e @` P) a i = \sum_( <oo | P i) a (e i).

Proof.

by move=> a0 einj; rewrite esum_image// nneseries_esum. Qed.

Arguments esum_pred_image {R T} a e P.

Lemma [ : realType] [ : choiceType] [ : T -> \bar R]
    [ : nat -> T] [ : set nat] :
    (forall : nat, P n -> 0 <= a (e n)) ->
  set_inj P e ->
  \esum_( in [set e x | in P]) a i = \sum_( <oo | i \in P) a (e i).

Proof.

move=> a0 einj; rewrite esum_image// nneseries_esum ?set_mem_set//.
by move=> n; rewrite inE => /a0.
Qed.

Arguments esum_set_image {R T} a e P.

Section esum_bigcup.
Variables ( : realType) ( : choiceType) ( : set nat).
Implicit Types (J : nat -> set T) (a : T -> \bar R).

Lemma : trivIset setT J -> (forall , 0 <= a x) ->
\esum_( in \bigcup_( in K) (J k)) a i =
\esum_( in K) \esum_( in J i) a j.

Proof.

move=> tJ a0; rewrite esum_esum//; apply: reindex_esum => //; split.
- by move=> [/= i j] [Ki Jij]; exists i.
- move=> [/= i1 j1] [/= i2 j2]; rewrite ?inE/=.
move=> [K1 J1] [K2 J2] j12; congr (_, _) => //.
by apply: (@tJ i1 i2) => //; exists j1; split=> //; rewrite j12.
- by move=> j [i Ki Jij]/=; exists (i, j).
Qed.

Lemma : trivIset [set | a @` J i != [set 0]] J ->
(forall : T, (\bigcup_( in K) J k) x -> 0 <= a x) ->
\esum_( in \bigcup_( in K) J k) a i = \esum_( in K) \esum_( in J k) a j.

Proof.

move=> Jtriv a_ge0.
pose J' := if a @` J i == [set 0] then set0 else J i.
pose a' := if x \in \bigcup_( in K) J k then a x else 0.
have a'E k x : K k -> J k x -> a' x = a x.
  move=> Kk Jkx; rewrite /a'; case: ifPn; rewrite ?(inE, notin_setE)//=.
  by case; exists k.
have a'_ge0 x : a' x >= 0 by rewrite /a'; case: ifPn; rewrite // ?inE => /a_ge0.
transitivity (\esum_( in \bigcup_( in K) J' k) a' i).
  rewrite esum_mkcond [RHS]esum_mkcond /a'; apply: eq_esum => x _.
  do 2!case: ifPn; rewrite ?(inE, notin_setE)//= => J'x Jx.
  apply: contra_not_eq J'x => Nax.
  move: Jx => [k kK Jkx]; exists k=> //; rewrite /J'/=; case: ifPn=> //=.
  move=> /eqP/(congr1 (@^~ (a x)))/=; rewrite propeqE => -[+ _].
  by apply: contra_neq_not Nax; apply; exists x.
rewrite esum_bigcupT//.
  move=> i j _ _ [x []]; rewrite /J'/=.
  case: eqVneq => //= Ai0 Jix; case: eqVneq => //= Aj0 Jjx.
  by have := Jtriv i j Ai0 Aj0; apply; exists x.
apply: eq_esum => i Ki.
rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum => x _.
do 2!case: ifPn; rewrite ?(inE, notin_setE)//=.
- by move=> /a'E->//.
- by rewrite /J'; case: ifPn => //.
move=> Jix; rewrite /J'; case: ifPn=> //=.
by move=> /eqP/(congr1 (@^~ (a x)))/=; rewrite propeqE => -[->]//; exists x.
Qed.

End esum_bigcup.

Arguments esum_bigcupT {R T K} J a.
Arguments esum_bigcup {R T K} J a.

Lemma { : realType} ( : choiceType) ( : (set T)^nat)
( : T -> \bar R) : trivIset [set: nat] F -> (forall , 0 <= f i)%E ->
(\esum_( in \bigcup_ F n) f i = \sum_(0 <= <oo) (\esum_( in F i) f j))%E.

Proof.

move=> tF f0; rewrite esum_bigcupT// nneseries_esum//.
by move=> k _; exact: esum_ge0.
by rewrite fun_true; apply: eq_esum => /= i _.
Qed.

Definition ( : choiceType) ( : realType) ( : set T)
( : T -> \bar R) := (\esum_( in D) `| f x | < +oo)%E.

Section summable_lemmas.
Local Open Scope ereal_scope.
Variables ( : choiceType) ( : realType).
Implicit Types (D : set T) (f : T -> \bar R).

Lemma : summable D f -> forall , 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 : summable D f = (\esum_( in D) `| f x | \is a fin_num).

Proof.

rewrite /summable fin_numElt; apply/idP/idP => [->|/andP[]//].
by rewrite andbT (lt_le_trans (ltNyr 0))//; exact: esum_ge0.
Qed.

Lemma : summable D f -> summable D g -> summable D (f \+ g).

Proof.

move=> Df Dg; apply: le_lt_trans (lte_add_pinfty Df Dg).
rewrite -esumD//; do 2 rewrite ge0_esum//.
by move=> x Dx; rewrite adde_ge0.
by apply: PosEsum.le_pos_esum => t Dt; exact: lee_abs_add.
Qed.

Lemma : summable D f = summable D (\- f).

Proof.

by rewrite /summable; congr (_ < +oo); apply: eq_esum => t Dt; rewrite abseN.
Qed.

Lemma : summable D f -> summable D g -> summable D (f \- g).

Proof.

by move=> Df; rewrite summableN; exact: summableD. Qed.

Lemma : summable D f -> summable D f^\+.

Proof.

apply: le_lt_trans.
do 2 rewrite ge0_esum//.
apply: PosEsum.le_pos_esum => t Dt.
by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl.
Qed.

Lemma : summable D f -> summable D f^\-.

Proof.

apply: le_lt_trans.
do 2 rewrite ge0_esum//.
apply: PosEsum.le_pos_esum => t Dt.
by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
Qed.

End summable_lemmas.

Import numFieldNormedType.Exports.

Section summable_nat.
Local Open Scope ereal_scope.
Variable : realType.

Lemma ( : pred nat) ( : (\bar R)^nat) : summable P f ->
(\sum_(0 <= < r | P k) fine (f k))%R = fine (\sum_(0 <= < 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).
Qed.

Lemma ( : pred nat) ( : (\bar R)^nat) :
(forall , P i -> 0 <= f i)%E -> summable P f ->
cvg ((fun => \sum_(0 <= < 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_( <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 fineK//.
  rewrite nneseries_esum// fin_numElt; apply/andP; split.
    by rewrite (@lt_le_trans _ _ 0)// ?lte_ninfty//; exact: esum_ge0.
  apply: le_lt_trans Pf => /=.
  by rewrite ge0_esum.
apply: le_trans (nneseries_lim_ge n _) => //; apply: lee_sum => i _.
by rewrite lee_abs.
Qed.

Lemma ( : pred nat) ( : (\bar R)^nat) :
    (forall , P i -> 0 <= f i)%E -> summable P f ->
  \sum_( <oo | P i) f i =
  (lim ((fun => (\sum_(0 <= < n | P k) fine (f k))%R) @ \oo))%:E.

Proof.

move=> f0 Pf; pose A_ := (\sum_(0 <= < 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.
Qed.

Lemma ( : (\bar R)^nat) ( : pred nat) : summable P f ->
\sum_( <oo | P i) (f i) =
\sum_( <oo | P i) f^\+ i - \sum_( <oo | P i) f^\- i.

Proof.

move=> Pf.
pose A_ := (\sum_(0 <= < n | P k) fine (f^\+ k))%R.
pose B_ := (\sum_(0 <= < n | P k) fine (f^\- k))%R.
pose C_ := fine (\sum_(0 <= < n | P k) f k).
pose A := lim (A_ @ \oo).
pose B := lim (B_ @ \oo).
suff: ((fun => 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 -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 => 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.
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//.
  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 -[in LHS](funeposBneg f).
by rewrite distrC; apply: hN; near: n; exists N.
Unshelve. all: by end_near. Qed.

Lemma ( : (\bar R)^nat) ( : pred nat) :
summable P f -> \sum_( <oo | P i) f i = esum P f^\+ - esum P f^\-.

Proof.

move=> Pfoo.
by rewrite -nneseries_esum// -nneseries_esum// [LHS]summable_eseries.
Qed.

End summable_nat.

Section esumB.
Local Open Scope ereal_scope.
Variables ( : realType) ( : choiceType).
Implicit Types (D : set T) (f g : T -> \bar R).

Let := esum D f^\+ - esum D f^\-.

Let : (forall , D x -> 0 <= f x) ->
esum_posneg D f = \esum_( in D) f x.

Proof.

move=> Sa; rewrite /esum_posneg [X in _ - X](_ : _ = 0) ?sube0.
by rewrite esum1// => x Sx; rewrite -[LHS]/(f^\- x) (ge0_funenegE Sa)// inE.
apply: eq_esum => t St; rewrite funeposE; apply/max_idPl; exact: Sa.
Qed.

Lemma : summable D f -> summable D g ->
  (forall , D i -> 0 <= f i) -> (forall , D i -> 0 <= g i) ->
  \esum_( in D) (f \- g)^\+ i - \esum_( in D) (f \- g)^\- i =
  \esum_( in D) f i - \esum_( in D) g i.

Proof.

move=> Df Dg f0 g0.
have /eqP : esum D (f \- g)^\+ + esum_posneg D g =
            esum D (f \- g)^\- + esum_posneg D f.
  rewrite !ge0_esum_posneg// -!esumD//.
  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).
  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 [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 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.
  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.
  by rewrite /= gee0_abs// f0.
- rewrite fin_num_adde_defl// ge0_esum_posneg//.
  rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di.
  by rewrite /= gee0_abs// g0.
by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
Qed.

End esumB.

Section exchange_esum_ereal_sup.
Context { : realType} { : choiceType} { : T -> nat -> \bar R}.
Hypothesis : forall , 0 <= f t n.
Hypothesis : forall , nondecreasing_seq (f x).

Lemma ( : set T) :
\esum_( in A) ereal_sup (range (f i)) =
ereal_sup (range (fun => \esum_( in A) f x n)).

Proof.

rewrite ge0_esum.
  by move=> x Ax; apply: le_ereal_sup_tmp; exists (f x 0).
under eq_imagel.
  move=> B [fin BA]; rewrite fsbig_finite//= ereal_sup_sum//.
  over.
rewrite exchange_ereal_sup; congr ereal_sup; apply: eq_imagel => n _.
rewrite ge0_esum//; congr ereal_sup.
by apply: eq_imagel => B [finB BA]; rewrite fsbig_finite.
Qed.

End exchange_esum_ereal_sup.

Files

Module mathcomp.analysis.esum