Module mathcomp.experimental_reals.realsum

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

# Summability `summable f` : the function $f$ is summable, i.e., there is a bound that bounds every : finite sub-sum of absolute values $|f(x)|$ `psum f` : the supremum of the finite sub-sums if `f` is summable, and 0 o.w. `sum f` : `psum f^\+ - psum f^\-`

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 "\`| f |" := (fun => `|f x|) (at level 2).
Local Notation := Monoid.simpm.

Section Summable.
Context { : 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 <-> esummable [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 /esummable ge0_esum// (@le_lt_trans _ _ M%:E) ?ltey//.
  apply/ereal_supP => _/= [A [/finite_fsetP[B AB] _] <-].
  by rewrite AB fsbigsum; exact: fM.
rewrite /summable => sf.
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//; exact: 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.
Context { : 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) : f =1 g -> summable f -> summable g.

Proof.

move=> fg /esum_summableP sf; apply/esum_summableP.
by apply: eq_esummable sf => x _; rewrite /= fg.
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 <= f x <= g x) -> summable g -> summable f.

Proof.

move=> fg /esum_summableP => sg; apply/esum_summableP.
by apply: le_esummable sg => t _; rewrite /= !lee_fin fg.
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) ( : 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} ( : 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} ( : 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} ( : 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 f -> summable g -> summable (f \+ g).

Proof.

move=> sf sg; apply/esum_summableP.
rewrite [X in esummable _ X](_ : _ = (EFin \o f) \+ (EFin \o g))%E//.
by apply/esummableD; exact/esum_summableP.
Qed.

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

Proof.

move=> sf; apply/esum_summableP.
rewrite [X in esummable _ X](_ : _ = \- (EFin \o f))%E//.
by rewrite -esummableN; exact/esum_summableP.
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 f -> summable (c \*o f).

Proof.

move/esum_summableP => sf; apply/esum_summableP.
rewrite [X in esummable _ X](_ : _ = (fun => c%:E * (f x)%:E)%E)//.
exact: esummableZl.
Qed.

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

Proof.

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

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

Proof.

case=> M leM smg; apply/summable_abs.
apply/(le_summable (g := M \*o \`|g|)).
- by move=> x /=; rewrite normr_ge0 /= normrM ler_wpM2r.
- by apply/summableZ/summable_abs.
Qed.

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

Proof.

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

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

Proof.

move=> sf sg; apply/esum_summableP.
rewrite [X in esummable _ X](_ : _ = (EFin \o f) \* (EFin \o g))%E//.
by apply/esummableM; exact/esum_summableP.
Qed.

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

Proof.

move=> sf; apply/esum_summableP; rewrite -funerpos.
exact/esummable_funepos/esum_summableP.
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 (f := G)) => [x|].
  by rewrite {}/G big_cons; case: ifP=> Pi; rewrite !Monoid.simpm.
apply/summableD => //; case/boolP: (P i) => [|_].
  by move/sm_F; apply/eq_summable => x; rewrite mulr1.
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=> fs; rewrite esumE /sum EFinB.
rewrite -esum_psum//; first exact: summable_funrpos.
rewrite -esum_psum//; first exact: summable_funrneg.
by rewrite funerpos 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