Module mathcomp.analysis.esum

From mathcomp Require Import boot order ssralg ssrnum interval_inference
archimedean finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals topology ereal 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. esummable D f := \esum_(x in D) `| f x | < +oo ```

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

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.
Context { : 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.
Context { : 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.
Context { : 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 -> (\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 : S x -> f x <= \esum_( 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 { : choiceType} ( : set U) ( : U -> \bar R) :
(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 { : choiceType} ( : set U) ( : set T)
    ( : T -> U -> \bar R) :
  (\esum_( in A) (fine (\esum_( in B) h x i))%:E <=
  \esum_( in A) (\esum_( in B) h x i))%E.

Proof.

rewrite le_pos_esum // => u Au.
have := pos_esum_ge0 B (h ^~ u).
by case: (\esum_( in B) _).
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.
Context { : realFieldType} { : choiceType}.
Implicit Types (A : set T) (f g : T -> \bar R).

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

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

Lemma : (forall , A x -> 0 <= f x) ->
\esum_( in A) f i = ereal_sup [set \sum_( \in B) f x | in fsets A].

Proof.

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

Lemma :
\esum_( in A) f x = \esum_( in A) f^\+ x - \esum_( in A) f^\- x.

Proof.

rewrite [in RHS]ge0_esum; first by move=> x _; exact: funepos_ge0.
by rewrite [in RHS]ge0_esum.
Qed.

Lemma : (forall , A i -> f i = g i) ->
\esum_( in A) f i = \esum_( 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_( in set0) f i = 0.

Proof.

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

Lemma : (forall , A x -> 0 <= f x) ->
\esum_( in A) - f x = - \esum_( 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 _ _ A).
rewrite /PosEsum.pos_esum; congr (- ereal_sup _).
apply: eq_imagel => B AB; apply: eq_fsbigr => x xB.
rewrite funenegN (@ge0_funeposE _ _ B)// => y By; apply: f0.
by case: AB => _; exact.
Qed.

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

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

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

Lemma ( : T -> R) : uniq s ->
(forall , 0 <= h x)%R ->
(\sum_( <- s) h j)%:E <= \esum_( 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 : (forall , D x -> f x <= g x) ->
\esum_( in D) f i <= \esum_( in D) g i.

Proof.

move=> leD.
have {}leD : {in D, forall , 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 : (forall , D x -> 0 <= f x) -> 0 <= \esum_( in D) f i.

Proof.

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

Lemma { : choiceType} ( : set U) ( : set T)
    ( : T -> U -> \bar R) : (forall , 0 <= f x y) ->
  \esum_( in A) (fine (\esum_( in B) f x i))%:E <=
     \esum_( in A) (\esum_( 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 ( : set T) : (forall , J x -> 0 <= f x) ->
I `<=` J -> \esum_( in I) f i <= \esum_( in J) f i.

Proof.

move=> f0 IJ.
have I0f : forall , I x -> 0 <= f x by move => x /IJ /f0.
by rewrite !ge0_esum// PosEsum.subset_pos_esum.
Qed.

Lemma : finite_set D -> (forall , D i -> 0 <= f i) ->
\esum_( in D) f i = \sum_( \in D) 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.

Lemma { : realFieldType} { : choiceType} ( : set I) :
\esum_( in D) @cst _ (\bar R) 0 i = 0.

Proof.

by rewrite esum1. 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} ( : T -> \bar R) :
\esum_( in [set: T]) (if x == i then f i else 0) = f x.

Proof.

by rewrite esum_if_eq_op esum_set1. 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.

Lemma { : realType} { : choiceType} ( : set T) ( : T -> \bar R) :
\esum_( in I) a i != 0 -> exists2 , 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.

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

Proof.

by move=> f0 x Ix; rewrite ge0_esum//; exact: PosEsum.pos_esum_ge1. Qed.

Lemma { : realType} { : choiceType} ( : set T) : A !=set0 ->
\esum_(_ in A) +oo%E = +oo%E :> \bar R.

Proof.

move=> [x Ax]; apply/eqP; rewrite eq_le leey/=.
by apply: esum_ge1 Ax => i _; exact: leey.
Qed.

Lemma { : realType} { : choiceType} ( : \bar R) ( : set T)
    ( : T -> \bar R) :
  (0 < c)%E -> (forall , A x -> c <= f x)%E -> infinite_set A ->
  \esum_( in A) f x = +oo%E.

Proof.

move=> c0 cf infA; apply/eqyP => r r0.
have [cy|] := eqVneq c +oo%E.
  rewrite (@le_trans _ _ (\esum_(_ in A) +oo))//; last first.
    by apply: le_esum => x Ax; rewrite -cy cf.
  by rewrite nonempty_esumy ?leey//; exact: infinite_setN0.
move: c c0 cf => [c| |]//; rewrite lte_fin => c0 cf _.
have [B BA Brc] := infinite_set_fset (Num.truncn (r / c)).+1 infA.
apply: esum_ge.
  by move=> i Ai; rewrite (le_trans _ (cf _ Ai))// lee_fin ltW.
exists [set` B]; first by split=> //; apply/subsetP => x; rewrite inE => /BA.
rewrite fsbig_finite//= set_fsetK.
rewrite (@le_trans _ _ (\sum_( <- B) c%:E))//; last first.
  by rewrite !big_seq; apply: lee_sum => x Bx; rewrite cf//; exact: BA.
rewrite sumEFin big_const_seq count_predT.
rewrite iter_addr addr0 -mulr_natr lee_fin -ler_pdivrMl//.
rewrite (@le_trans _ _ (Num.truncn (r / c)).+1%:R) ?ler_nat//.
by rewrite mulrC ltW// truncnS_gt.
Qed.

Arguments infinite_esum_cst {R T} c.

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.
Context { : realType} { : choiceType} ( : set U).
Implicit Types (J : U -> 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 U K} J a.
Arguments esum_bigcup {R T U 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.
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable)]
Notation := esummable (only parsing).

Section esummable_lemmas.
Local Open Scope ereal_scope.
Context { : choiceType} { : realType}.
Implicit Types (D : set T) (f : T -> \bar R).

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

Proof.

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

Lemma : {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 :
(forall , 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 : 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//.
by move=> x Dx; rewrite adde_ge0.
by apply: PosEsum.le_pos_esum => t Dt; exact: lee_abs_add.
Qed.

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

Proof.

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

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

Proof.

by move=> Df; rewrite esummableN; exact: esummableD. Qed.

Lemma : esummable D f -> esummable 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 : esummable D f -> esummable 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.

Lemma : c \is a fin_num ->
esummable D f -> esummable D (fun => 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 : c \is a fin_num ->
esummable D f -> esummable D (fun => f x * c).

Proof.

by under eq_fun do rewrite muleC; exact: esummableZl. Qed.

Lemma :
(exists2 , forall , 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 :
(exists2 , forall , 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 :
esummable D f1 -> esummable D f2 -> esummable D (f1 \* f2).

Proof.

rewrite esummableE => smS1 smS2; apply/esummableMl => //.
by exists (\esum_( in D) `|f1 x|) => //; exact: esum_ge1.
Qed.

End esummable_lemmas.
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_pinfty)]
Notation := esummable_pinfty (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableE)]
Notation := esummableE (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableD)]
Notation := esummableD (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableN)]
Notation := esummableN (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummableB)]
Notation := esummableB (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_funepos)]
Notation := esummable_funepos (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_funeneg)]
Notation := esummable_funeneg (only parsing).

Import numFieldNormedType.Exports.

Section esummable_nat.
Local Open Scope ereal_scope.
Context { : realType}.

Lemma ( : pred nat) ( : (\bar R)^nat) : esummable 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 (esummable_pinfty Pf).
by apply/sum_fin_numP => i ir Pi; rewrite fin_num_abs (esummable_pinfty Pf).
Qed.

Lemma ( : pred nat) ( : (\bar R)^nat) :
(forall , P i -> 0 <= f i)%E -> esummable 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 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.
  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 -> esummable 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 (@esummable_pinfty _ _ P).
by rewrite EFin_lim//; exact: esummable_cvg.
Qed.

Lemma ( : (\bar R)^nat) ( : pred nat) : esummable 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 - _]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)).
  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: 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/= -esummable_fine_sum//.
  apply eq_bigr => i Pi; rewrite -fineB//.
  - 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 ( : (\bar R)^nat) ( : pred nat) :
esummable P f -> \sum_( <oo | P i) f i = esum P f^\+ - esum P f^\-.

Proof.

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

End esummable_nat.
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_fine_sum)]
Notation := esummable_fine_sum (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_cvg)]
Notation := esummable_cvg (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_nneseries_lim)]
Notation := esummable_nneseries_lim (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_eseries)]
Notation := esummable_eseries (only parsing).
#[deprecated(since="mathcomp-analysis 1.18.0", use=esummable_eseries_esum)]
Notation := esummable_eseries_esum (only parsing).

Section esumB.
Local Open Scope ereal_scope.
Context { : 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 : esummable D f -> esummable 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 (esummable_pinfty Dg).
  rewrite add0e max_l; first by rewrite leeNr oppe0 ltW.
  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 -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))// -?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))// -?esummableE// => i Di.
  by rewrite /= gee0_abs// f0.
- rewrite fin_num_adde_defl// ge0_esum_posneg//.
  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 { : realType} { : choiceType}.
Implicit Types (D : set T) (f g : T -> \bar R).

Lemma :
esummable D f -> \esum_( in D) f^\+ t \is a fin_num.

Proof.

move=> /esummable_funepos; rewrite esummableE => ffin.
by rewrite (eq_esum _ _ (fun => `|f^\+ y|))//= => t Dt; rewrite gee0_abs.
Qed.

Lemma :
esummable D f -> \esum_( in D) f^\- t \is a fin_num.

Proof.

rewrite esummableN => /esummable_esum_funepos.
by under eq_esum do rewrite funeposN.
Qed.

Lemma :
esummable D f -> \esum_( 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 D f -> \esum_( in D) - f i = - \esum_( 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 : esummable D f -> 0 <= d -> d \is a fin_num ->
\esum_( in D) d * f x = d * \esum_( 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 : `|c| \is a fin_num -> esummable D f ->
\esum_( in D) c * f x = c * \esum_( 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 D f -> esummable D g ->
\esum_( in D) (f x + g x) = \esum_( in D) f x + \esum_( 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 D f -> esummable D g ->
\esum_( in D) (f x - g x) = \esum_( in D) f x - \esum_( 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 { : 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 => 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.
Qed.

End exchange_esum_ereal_sup.

Files

Module mathcomp.analysis.esum