Module mathcomp.experimental_reals.realsum

From mathcomp Require Import boot order algebra.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp fsbigop classical_sets functions.
From mathcomp Require Import cardinality.
From mathcomp Require Import constructive_ereal reals.
From mathcomp Require Import xfinmap discrete realseq.
From mathcomp Require Import esum ereal numfun.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope fset_scope.
Local Open Scope ring_scope.

Local Notation := (fun => `|f x|) (at level 2).
Local Notation := Monoid.simpm.

Section Summable.
Variables ( : choiceType) ( : realType) ( : T -> R).

Definition := exists ( : R), forall ( : {fset T}),
\sum_( : J) `|f (val x)| <= M.

Lemma : summable ->
{ | 0 <= M & forall ( : {fset T}), \sum_( : J) `|f (val x)| <= M }.

Proof.

move/asboolP/exists_asboolP=> h; have := (xchooseP h).
move: (xchoose _)=> {h} M /asboolP h; exists M => //.
by have := h fset0; rewrite big_pred0 // => -[x]; rewrite in_fset0.
Qed.

End Summable.

Lemma ( : choiceType) ( : realType) ( : T -> R) :
summable f <-> esum.summable [set: T] (EFin \o f).

Proof.

have fsbigsum ( : {fset T}) :
    (\sum_( \in [set` B]) `|f x|%:E)%R = (\sum_( : B) `|f (\val x)|)%:E.
  rewrite (fsbigE B)//=; first by move=> i ->.
  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//.
  apply/ereal_supP => _/= [A [/finite_fsetP[B AB] _] <-].
  by rewrite AB fsbigsum; exact: fM.
rewrite /summable => H.
exists (fine (\esum_( 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.
Qed.

Module .

Definition { : realType} { : choiceType} ( : T -> R) : R :=
  let := [set | exists : {fset T}, x = \sum_( : J) `|f (val x)| ]%classic in
  if `[<summable f>] then sup S else 0.

End PosSum.
#[deprecated(since="1.17.0", note="use `PosSum.psum` instead")]
Notation := PosSum.psum.

Definition { : realType} { : choiceType} ( : T -> R) : R :=
  PosSum.psum f^\+ - PosSum.psum f^\-.

Section SummableCountable.
Variable ( : choiceType) ( : realType) ( : T -> R).

Lemma : summable f -> discrete.countable [pred | f x != 0].

Proof.

case/summableP=> M ge0_M bM; pose E ( : nat) := [pred | `|f x| > p.+1%:~R^-1].
set F := [pred | _]; have le: {subset F <= [pred | `[< exists , x \in E p >]]}.
  move=> x; rewrite !inE => nz_fx; apply/asboolP; exists (Num.truncn `|f x|^-1).
  by rewrite inE invf_plt ?unfold_in/= ?normr_gt0 // -normfV ltr_norm_bound.
apply/(countable_sub le)/cunion_countable=> i /=.
case: (existsTP (fun : seq T => {subset E i <= s}))=> /= [[s le_Eis]|].
  by apply/finite_countable/finiteP; exists s => x /le_Eis.
move=> /finiteNP/(_ ((Num.truncn M).+1 * i.+1)%N)/asboolP/exists_asboolP h.
have/asboolP[] := xchooseP h.
set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset in s].
suff: \sum_( : J) `|f (val x)| > M by rewrite ltNge bM.
apply/(@lt_le_trans _ _ (\sum_( : J) i.+1%:~R^-1)); last first.
  apply/ler_sum=> /= m _; apply/ltW.
  by have:= fsvalP m; rewrite in_fset => /le_sEi.
rewrite sumr_const -cardfE card_fseq undup_id // eq_si.
by rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0// truncnS_gt.
Qed.

End SummableCountable.

Section PosCnv.
Context { : realType}.

Lemma ( : nat -> R) :
(forall , (x <= y)%N -> u x <= u y)
-> exists2 , (-oo < l)%E & ncvg u l.

Proof.

move=> mono_u; pose E := [set | exists , x = u n]%classic.
have nzE: nonempty E by exists (u 0%N); exists 0%N.
case: (pselect (has_sup E)); last first.
  move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=.
  case/(_ M): h=> x [K -> lt_MuK]; exists K=> n le_Kn; rewrite inE.
  by apply/(lt_le_trans lt_MuK)/mono_u.
move=> supE; exists (sup E)%:E => //; first exact: ltNyr.
elim/nbh_finW=>e /= gt0_e.
case: (sup_adherent gt0_e supE)=> x [K ->] lt_uK.
exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.
  by move/ubP: (sup_upper_bound supE); apply; exists n.
rewrite ltrBlDr addrC -ltrBlDr.
by rewrite (lt_le_trans lt_uK) //; apply/mono_u.
Qed.

Lemma ( : nat -> R) :
(forall , (x <= y)%N -> u x <= u y)
-> nbounded u -> exists , ncvg u l%:E.

Proof.

case/ncvg_mono=> -[x||] // _ cu bdu; first by exists x.
case/asboolP/nboundedP: bdu=> M gt0_M bdu.
case/(_ (NPInf M)): cu => K /= /(_ K (leqnn _)).
rewrite inE/= => /ltW /le_trans /(_ (ler_norm _)).
by move/le_lt_trans/(_ (bdu _)); rewrite ltxx.
Qed.

End PosCnv.

Section SumTh.
Context { : realType} ( : choiceType).

Implicit Type S : T -> R.

Lemma ( : T -> R) : summable S -> has_sup
[set | exists : {fset T}, x = \sum_( : J) `|S (val j)|]%classic.

Proof.

case/summableP=> M _ hbd; split.
by exists 0, fset0; rewrite big_fset0.
by exists M; apply/ubP=> y [J ->].
Qed.

Lemma : PosSum.psum S =
sup [set | exists : {fset T}, x = \sum_( : J) `|S (val x)|]%classic.

Proof.

rewrite /PosSum.psum; case: ifPn => // /asboolPn h.
rewrite sup_out //; set X := [set | _]%classic => hs.
apply: h; exists (sup X) => J.
by move/ubP : (sup_upper_bound hs); apply; exists J.
Qed.

Lemma : PosSum.psum S =
sup [set | exists2 : seq T,
uniq J & x = \sum_( <- J) `|S x| ]%classic.

Proof.

rewrite psum_sup; congr sup; rewrite predeqE => x; split.
  case=> J ->; exists (enum_fset J).
    by case: J => /= J /canonical_uniq.
  by rewrite (big_fset_seq \`|_|) /=.
case=> J uqJ ->; exists [fset in J].
by rewrite (big_seq_fset \`|_|).
Qed.

Lemma ( : T -> R) :
(S1 =1 S2) -> summable S1 -> summable S2.

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.
Qed.

Lemma ( : T -> R) :
(S1 =1 S2) -> `[< summable S2 >] = `[< summable S1 >].

Proof.

by move=> eq_12; apply/asboolP/asboolP; apply/eq_summable. Qed.

Lemma ( : {fset T} -> R) : F1 =1 F2 ->
(sup [set | exists , x = F1 J] = sup [set | exists , x = F2 J])%classic.

Proof.

move=> eq_12; congr sup; rewrite predeqE => x.
by split=> -[J ->]; exists J.
Qed.

Lemma ( : T -> R) : F1 =1 F2 -> PosSum.psum F1 = PosSum.psum F2.

Proof.

move=> eq_12; rewrite /PosSum.psum (eq_summableb eq_12).
case: `[< summable F1 >] => //.
congr sup.
rewrite predeqE => x; split=> -[J ->]; exists J;
by apply/eq_bigr=> /= K _; rewrite eq_12.
Qed.

Lemma ( : T -> R) : F1 =1 F2 -> sum F1 = sum F2.

Proof.

move=> eq_fg; rewrite /sum; congr (_ - _); apply/eq_psum.
- exact/eq_funrpos.
- exact/eq_funrneg.
Qed.

Lemma ( : T -> R) :
(forall , 0 <= F1 x <= F2 x) -> summable F2 -> summable F1.

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).
Qed.

Lemma ( : T -> R) :
(forall , 0 <= F1 x <= F2 x) -> summable F2 -> PosSum.psum F1 <= PosSum.psum F2.

Proof.

move=> le_F smF2; have smF1: summable F1 by apply/(le_summable le_F).
rewrite /PosSum.psum (asboolT smF1) (asboolT smF2); apply: sup_le; first last.
+ exact/summable_sup.
+ by exists 0, fset0; rewrite big_fset0.
move=> x [J ->]; apply/downP; exists (\sum_( : J) `|F2 (val j)|).
by exists J.
apply/ler_sum=> /= j _; case/andP: (le_F (val j)) => h1 h2.
by rewrite !ger0_norm // (le_trans h1 h2).
Qed.

Lemma : ~ summable S -> PosSum.psum S = 0.

Proof.

by move/asboolPn/negbTE=> smN; rewrite /PosSum.psum smN. Qed.

Lemma : (forall , 0 <= S x) -> summable S -> PosSum.psum S =
sup [set | exists : {fset T}, x = \sum_( : J) S (val j)]%classic.

Proof.

move=> gt0_S smS; rewrite /PosSum.psum (asboolT smS); apply/eq_ppsum=> /=.
by move=> J; apply/eq_bigr=> j _; rewrite ger0_norm.
Qed.

Lemma : summable S -> PosSum.psum S =
sup [set | exists : {fset T}, x = \sum_( : J) `|S (val j)|]%classic.

Proof.

by move=> smS; rewrite /PosSum.psum (asboolT smS). Qed.

Lemma :
summable S <-> (exists2 , 0 <= M &
forall : seq T, uniq s -> \sum_( <- s) `|S x| <= M).

Proof.

Lemma ( : {fset T}) :
summable S -> \sum_( : J) `|S (val j)| <= PosSum.psum S.

Proof.

move=> smS; rewrite /PosSum.psum (asboolT smS).
by move/ubP : (sup_upper_bound (summable_sup smS)); apply; exists J.
Qed.

Lemma ( : seq T) :
uniq r -> summable S -> \sum_( <- r) `|S j| <= PosSum.psum S.

Proof.

move=> uq_r /gerfin_psum -/(_ [fset in r]);
by rewrite (big_seq_fset \`|S|).
Qed.

Lemma :
(forall , uniq J -> \sum_( <- J) `|S j| <= z) -> PosSum.psum S <= z.

Proof.

move=> le_z; have: summable S; first (apply/summable_seqP; exists z).
+ by apply/(le_trans _ (le_z [::] _)) => //; rewrite big_nil.
+ by move=> J uqJ; apply/le_z.
move/summable_sup=> [neS hsS]; rewrite psum_sup.
apply: ge_sup => //; apply/ubP=> r [J ->].
by rewrite (big_fset_seq \`|_|) le_z /=; case: J => J /= /canonical_uniq.
Qed.

Lemma ( : T -> R) :
summable F -> l < PosSum.psum F ->
exists : {fset T}, l < \sum_( : J) `|F (val j)|.

Proof.

move=> smF; rewrite /PosSum.psum (asboolT smF) => /lt_sup_imfset.
by case=> /= [|J lt_lJ _]; [apply/summable_sup | exists J].
Qed.

End SumTh.

Lemma { : realType} { : choiceType} ( : T -> R) :
(forall , 0 <= f i) -> summable f ->
\esum_( in [set: T]) (f x)%:E = (PosSum.psum f)%:E.

Proof.

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 [A [finA _]].
  rewrite fsumEFin// => <-.
  rewrite lee_fin fsbig_finite//=.
  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 => `|f x|%:E)).
    by move => t _; rewrite ger0_norm.
  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.

Lemma { : realType} ( : set R) :
(E `&` ubound E)%classic x -> sup E = x.

Proof.

case=> /= xE xubE; have nzE: nonempty E by exists x.
apply/eqP; rewrite eq_le ge_sup //=.
have : has_sup E by split; exists x.
by move/sup_upper_bound/ubP; apply.
Qed.

Section FinSumTh.
Context { : realType} ( : finType).

Lemma ( : I -> R) : summable f.

Proof.

Lemma ( : I -> R) : PosSum.psum f = \sum_ `|f i|.

Proof.

(* FIXME *)
pose S := \sum_( : [fset i | : I]) `|f (val i)|.
rewrite /PosSum.psum (asboolT (summable_fin f)) (@max_sup _ S).
  rewrite /=; split; first by exists [fset i | : I]%fset.
  apply/ubP=> y [J ->]; apply/(big_fset_subset (F := \`|_|)).
    by move=> i; rewrite normr_ge0.
  by move=> j jJ; apply/in_imfset.
rewrite /S -(big_map val xpredT \`|f|); apply/perm_big.
rewrite /index_enum -!enumT; apply/(perm_trans _ enum_fsetT).
apply/uniq_perm; rewrite ?map_inj_uniq ?enum_uniq //=.
  by apply/val_inj. by rewrite -enumT enum_uniq.
move=> i /=; rewrite mem_enum in_imfset //; apply/mapP.
have h: i \in [fset j | : I] by rewrite in_imfset.
by exists (FSetSub h) => //; rewrite mem_enum.
Qed.

End FinSumTh.

Section PSumGe.
Context { : realType} ( : choiceType).

Variable ( : T -> R).

Lemma : uniq r -> summable S ->
\sum_( <- r) `|S x| <= PosSum.psum S.

Proof.

move=> uq_r smS; rewrite /PosSum.psum (asboolT smS).
set E := (X in sup X).
have : has_sup E by exact/summable_sup.
move/sup_upper_bound/ubP; apply.
by exists [fset in r]; rewrite (big_seq_fset (fun => `|S i|)).
Qed.

Lemma : summable S -> `|S x| <= PosSum.psum S.

Proof.

move=> smS; have h := @ger_big_psum [:: x] _ smS.
by rewrite (le_trans _ (h _)) ?big_seq1.
Qed.

Lemma : 0 <= PosSum.psum S.

Proof.

(* FIXME: asbool_spec *)
case/boolP: `[< summable S >] => [|/asboolPn/psum_out ->//].
move/asboolP=> smS; have h := @ger_big_psum [::] _ smS.
by rewrite (le_trans _ (h _)) ?big_nil.
Qed.

End PSumGe.

Section PSumNatGe.
Context { : realType}.

Variable ( : nat -> R) ( : summable S).

Lemma : \sum_( < n) `|S i| <= PosSum.psum S.

Proof.

rewrite -(big_mkord predT (fun => `|S i|)) /=.
by apply/ger_big_psum => //; rewrite iota_uniq.
Qed.

End PSumNatGe.

Section PSumCnv.
Context { : realType}.

Variable ( : nat -> R).

Hypothesis : (forall , 0 <= S n).
Hypothesis : summable S.

Lemma : (x <= y)%N -> (\sum_( < x) S i <= \sum_( < y) S i).

Proof.

move=> le_xy; rewrite -!(big_mkord predT) -(subnKC le_xy) /=.
by rewrite /index_iota !subn0 iotaD big_cat /= lerDl sumr_ge0.
Qed.

Lemma : nbounded (fun => \sum_( < n) S i).

Proof.

apply/asboolP/nboundedP; exists (PosSum.psum S + 1).
rewrite ltr_pwDr ?ltr01 1?(le_trans (normr_ge0 (S 0%N))) //.
by apply/ger1_psum.
move=> n; rewrite ltr_pwDr ?ltr01 // ger0_norm ?sumr_ge0 //.
apply/(le_trans _ (ger_big_ord_psum _ n)) => //.
by apply/ler_sum=> /= i _; apply/ler_norm.
Qed.

Lemma : ncvg (fun => \sum_( < n) S i) (PosSum.psum S)%:E.

Proof.

set u := (fun => _); apply: contraPP smS => ncv _.
case: (ncvg_mono_bnd (u := u)) => //.
  by apply/ptsum_homo. by apply/psummable_ptbounded.
move=> x cvux; suff xE: x = (PosSum.psum S) by rewrite xE in cvux.
apply/eqP; case: (x =P _) => // /eqP /lt_total /orP[]; last first.
+ rewrite -lte_fin => /ncvg_gt /(_ cvux) [K /(_ _ (leqnn _))] /=.
  rewrite ltNge lee_fin (le_trans _ (ger_big_ord_psum _ K)) //.
  by apply/ler_sum=> /= i _; apply/ler_norm.
move=> lt_xS; pose e := PosSum.psum S - x.
  have ge0_e: 0 < e by rewrite subr_gt0.
case: (sup_adherent ge0_e (summable_sup smS)) => y.
case=> /= J ->; rewrite /e /PosSum.psum (asboolT smS) subKr => lt_xSJ.
pose k := \max_( : J) (val j); have lt_x_uSk: x < u k.+1.
  apply/(lt_le_trans lt_xSJ); rewrite /u big_ord_mkfset.
  rewrite (eq_bigr (S \o val)) => /= [j _|]; first by rewrite ger0_norm.
  apply/big_fset_subset=> // j jJ; rewrite in_fset //.
  by rewrite (mem_iota _ k.+1) /= add0n ltnS (leq_bigmax (FSetSub jJ)).
have /= := ncvg_homo_le ptsum_homo cvux k.+1; rewrite -/(u _).
by rewrite lee_fin => /le_lt_trans/(_ lt_x_uSk); rewrite ltxx.
Qed.

Lemma :
ncvg (fun => \sum_( < n) S i) l%:E -> summable S.
Proof using ge0_S. End PSumCnv.

Section PSumAsLim.
Context { : realType} { : choiceType}.

Variable ( : T -> R) ( : nat -> {fset T}).

Hypothesis : (forall , 0 <= S x).
Hypothesis : summable S.
Hypothesis : forall , (n <= m)%N -> (P n `<=` P m).
Hypothesis : forall , S x != 0 -> exists , x \in P n.

Lemma : PosSum.psum S = fine (nlim (fun => \sum_( : P n) (S (val j)))).

Proof.

set v := fun => _; have hm_v m n: (m <= n)%N -> v m <= v n.
  by move=> le_mn; apply/big_fset_subset/fsubsetP/homo_P.
have bd_v n : v n <= PosSum.psum S.
  apply/(le_trans _ (gerfin_psum _ smS))/ler_sum.
  by move=> J _; apply/ler_norm.
case: (ncvg_mono_bnd hm_v) => [|l cv].
  apply/asboolP/nboundedP; exists (PosSum.psum S + 1) => //.
    by apply/(le_lt_trans (ge0_psum S)); rewrite ltrDl ltr01.
  move=> n; rewrite ger0_norm ?sumr_ge0 //.
  by rewrite (le_lt_trans (bd_v n)) // ltrDl ltr01.
have le_lS: l <= PosSum.psum S by rewrite -lee_fin (ncvg_leC _ cv).
rewrite (nlimE cv) /= (rwP eqP) eq_le le_lS andbT.
rewrite leNgt; apply/negP=> {le_lS} /(lt_psum smS)[J].
rewrite (big_fset_seq \`|_|) /=; case: J => /= J.
move/canonical_uniq=> uqJ lt_jS; pose K := [seq <- J | S x != 0].
have [n]: exists , {subset K <= P n}; first rewrite {}/K.
  elim: {uqJ lt_jS} J => /= [|x J [n ih]]; first by exists 0%N.
  case: (S x =P 0) => /=; first by move=> _; exists n.
  move/eqP/cover_P=> [k Pk_x]; exists (maxn n k)=> y.
  rewrite inE => /orP[/eqP->|/=].
    by apply/fsubsetP/homo_P/leq_maxr: x Pk_x.
  by move/ih; apply/fsubsetP/homo_P/leq_maxl: y.
move=> le_K_Pn; have: l < v n; first apply/(lt_le_trans lt_jS).
  rewrite (eq_bigr S) => [x _|]; first by rewrite ger0_norm.
  rewrite /v (bigID (fun => S x == 0)) /= big1 => [x /eqP|] //.
  rewrite add0r -big_filter -/K -big_seq_fset ?filter_uniq //=.
  by apply/big_fset_subset => // x; rewrite in_fset => /le_K_Pn.
by apply/negP; rewrite -leNgt -lee_fin ncvg_homo_le.
Qed.

End PSumAsLim.

Section SummableAlg.
Context { : realType} ( : choiceType) ( : Type).

Lemma ( : T -> R) :
summable (S1 \+ S2) -> summable (S2 \+ S1).

Proof.

by apply/eq_summable => x; rewrite /= addrC. Qed.

Lemma ( : T -> R) :
summable (S1 \* S2) -> summable (S2 \* S1).

Proof.

by apply/eq_summable => x; rewrite /= mulrC. Qed.

Lemma ( : T -> R) : summable \`|S| <-> summable S.

Proof.

have h J: \sum_( <- J) `| `|S j| | = \sum_( <- J) `|S j|.
by apply/eq_bigr=> j _; rewrite normr_id.
split=> /summable_seqP[M ge0_M leM]; apply/summable_seqP;
by exists M=> // => J /leM; rewrite h.
Qed.

Lemma : summable (fun _ : T => 0 : R).

Proof.

by exists 0 => J; rewrite big1 ?normr0. Qed.

Lemma ( : T -> R) :
summable S1 -> summable S2 -> summable (S1 \+ S2).

Proof.

Lemma ( : T -> R) : summable S -> summable (- S).

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.
Qed.

Lemma ( : T -> R) :
`[< summable (- S)>] = `[< summable S >].

Proof.

apply/asboolP/asboolP => /summableN //.
by apply/eq_summable => x /=; rewrite opprK.
Qed.

Lemma ( : T -> R) : summable S1 ->
`[< summable (S1 \+ S2) >] = `[< summable S2 >].

Proof.

move=> sm1; apply/asboolP/asboolP; last by apply/(summableD sm1).
move=> sm12; apply/(@eq_summable _ _ ((S1 \+ S2) \- S1)).
by move=> x /=; rewrite addrC addKr.
by apply/summableD/summableN.
Qed.

Lemma ( : T -> R) : summable S2 ->
`[< summable (S1 \+ S2) >] = `[< summable S1 >].

Proof.

move=> sm1; rewrite (@eq_summableb _ _ (S2 \+ S1)) ?summablebDl //.
by move=> x /=; rewrite addrC.
Qed.

Lemma ( : T -> R) : summable S -> summable (c \*o S).

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.
Qed.

Lemma ( : T -> R) ( : R) :
summable S -> summable (c \o* S).

Proof.

by move=> smS; apply/summable_mulrC/summableZ. Qed.

Lemma ( : T -> R) :
(exists , forall , `|S1 x| <= M) -> summable S2 -> summable (S1 \* S2).

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.
Qed.

Lemma ( : T -> R) :
(exists , forall , `|S2 x| <= M) -> summable S1 -> summable (S1 \* S2).

Proof.

by move=> bd sm; apply/summable_mulrC/summableMl. Qed.

Lemma ( : T -> R) :
summable S1 -> summable S2 -> summable (S1 \* S2).

Proof.

move=> smS1 smS2; apply/summableMl => //; exists (PosSum.psum S1).
by move=> x; apply/ger1_psum.
Qed.

Lemma ( : T -> R) : summable f -> summable f^\+.

Proof.

move/summable_abs; apply/le_summable => x.
by rewrite funrpos_ge0 le_funrpos_norm.
Qed.

Lemma ( : T -> R) : summable f -> summable f^\-.

Proof.

by move/summableN/summable_funrpos; apply: eq_summable => x; rewrite funrposN.
Qed.

Lemma ( : T -> R) ( : pred T) :
summable S -> summable (fun => (P x)%:R * S x).

Proof.

case/summable_seqP=> M ge0_M leM; apply/summable_seqP.
exists M => //; move=> J /leM /(le_trans _); apply.
apply/ler_sum=> x _; case: (P x); rewrite (mul1r, mul0r) //.
by rewrite normr0 normr_ge0.
Qed.

Lemma ( : T -> R) ( : pred T) :
summable S -> summable (fun => S x * (P x)%:R).

Proof.

move=> /(summable_condl P) /eq_summable; apply.
by move=> x /=; rewrite mulrC.
Qed.

Lemma ( : T -> R) ( : R) :
(forall , uniq J -> \sum_( <- J) `|S x| <= d) ->
summable S /\ PosSum.psum S <= d.

Proof.

move=> leS; have ge0_d: 0 <= d.
by apply/(le_trans _ (leS [::] _)); rewrite // big_nil.
have smS: summable S by apply/summable_seqP; exists d.
split=> //; rewrite /PosSum.psum (asboolT smS); apply: ge_sup.
by exists 0, fset0; rewrite big_fset0.
apply/ubP=> _ [J ->]; rewrite (big_fset_seq \`|_|) /=.
by apply/leS; case: J => J /= /canonical_uniq.
Qed.

Lemma ( : I -> T -> R) ( : pred I) :
(forall , P i -> summable (F i))
-> summable (fun => \sum_( <- 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 := (F i x) * (P i)%:R + \sum_( <- r | P i) F i x.
apply/(eq_summable (S1 := 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.
by apply/(eq_summable _ summable0) => x; rewrite mulr0.
Qed.

End SummableAlg.

Lemma { : choiceType} { : realType} ( : T -> R) : summable f ->
\esum_( 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.
Qed.

Section StdSum.
Context { : realType} ( : choiceType) ( : Type).
Implicit Type f g S : T -> R.

Lemma : PosSum.psum (fun _ : T => 0) = 0 :> R.

Proof.

rewrite /PosSum.psum asboolT; first by apply/summable0.
set S := [set | _]%classic; suff: S = (set1 0).
by move => ->; rewrite sup1.
rewrite predeqE => x; split.
by case=> J -> /=; rewrite big1 // normr0.
by move=> ->; exists fset0; rewrite big_fset0.
Qed.

Lemma : (forall , f x = 0) -> PosSum.psum f = 0.

Proof.

by move=> eq; rewrite (eq_psum eq) psum0. Qed.

Lemma :
summable f -> PosSum.psum f = 0 -> (forall : T, f x = 0).

Proof.

move=> sm psum_eq0 x; apply/eqP; rewrite -normr_eq0.
rewrite eq_le normr_ge0 andbT -psum_eq0.
apply/(le_trans _ (gerfinseq_psum (r := [:: x]) _ sm)) => //.
by rewrite big_seq1.
Qed.

Lemma : PosSum.psum f <> 0 -> exists : T, f x <> 0.

Proof.

by move=> nz_psum; apply/existsp_asboolPn/asboolPn => /psum_eq0.
Qed.

Lemma : PosSum.psum \`|S| = PosSum.psum S.

Proof.

rewrite /PosSum.psum; do 2! case: ifPn => //; first last.
+ by move/asboolP/summable_abs/asboolP=> ->.
+ by move/asboolPn/summable_abs/asboolPn=> /negbTE->.
move=> _ _; congr sup; rewrite predeqE => x; split.
case=> J ->; exists J.
by under eq_bigr do rewrite normr_id.
case=> J ->; exists J.
by under [in RHS]eq_bigr do rewrite normr_id.
Qed.

Lemma : \`|S1| =1 \`|S2| -> PosSum.psum S1 = PosSum.psum S2.

Proof.

by move=> eqS; rewrite -[LHS]psum_abs -[RHS]psum_abs; apply/eq_psum.
Qed.

Lemma : (forall , `|S1 x| <= `|S2 x|) -> summable S2 ->
PosSum.psum S1 <= PosSum.psum S2.

Proof.

move=> leS smS2; rewrite -[X in X<=_]psum_abs -[X in _<=X]psum_abs.
by apply/le_psum/summable_abs => // x; rewrite normr_ge0 leS.
Qed.

Lemma ( : pred T) :
summable S -> PosSum.psum (fun => (P x)%:R * S x) <= PosSum.psum S.

Proof.

move=> smS; apply/le_psum_abs=> // x; rewrite normrM.
by apply/ler_piMl => //; rewrite normr_nat lern1 leq_b1.
Qed.

Lemma ( : pred T) :
summable S -> PosSum.psum (fun => S x * (P x)%:R) <= PosSum.psum S.

Proof.

move=> smS; apply/(le_trans _ (le_psum_condl P smS)).
rewrite le_eqVlt -(rwP orP); left; apply/eqP/eq_psum.
by move=> x /=; rewrite mulrC.
Qed.

Lemma : PosSum.psum (- S) = PosSum.psum S.

Proof.

case/boolP: `[< summable S >] => h; last first.
by rewrite !psum_out ?oppr0 //; apply/asboolPn; rewrite ?summablebN.
rewrite /PosSum.psum summablebN h; apply/eq_ppsum=> J /=.
by apply/eq_bigr=> j _; rewrite normrN.
Qed.

Lemma :
    (forall , 0 <= S1 x) -> (forall , 0 <= S2 x)
  -> summable S1 -> summable S2
  -> PosSum.psum (S1 \+ S2) = (PosSum.psum S1 + PosSum.psum S2).

Proof.

move=> ge0_S1 ge0_S2 smS1 smS2; have smD := summableD smS1 smS2.
have ge0D: forall , 0 <= S1 x + S2 x by move=> x; rewrite addr_ge0.
rewrite !psumE // (rwP eqP) eq_le -(rwP andP); split.
  apply: ge_sup.
  + by exists 0, fset0; rewrite big_fset0.
  apply/ubP=> _ [J ->]; rewrite big_split /=.
  apply/lerD; rewrite -psumE 1?(le_trans _ (gerfin_psum J _)) //.
  + by apply/ler_sum=> j _ /=; exact/ler_norm.
  + by apply/ler_sum=> j _ /=; exact/ler_norm.
rewrite -lerBrDr; apply: ge_sup.
+ by exists 0, fset0; rewrite big_fset0.
apply/ubP=> _ [J1 ->]; rewrite lerBrDr addrC.
rewrite -lerBrDr; apply: ge_sup.
+ by exists 0, fset0; rewrite big_fset0.
apply/ubP=> _ [J2 ->]; rewrite lerBrDr addrC.
pose J := J1 `|` J2; rewrite -psumE ?(le_trans _ (gerfin_psum J _)) //.
pose D := \sum_( : J) (S1 (val j) + S2 (val j)).
apply/(@le_trans _ _ D); last by apply/ler_sum=> i _; apply/ler_norm.
rewrite /D big_split /=; apply/lerD; apply/big_fset_subset=> //.
+ by apply/fsubsetP/fsubsetUl. + by apply/fsubsetP/fsubsetUr.
Qed.

Lemma : (forall , 0 <= g x <= f x) -> summable f ->
PosSum.psum (f \- g) = PosSum.psum f - PosSum.psum g.

Proof.

move=> gf0 sumf.
have g0 x : 0 <= g x by have /andP[] := gf0 x.
have gf x : g x <= f x by have /andP[] := gf0 x.
rewrite -[in RHS](subrK g f) [in RHS]psumD ?addrK//.
- by move=> x; rewrite subr_ge0.
- by apply: le_summable sumf => x; rewrite subr_ge0 gf lerBlDr lerDl g0.
- exact: le_summable sumf.
Qed.

Lemma : 0 <= c -> PosSum.psum (c \*o S) = c * PosSum.psum S.

Proof.

rewrite le_eqVlt => /orP[/eqP<-|gt0_c].
  by rewrite mul0r psum_eq0 // => x /=; rewrite mul0r.
case/asboolP: (summable S) => [smS|NsmS]; last first.
  rewrite !psum_out ?mulr0 // => smZ; apply/NsmS.
  move/(summableZ c^-1): smZ; apply/eq_summable=> x /=.
  by rewrite mulKf // gt_eqF.
have smZ := summableZ c smS; rewrite (rwP eqP) eq_le.
apply/andP; split; first rewrite {1}/PosSum.psum asboolT //.
  apply: ge_sup.
  + by exists 0, fset0; rewrite big_fset0.
  apply/ubP=> _ [J ->]; rewrite -ler_pdivrMl //.
  rewrite mulr_sumr (le_trans _ (gerfin_psum J _)) //.
  apply/ler_sum=> /= j _; rewrite normrM.
  by rewrite gtr0_norm // mulKf ?gt_eqF.
rewrite -ler_pdivlMl // {1}/PosSum.psum asboolT //; apply: ge_sup.
+ by exists 0, fset0; rewrite big_fset0.
apply/ubP=> _ [J ->]; rewrite ler_pdivlMl //.
rewrite mulr_sumr; apply/(le_trans _ (gerfin_psum J _))=> //.
by apply/ler_sum=> /= j _; rewrite normrM (gtr0_norm gt0_c).
Qed.

Lemma : 0 <= c -> PosSum.psum (c \o* S) = PosSum.psum S * c.

Proof.

move=> ge0_c; rewrite [RHS]mulrC -psumZ //.
by apply/eq_psum => x /=; rewrite mulrC.
Qed.

Lemma ( : I -> T -> R) :
    (forall , 0 <= F i x) -> (forall , summable (F i)) ->
  \sum_( <- r | P i) PosSum.psum (F i) =
    PosSum.psum (fun => \sum_( <- r | P i) F i x).

Proof.

move=> ge0_F sm_F; elim: r => [|i r ih].
  by rewrite big_nil; apply/esym/psum_eq0 => x; rewrite big_nil.
rewrite big_cons ih; case: ifP => Pi; last first.
  by apply/eq_psum=> x /=; rewrite big_cons Pi.
rewrite -psumD //; first by move=> x; apply/sumr_ge0.
  by apply/summable_sum.
by apply/eq_psum=> x /=; rewrite big_cons Pi.
Qed.

Lemma ( : pred T) : summable S ->
PosSum.psum S =
PosSum.psum (fun => (P x)%:R * S x) + PosSum.psum (fun => (~~P x)%:R * S x).

Proof.

have h x: `|S x| = (P x)%:R * `|S x| + (~~P x)%:R * `|S x|.
  by case: (P x); rewrite !Monoid.simpm.
move=> smS; rewrite -[LHS]psum_abs (eq_psum h) psumD.
  by move=> x; rewrite mulr_ge0. by move=> x; rewrite mulr_ge0.
  by apply/summable_condl/summable_abs.
  by apply/summable_condl/summable_abs.
congr (_ + _); apply/eq_psum_abs=> x /=.
  by rewrite !normrM normr_nat normr_id.
  by rewrite !normrM normr_nat normr_id.
Qed.

Lemma ( : seq T) : uniq r -> {subset [pred | S x != 0] <= r} ->
PosSum.psum S = \sum_( <- r) `|S x|.

Proof.

move=> eq_r ler; set s := RHS; have h J: uniq J -> \sum_( <- J) `|S x| <= s.
  move=> uqJ; rewrite (bigID (ssrbool.mem r)) /= addrC big1.
    move=> x xNr; apply/eqP; apply/contraR: xNr.
    by rewrite normr_eq0 => /ler.
  rewrite add0r {}/s -big_filter; set s := seq.filter _ _.
  rewrite [X in _<=X](bigID (ssrbool.mem J)) /=.
  rewrite (perm_big [seq <- r | x \in J]) /=.
    apply/uniq_perm; rewrite ?filter_uniq // => x.
    by rewrite !mem_filter andbC.
  by rewrite big_filter lerDl sumr_ge0.
case/summable_of_bd: h => smS le_psum; apply/eqP.
by rewrite eq_le le_psum /=; apply/gerfinseq_psum.
Qed.

End StdSum.

#[deprecated(since="1.17.0", note="use `psumB` instead")]
Notation := psumB (only parsing).

Section PSumReindex.
Context { : realType} { : choiceType}.
Context ( : T -> R) ( : pred T) ( : U -> T).

Lemma :
     (forall , S x != 0 -> x \in P)
  -> (forall , i \in P -> omap h (h' i) = Some i)
  -> (forall , h i \in P -> h' (h i) = Some i)
  -> PosSum.psum S = PosSum.psum (fun : U => S (h x)).

Proof.

move=> PS hO hP; rewrite !psum_sup_seq; congr sup; rewrite predeqE => x.
split=> -[J uqJ ->] {x}; last first.
  exists [seq h j | <- J & S (h j) != 0].
    rewrite map_inj_in_uniq ?filter_uniq // => y1 y2.
    rewrite !mem_filter => /andP[nz_S1 _] /andP[nz_S2 _].
    by move/(congr1 h'); rewrite !hP ?PS // => -[].
  apply/eqP; rewrite big_map big_filter.
  rewrite (bigID (fun => S (h i) == 0)) /= big1 ?add0r //.
  by move=> y /eqP->; rewrite normr0.
have uqpJ: uniq (pmap h' [seq j | <- J & S j != 0]).
  apply/(map_uniq (f := some)); rewrite pmapS_filter.
  rewrite map_inj_in_uniq ?filter_uniq // => [y1 y2|]; last first.
    by rewrite map_id filter_uniq.
  rewrite !map_id !mem_filter => /andP[h'1 h1] /andP[h'2 h2].
  case/andP: h1 => h1 _; case/andP: h2 => h2 _.
  by move/(congr1 (omap h)); rewrite !hO ?PS // => -[].
exists (pmap h' [seq j | <- J & S j != 0]) => //.
apply/eqP; rewrite -(big_map h predT \`|S|) (bigID [pred | S j == 0]) /=.
rewrite big1 ?add0r => [i /eqP->|]; first by rewrite normr0.
rewrite -big_filter; apply/eqP; apply/perm_big/uniq_perm.
+ by rewrite filter_uniq.
+ rewrite map_inj_in_uniq // !map_id => y1 y2 h1 h2.
  move/(congr1 h'); rewrite !hP ?PS //; last by case.
  * move: h1; rewrite mem_pmap => /mapP[x1].
    rewrite mem_filter => /andP[nz_Sx1 _] /(congr1 (omap h)) /=.
    by rewrite hO ?PS // => -[->].
  * move: h2; rewrite mem_pmap => /mapP[x2].
    rewrite mem_filter => /andP[nz_Sx2 _] /(congr1 (omap h)) /=.
    by rewrite hO ?PS // => -[->].
move=> x; rewrite !mem_filter; apply/andP/idP.
+ case=> nzSx Jx; apply/mapP; move/(_ x (PS _ nzSx)): hO.
  case E: (h' x) => [u|] //= -[xE]; exists u => //.
  rewrite mem_pmap; apply/mapP; exists x => //.
  by rewrite map_id mem_filter nzSx.
+ case/mapP=> u; rewrite mem_pmap => /mapP[t]; rewrite map_id.
  rewrite mem_filter=> /andP[h1 h2] /(congr1 (omap h)) /=.
  by rewrite hO ?PS // => -[->] ->; split.
Qed.

Lemma :
     (forall , S x != 0 -> x \in P)
  -> {on P, bijective h}
  -> PosSum.psum S = PosSum.psum (fun : U => S (h x)).

Proof.

move=> hP [hI h1 h2]; apply/(@reindex_psum_onto (some \o hI)) => //.
- by move=> x Px /=; rewrite h2.
- by move=> x Px /=; rewrite h1.
Qed.

End PSumReindex.

Section PSumPartition.
Context { : realType} { : choiceType} ( : T -> U).

Let := `[< exists : T, f x == y >].

Lemma ( : T -> R) : summable S ->
PosSum.psum S = PosSum.psum (fun => PosSum.psum (fun => S x * (f x == y)%:R)).

Proof.

(* FIXME: this proof is a joke *)
move=> smS; rewrite (rwP eqP) eq_le -(rwP andP); split.
  pose F := `|S x| * (f x == y :> U)%:R.
  have smFy y: summable (F^~ y).
    by apply/summable_condr/summable_abs.
  set G := fun : U => _; have: summable G.
    case/summable_seqP: smS => M ge0_M leM.
    apply/summable_seqP; exists M => // J uqJ; rewrite {}/G.
    rewrite (eq_bigr (fun => PosSum.psum (F^~ y))) => [y _|].
      rewrite ger0_norm ?ge0_psum //; apply/eq_psum_abs => x.
      by rewrite !normrM [ `|_%:R|]ger0_norm ?(normr_id, ler0n).
    rewrite psum_bigop // => [y x|].
      by rewrite mulr_ge0 ?(normr_ge0, ler0n).
    apply/psum_le=> L uqL; pose G := \sum_( <- J | f x == j) `|S x|.
    rewrite (eq_bigr G) => [x _|]; first rewrite ger0_norm //.
    + by rewrite sumr_ge0 // => y _; rewrite mulr_ge0.
    + rewrite /G [RHS]big_mkcond /F /=; apply/eq_bigr=> y _.
      by case: ifPn => //; rewrite !simpm.
    rewrite {}/G /F; pose K := [seq <- L | f x \in J].
    apply/(le_trans _ (leM K _)); rewrite ?filter_uniq //.
    rewrite le_eqVlt -(rwP orP); left; apply/eqP.
    rewrite /K big_filter [RHS]big_mkcond /=; apply/eq_bigr.
    move=> x _; case: ifPn => [fxJ|fxNJ].
      rewrite big_mkcond (bigD1_seq _ fxJ uqJ) /= eqxx.
      by rewrite big1 ?addr0 // => y; rewrite eq_sym => /negbTE=> ->.
    rewrite big_seq_cond big1 // => y; rewrite andbC.
    by case/andP=> /eqP<-; rewrite (negbTE fxNJ).
  move=> smG; apply/psum_le => J uqJ; pose K := undup (map f J).
  move/gerfinseq_psum: smG => /(_ K (undup_uniq _)).
  move/(le_trans _); apply; rewrite {}/G.
  pose G := `|S x| * (f x == y)%:R.
  rewrite (eq_bigr (fun => PosSum.psum (G^~ y))).
    move=> y _; rewrite ger0_norm ?ge0_psum //.
    rewrite -psum_abs; apply/eq_psum=> x.
    by rewrite normrM [ `|_%:R|]ger0_norm ?ler0n.
  rewrite psum_bigop => [y x|y|]; first by rewrite mulr_ge0.
    by apply/summable_condr/summable_abs.
  rewrite (eq_psum (F2 := fun => `|S x * (f x \in K)%:R|)).
    move=> x; rewrite {}/G normrM. (*[ `|_%:R|]ger0_norm //.*)
    case/boolP: (f x \in K); last first.
      move=> fxNK.
      rewrite [ `|_%:R|]ger0_norm // mulr0 big_seq big1 // => y.
      apply/contraTeq; rewrite mulf_eq0 pnatr_eq0 eqb0.
      by rewrite negb_or negbK => /andP[_ /eqP<-].
    move=> fxK; rewrite (bigD1_seq (f x)) ?undup_uniq //=.
    rewrite [ `|_%:R|]ger0_norm // ?ler01 // eqxx !mulr1 big1 ?addr0 // => y; rewrite eq_sym.
    by move/negbTE=> ->; rewrite mulr0.
  rewrite big_seq (eq_bigr (fun => `|S j * (f j \in K)%:R|)) {}/G.
    by move=> x /(map_f f); rewrite -mem_undup => ->; rewrite mulr1.
  rewrite psum_abs; set G := (fun : T => _ in X in _<=X).
  have: summable G by apply/summable_condr.
  move/gerfinseq_psum => /(_ _ uqJ) /(le_trans _); apply.
  by rewrite -big_seq; apply/ler_sum => x _; rewrite normrM.
apply/psum_le=> J uqJ; pose F := PosSum.psum (fun => `|S x| * (f x == j)%:R).
rewrite (eq_bigr F) => [y _|]; first rewrite ger0_norm ?ge0_psum //.
+ rewrite -psum_abs; apply/eq_psum => x; rewrite normrM.
  by rewrite [ `|_%:R|]ger0_norm ?ler0n.
rewrite psum_bigop => [y x|y|].
+ by rewrite mulr_ge0 ?(normr_ge0, ler0n).
+ by apply/summable_condr/summable_abs.
apply/psum_le=> L uqL; pose K := [seq <- L | f x \in J].
have /gerfinseq_psum: uniq K by rewrite filter_uniq.
move=> /(_ _ _ smS) /(le_trans _); apply; rewrite big_filter.
rewrite le_eqVlt -(rwP orP); left; apply/eqP.
rewrite [RHS]big_mkcond /=; apply/eq_bigr=> x _.
rewrite big_seq; case: ifPn => [fx_in_J|fx_Nin_J].
  rewrite -big_seq (bigD1_seq _ fx_in_J uqJ) /= eqxx mulr1.
  rewrite big1 ?addr0 ?normr_id // => y; rewrite eq_sym.
  by move/negbTE=> ->; rewrite mulr0.
rewrite big1 ?normr0 // => y; apply/contraTeq.
rewrite mulf_eq0 pnatr_eq0 eqb0 negb_or negbK.
by case/andP => _ /eqP<-.
Qed.

Lemma ( : T -> R) : summable S ->
PosSum.psum S = PosSum.psum (fun => (C y)%:R * PosSum.psum (fun => S x * (f x == y)%:R)).

Proof.

move=> smS; apply/(eq_trans (partition_psum smS)).
apply/eq_psum => y; case/boolP: (C y); rewrite !simpm //.
move=> NCy; rewrite psum_eq0 // => x; case: (_ =P y).
by move/eqP=> fxE; move/asboolP: NCy; case; exists x.
by rewrite mulr0.
Qed.

End PSumPartition.

Section PSumPair.
Context { : realType} { : choiceType}.

Lemma ( : T * U -> R) : summable S ->
PosSum.psum S = PosSum.psum (fun => PosSum.psum (fun => S (x, y))).

Proof.

move=> sblS; rewrite (partition_psum fst) //; apply/eq_psum.
move=> x /=; pose P := [pred : T * U | xy.1 == x].
rewrite (reindex_psum (h := [eta pair x]) (P := P)) //=.
+ case=> x' y' /=; rewrite mulf_eq0 => /norP[_].
by rewrite pnatr_eq0 eqb0 negbK /P inE => /eqP->.
+ by exists snd => // -[x' y'] /eqP /= <-.
by apply/eq_psum=> y /=; rewrite eqxx mulr1.
Qed.

Lemma ( : T * U -> R) : summable S ->
PosSum.psum S = PosSum.psum (fun => PosSum.psum (fun => S (x, y))).

Proof.

move=> sblS; rewrite (partition_psum snd) //; apply/eq_psum.
move=> y /=; pose P := [pred : T * U | xy.2 == y].
rewrite (reindex_psum (h := [eta pair^~ y]) (P := P)) //=.
+ case=> x' y' /=; rewrite mulf_eq0 => /norP[_].
by rewrite pnatr_eq0 eqb0 negbK /P inE => /eqP->.
+ by exists fst => // -[x' y'] /eqP /= <-.
by apply/eq_psum=> x /=; rewrite eqxx mulr1.
Qed.

End PSumPair.

Section PSumInterchange.
Context { : realType} { : choiceType}.

Let ( : X -> Y -> R) :
(forall , summable (S x)) -> summable (PosSum.psum \o S) ->
summable (fun => S xy.1 xy.2).

Proof.

move=> sumS sum_psumS.
exists (PosSum.psum (PosSum.psum \o S)) => J.
rewrite (big_fset_seq (fun => `|S xy.1 xy.2|))/=.
rewrite (partition_big_imfset _ fst J (fun => `|S xy.1 xy.2|))/=.
pose J1 := [fset xy.1 | in J]%fset.
have := gerfin_psum J1 sum_psumS.
rewrite (big_fset_seq (fun => `|PosSum.psum (S x)|))/=.
apply: le_trans; apply: ler_sum => x _.
rewrite ger0_norm ?ge0_psum//.
pose F := [fset in J | xy.1 == x]%fset.
rewrite [leLHS](_ : _ = \sum_( <- F) `|S x xy.2|).
by rewrite /F big_fset /=; apply: eq_bigr => xy /eqP ->.
rewrite -(big_map snd predT (fun => `|S x y|)).
apply: gerfinseq_psum => //.
rewrite map_inj_in_uniq; last exact: uniq_fset_keys.
move=> [x1 y1] [x2 y2] /[!in_fset] /= /[!inE] /=.
by move=> /andP[_ /eqP ->] /andP[_ /eqP /= ->] ->.
Qed.

Lemma ( : X -> Y -> R) :
    (forall , summable (S x)) -> summable (PosSum.psum \o S) ->
  PosSum.psum (PosSum.psum \o S) =
  PosSum.psum (fun => PosSum.psum (S ^~ y)).

Proof.

move=> row_summable rows_summable.
pose P ( : X * Y) := S xy.1 xy.2.
suff sumP : summable P.
by rewrite -[LHS](psum_pair sumP)// [LHS](psum_pair_swap sumP).
apply: summable_pair_from_rows_psum.
- exact: row_summable.
- exact: eq_summable rows_summable.
Qed.

End PSumInterchange.

#[deprecated(since="1.17.0", note="use `interchange_psum` instead")]
Notation := interchange_psum (only parsing).

Section SumTheory.
Context { : realType} { : choiceType}.

Implicit Types (S : T -> R).

Lemma : (forall , 0 <= S x) -> PosSum.psum S = sum S.

Proof.

move=> ge0_S; rewrite /sum [X in _-X]psum_eq0 ?subr0.
by move=> x; rewrite (@ge0_funrnegE _ _ setT) ?in_setT.
by apply/eq_psum=> x; rewrite (@ge0_funrposE _ _ setT) ?in_setT.
Qed.

Lemma : summable S1 -> summable S2 -> S1 <=1 S2 ->
sum S1 <= sum S2.

Proof.

move=> smS1 smS2 leS; rewrite /sum lerB //.
- apply/le_psum/summable_funrpos => // x.
  by rewrite funrpos_ge0/= (@funrpos_le _ _ setT)//= in_setE.
- apply/le_psum/summable_funrneg => // x.
  rewrite -!funrposN funrpos_ge0 (@funrpos_le _ _ setT) ?in_setE//= => y _.
  by rewrite lerN2.
Qed.

Lemma : sum (@cst T _ 0) = 0 :> R.

Proof.

rewrite /sum !(eq_psum (@funrpos_cst0 _ _), eq_psum (@funrneg_cst0 _ _)).
by rewrite !psum0 subr0.
Qed.

Lemma : sum (- S) = - sum S.

Proof.

by rewrite /sum funrnegN funrposN opprB. Qed.

Lemma : sum (c \*o S) = c * sum S.

Proof.

rewrite (eq_sum (F2 := fun => Num.sg c * (`|c| * S x))).
  by move=> x; rewrite mulrA -numEsg.
transitivity (Num.sg c * sum (`|c| \*o S)).
  case: sgrP => [_|gt0_c|lt0_c]; rewrite ?Monoid.simpm.
  + by rewrite (eq_sum (F2 := cst 0)) ?sum0 // => x; rewrite !mul0r.
  + by apply/eq_sum=> x; rewrite mul1r.
  by rewrite mulN1r -sumN; apply/eq_sum=> x; rewrite !mulN1r.
rewrite {1}/sum !(eq_psum (funrposZ _ _), eq_psum (funrnegZ _ _)) //.
by rewrite !psumZ // -mulrBr mulrA -numEsg.
Qed.

Lemma ( : pred T) :
summable S -> sum S =
sum (fun => (P x)%:R * S x) + sum (fun => (~~ P x)%:R * S x).

Proof.

move=> sm_S; rewrite /sum addrACA -[in RHS]opprD; congr (_ - _).
+ rewrite (psumID P); first exact/summable_funrpos.
by congr (_ + _); apply/eq_psum => x; rewrite funrpos_natrM.
+ rewrite (psumID P); first exact/summable_funrneg.
by congr (_ + _); apply/eq_psum => x; rewrite funrneg_natrM.
Qed.

Lemma ( : seq T) :
uniq r -> {subset [pred | S x != 0] <= r} ->
sum S = \sum_( <- r) S x.

Proof.

move=> eqr domS; rewrite /sum !(psum_finseq eqr).
+ move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
  move: xPS; rewrite /funrpos.
  by apply: contra => /eqP ->; rewrite maxxx.
+ move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
  move: xPS; rewrite /funrneg.
  by apply: contra => /eqP ->; rewrite oppr0 maxxx.
rewrite -sumrB; apply/eq_bigr=> i _.
by rewrite !ger0_norm// -[in RHS](funrposBneg S).
Qed.

Lemma : (forall , S y != 0 -> x == y) -> sum S = S x.

Proof.

move=> domS; rewrite (sum_finseq (r := [:: x])) ?big_seq1//.
by move=> y; rewrite !inE => /domS /eqP->.
Qed.

End SumTheory.

Arguments sum_seq1 {R T} [S] x _.

Files

Module mathcomp.experimental_reals.realsum