Top source

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.


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

x

---

Source code

=> `|f x|) (at level 2).
Local Notation

simpm

---

Source code

:= Monoid.simpm.

Section Summable.
Context {

T

---

Source code

: choiceType} {

R

---

Source code

: realType} (

f

---

Source code

: T -> R).

Definition

summable

---

Source code

:= exists (

M

---

Source code

: R), forall (

J

---

Source code

: {fset T}),
  \sum_(

x

---

Source code

: J) `|f (val x)| <= M.

Lemma

summableP

---

Source code

: summable ->
  {

M

---

Source code

| 0 <= M & forall (

J

---

Source code

: {fset T}), \sum_(

x

---

Source code

: 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

esum_summableP

---

Source code

{

T

---

Source code

: choiceType} {

R

---

Source code

: realType} (

f

---

Source code

: T -> R) :
  summable f <-> esummable [set: T] (EFin \o f).

Proof.

have fsbigsum (

B

---

Source code

: {fset T}) :
    (\sum_(

x

---

Source code

\in [set` B]) `|f x|%:E)%R = (\sum_(

x

---

Source code

: 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_(

x

---

Source code

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

PosSum

---

Source code

.

Definition

psum

---

Source code

{

R

---

Source code

: realType} {

T

---

Source code

: choiceType} (

f

---

Source code

: T -> R) : R :=
  let

S

---

Source code

:= [set

x

---

Source code

| exists

J

---

Source code

: {fset T}, x = \sum_(

x

---

Source code

: 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

psum

---

Source code

:= PosSum.psum.

Definition

sum

---

Source code

{

R

---

Source code

: realType} {

T

---

Source code

: choiceType} (

f

---

Source code

: T -> R) : R :=
  PosSum.psum f^\+ - PosSum.psum f^\-.

Section SummableCountable.
Context {

T

---

Source code

: choiceType} {

R

---

Source code

: realType} (

f

---

Source code

: T -> R).

Lemma

summable_countn0

---

Source code

: summable f -> discrete.countable [pred

x

---

Source code

| f x != 0].

Proof.

case/summableP=> M ge0_M bM; pose E (

p

---

Source code

: nat) := [pred

x

---

Source code

| `|f x| > p.+1%:~R^-1].
set F := [pred

x

---

Source code

| _]; have le: {subset F <= [pred

x

---

Source code

| `[< exists

p

---

Source code

, 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

s

---

Source code

: 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

x

---

Source code

in s].
suff: \sum_(

x

---

Source code

: J) `|f (val x)| > M by rewrite ltNge bM.
apply/(@lt_le_trans _ _ (\sum_(

x

---

Source code

: 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 {

R

---

Source code

: realType}.

Lemma

ncvg_mono

---

Source code

(

u

---

Source code

: nat -> R) :
    (forall

x

---

Source code

y

---

Source code

, (x <= y)%N -> u x <= u y)
  -> exists2

l

---

Source code

, (-oo < l)%E & ncvg u l.

Proof.

move=> mono_u; pose E := [set

x

---

Source code

| exists

n

---

Source code

, 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

ncvg_mono_bnd

---

Source code

(

u

---

Source code

: nat -> R) :
    (forall

x

---

Source code

y

---

Source code

, (x <= y)%N -> u x <= u y)
  -> nbounded u -> exists

l

---

Source code

, 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 {

R

---

Source code

: realType} (

T

---

Source code

: choiceType).

Implicit Type S : T -> R.

Lemma

summable_sup

---

Source code

(

S

---

Source code

: T -> R) : summable S -> has_sup
  [set

x

---

Source code

| exists

J

---

Source code

: {fset T}, x = \sum_(

j

---

Source code

: 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

psum_sup

---

Source code

S

---

Source code

: PosSum.psum S =
  sup [set

x

---

Source code

| exists

J

---

Source code

: {fset T}, x = \sum_(

x

---

Source code

: J) `|S (val x)|]%classic.

Proof.

rewrite /PosSum.psum; case: ifPn => // /asboolPn h.
rewrite sup_out //; set X := [set

r

---

Source code

| _]%classic => hs.
apply: h; exists (sup X) => J.
by move/ubP : (sup_upper_bound hs); apply; exists J.
Qed.

Lemma

psum_sup_seq

---

Source code

S

---

Source code

: PosSum.psum S =
  sup [set

x

---

Source code

| exists2

J

---

Source code

: seq T, uniq J & x = \sum_(

x

---

Source code

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

x

---

Source code

in J].
by rewrite (big_seq_fset \`|_|).
Qed.

Lemma

eq_summable

---

Source code

(

f

---

Source code

g

---

Source code

: 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

eq_summableb

---

Source code

(

S1

---

Source code

S2

---

Source code

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

Proof.

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

Lemma

eq_ppsum

---

Source code

(

F1

---

Source code

F2

---

Source code

: {fset T} -> R) : F1 =1 F2 ->
  (sup [set

x

---

Source code

| exists

J

---

Source code

, x = F1 J] = sup [set

x

---

Source code

| exists

J

---

Source code

, x = F2 J])%classic.

Proof.

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

Lemma

eq_psum

---

Source code

(

F1

---

Source code

F2

---

Source code

: 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

eq_sum

---

Source code

(

F1

---

Source code

F2

---

Source code

: 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

le_summable

---

Source code

(

f

---

Source code

g

---

Source code

: T -> R) :
  (forall

x

---

Source code

, 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

le_psum

---

Source code

(

F1

---

Source code

F2

---

Source code

: T -> R) :
  (forall

x

---

Source code

, 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

---

Source code

: 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

psum_out

---

Source code

S

---

Source code

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

Proof.

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

Lemma

psumE

---

Source code

S

---

Source code

: (forall

x

---

Source code

, 0 <= S x) -> summable S -> PosSum.psum S =
  sup [set

x

---

Source code

| exists

J

---

Source code

: {fset T}, x = \sum_(

j

---

Source code

: 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

psum_absE

---

Source code

S

---

Source code

: summable S -> PosSum.psum S =
  sup [set

x

---

Source code

| exists

J

---

Source code

: {fset T}, x = \sum_(

j

---

Source code

: J) `|S (val j)|]%classic.

Proof.

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

Lemma

summable_seqP

---

Source code

S

---

Source code

:
  summable S <-> (exists2

M

---

Source code

, 0 <= M &
    forall

s

---

Source code

: seq T, uniq s -> \sum_(

x

---

Source code

<- s) `|S x| <= M).

Proof.

split=> [/summableP|] [M gt0_M h]; exists M => //.
  by move=> s uq_s; have := h [fset

x

---

Source code

in s]; rewrite (big_seq_fset \`|S|).
by case=> J cJ; rewrite (big_fset_seq \`|_|) /=; apply/h/canonical_uniq.
Qed.

Lemma

gerfin_psum

---

Source code

S

---

Source code

(

J

---

Source code

: {fset T}) :
  summable S -> \sum_(

j

---

Source code

: 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

gerfinseq_psum

---

Source code

S

---

Source code

(

r

---

Source code

: seq T) :
  uniq r -> summable S -> \sum_(

j

---

Source code

<- r) `|S j| <= PosSum.psum S.

Proof.

move=> uq_r /gerfin_psum -/(_ [fset

x

---

Source code

in r]);
  by rewrite (big_seq_fset \`|S|).
Qed.

Lemma

psum_le

---

Source code

S

---

Source code

z

---

Source code

:
  (forall

J

---

Source code

, uniq J -> \sum_(

j

---

Source code

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

lt_psum

---

Source code

(

F

---

Source code

: T -> R)

l

---

Source code

:
  summable F -> l < PosSum.psum F ->
    exists

J

---

Source code

: {fset T}, l < \sum_(

j

---

Source code

: 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

esum_psum

---

Source code

{

R

---

Source code

: realType} {

T

---

Source code

: choiceType} (

f

---

Source code

: T -> R) :
    (forall

i

---

Source code

, 0 <= f i) -> summable f ->
  \esum_(

x

---

Source code

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

x

---

Source code

=> `|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

max_sup

---

Source code

{

R

---

Source code

: realType}

x

---

Source code

(

E

---

Source code

: 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 {

R

---

Source code

: realType} (

I

---

Source code

: finType).

Lemma

summable_fin

---

Source code

(

f

---

Source code

: I -> R) : summable f.

Proof.

exists (\sum_(

i

---

Source code

: [fset i |

i

---

Source code

: I]) `|f (val i)|).
move=> J; apply: (big_fset_subset (F := \`|_|)).
  by move=> x; rewrite normr_ge0.
by move=> i _; apply/imfsetP; exists i.
Qed.

Lemma

psum_fin

---

Source code

(

f

---

Source code

: I -> R) : PosSum.psum f = \sum_

i

---

Source code

`|f i|.

Proof.

(* FIXME *)
pose S := \sum_(

i

---

Source code

: [fset i |

i

---

Source code

: I]) `|f (val i)|.
rewrite /PosSum.psum (asboolT (summable_fin f)) (@max_sup _ S).
  rewrite /=; split; first by exists [fset i |

i

---

Source code

: 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 |

j

---

Source code

: I] by rewrite in_imfset.
by exists (FSetSub h) => //; rewrite mem_enum.
Qed.

End FinSumTh.

Section PSumGe.
Context {

R

---

Source code

: realType} (

T

---

Source code

: choiceType) (

S

---

Source code

: T -> R).

Lemma

ger_big_psum

---

Source code

r

---

Source code

: uniq r -> summable S ->
  \sum_(

x

---

Source code

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

x

---

Source code

in r]; rewrite (big_seq_fset (fun

i

---

Source code

=> `|S i|)).
Qed.

Lemma

ger1_psum

---

Source code

x

---

Source code

: 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

ge0_psum

---

Source code

: 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 {

R

---

Source code

: realType} (

S

---

Source code

: nat -> R) (

smS

---

Source code

: summable S).

Lemma

ger_big_ord_psum

---

Source code

n

---

Source code

: \sum_(

i

---

Source code

< n) `|S i| <= PosSum.psum S.

Proof.

rewrite -(big_mkord predT (fun

i

---

Source code

=> `|S i|)) /=.
by apply/ger_big_psum => //; rewrite iota_uniq.
Qed.

End PSumNatGe.

Section PSumCnv.
Context {

R

---

Source code

: realType} (

S

---

Source code

: nat -> R).

Hypothesis

ge0_S

---

Source code

: (forall

n

---

Source code

, 0 <= S n).
Hypothesis

smS

---

Source code

: summable S.

Lemma

ptsum_homo

---

Source code

x

---

Source code

y

---

Source code

: (x <= y)%N -> (\sum_(

i

---

Source code

< x) S i <= \sum_(

i

---

Source code

< 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

psummable_ptbounded

---

Source code

: nbounded (fun

n

---

Source code

=> \sum_(

i

---

Source code

< 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_sum

---

Source code

: ncvg (fun

n

---

Source code

=> \sum_(

i

---

Source code

< n) S i) (PosSum.psum S)%:E.

Proof.

set u := (fun

n

---

Source code

=> _); 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

---

Source code

: 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

sum_ncvg

---

Source code

l

---

Source code

:
  ncvg (fun

n

---

Source code

=> \sum_(

i

---

Source code

< n) S i) l%:E -> summable S.
Proof using ge0_S. End PSumCnv.

Section PSumAsLim.
Context {

R

---

Source code

: realType} {

T

---

Source code

: choiceType} (

S

---

Source code

: T -> R) (

P

---

Source code

: nat -> {fset T}).

Hypothesis

ge0_S

---

Source code

: (forall

x

---

Source code

, 0 <= S x).
Hypothesis

smS

---

Source code

: summable S.
Hypothesis

homo_P

---

Source code

: forall

n

---

Source code

m

---

Source code

, (n <= m)%N -> (P n `<=` P m).
Hypothesis

cover_P

---

Source code

: forall

x

---

Source code

, S x != 0 -> exists

n

---

Source code

, x \in P n.

Lemma

psum_as_lim

---

Source code

:
  PosSum.psum S = fine (nlim (fun

n

---

Source code

=> \sum_(

j

---

Source code

: P n) (S (val j)))).

Proof.

set v := fun

n

---

Source code

=> _; 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

x

---

Source code

<- J | S x != 0].
have [n]: exists

n

---

Source code

, {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

x

---

Source code

=> 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 {

R

---

Source code

: realType} (

T

---

Source code

: choiceType) (

I

---

Source code

: Type).

Lemma

summable_addrC

---

Source code

(

S1

---

Source code

S2

---

Source code

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

Proof.

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

Lemma

summable_mulrC

---

Source code

(

S1

---

Source code

S2

---

Source code

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

Proof.

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

Lemma

summable_abs

---

Source code

(

S

---

Source code

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

Proof.

have h J: \sum_(

j

---

Source code

<- J) `| `|S j| | = \sum_(

j

---

Source code

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

summable0

---

Source code

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

Proof.

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

Lemma

summableD

---

Source code

(

f

---

Source code

g

---

Source code

: 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

summableN

---

Source code

(

f

---

Source code

: 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

summablebN

---

Source code

(

S

---

Source code

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

Proof.

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

Lemma

summablebDl

---

Source code

(

S1

---

Source code

S2

---

Source code

: 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

summablebDr

---

Source code

(

S1

---

Source code

S2

---

Source code

: 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

summableZ

---

Source code

(

f

---

Source code

: T -> R)

c

---

Source code

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

Proof.

move/esum_summableP => sf; apply/esum_summableP.
rewrite [X in esummable _ X](_ : _ = (fun

x

---

Source code

=> c%:E * (f x)%:E)%E)//.
exact: esummableZl.
Qed.

Lemma

summableZr

---

Source code

(

f

---

Source code

: T -> R) (

c

---

Source code

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

Proof.

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

Lemma

summableMl

---

Source code

(

f

---

Source code

g

---

Source code

: T -> R) :
  (exists

M

---

Source code

, forall

x

---

Source code

, `|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

summableMr

---

Source code

(

f

---

Source code

g

---

Source code

: T -> R) :
  (exists

M

---

Source code

, forall

x

---

Source code

, `|g x| <= M) -> summable f -> summable (f \* g).

Proof.

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

Lemma

summableM

---

Source code

(

f

---

Source code

g

---

Source code

: 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

summable_funrpos

---

Source code

(

f

---

Source code

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

Proof.

move=> sf; apply/esum_summableP; rewrite -funerpos.
exact/esummable_funepos/esum_summableP.
Qed.

Lemma

summable_funrneg

---

Source code

(

f

---

Source code

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

Proof.

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

Lemma

summable_condl

---

Source code

(

S

---

Source code

: T -> R) (

P

---

Source code

: pred T) :
  summable S -> summable (fun

x

---

Source code

=> (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

summable_condr

---

Source code

(

S

---

Source code

: T -> R) (

P

---

Source code

: pred T) :
  summable S -> summable (fun

x

---

Source code

=> S x * (P x)%:R).

Proof.

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

Lemma

summable_of_bd

---

Source code

(

S

---

Source code

: T -> R) (

d

---

Source code

: R) :
  (forall

J

---

Source code

, uniq J -> \sum_(

x

---

Source code

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

summable_sum

---

Source code

(

F

---

Source code

: I -> T -> R) (

P

---

Source code

: pred I)

r

---

Source code

:
    (forall

i

---

Source code

, P i -> summable (F i)) ->
  summable (fun

x

---

Source code

=> \sum_(

i

---

Source code

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

x

---

Source code

:= (F i x) * (P i)%:R + \sum_(

i

---

Source code

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

esum_sum

---

Source code

{

T

---

Source code

: choiceType} {

R

---

Source code

: realType} (

f

---

Source code

: T -> R) : summable f ->
  \esum_(

x

---

Source code

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 {

R

---

Source code

: realType} (

T

---

Source code

: choiceType) (

I

---

Source code

: Type).
Implicit Type f g S : T -> R.

Lemma

psum0

---

Source code

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

Proof.

rewrite /PosSum.psum asboolT; first by apply/summable0.
set S := [set

x

---

Source code

| _]%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

psum_eq0

---

Source code

f

---

Source code

: (forall

x

---

Source code

, f x = 0) -> PosSum.psum f = 0.

Proof.

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

Lemma

eq0_psum

---

Source code

f

---

Source code

:
  summable f -> PosSum.psum f = 0 -> (forall

x

---

Source code

: 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

neq0_psum

---

Source code

f

---

Source code

: PosSum.psum f <> 0 -> exists

x

---

Source code

: T, f x <> 0.

Proof.

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

Lemma

psum_abs

---

Source code

S

---

Source code

: 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

eq_psum_abs

---

Source code

S1

---

Source code

S2

---

Source code

: \`|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

le_psum_abs

---

Source code

S1

---

Source code

S2

---

Source code

: (forall

x

---

Source code

, `|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

le_psum_condl

---

Source code

S

---

Source code

(

P

---

Source code

: pred T) :
  summable S -> PosSum.psum (fun

x

---

Source code

=> (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

le_psum_condr

---

Source code

S

---

Source code

(

P

---

Source code

: pred T) :
  summable S -> PosSum.psum (fun

x

---

Source code

=> 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

psumN

---

Source code

S

---

Source code

: 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

psumD

---

Source code

S1

---

Source code

S2

---

Source code

:
    (forall

x

---

Source code

, 0 <= S1 x) -> (forall

x

---

Source code

, 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

x

---

Source code

, 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

---

Source code

: 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

psumB

---

Source code

f

---

Source code

g

---

Source code

: (forall

x

---

Source code

, 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

psumZ

---

Source code

S

---

Source code

c

---

Source code

: 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

psumZr

---

Source code

S

---

Source code

c

---

Source code

: 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

psum_bigop

---

Source code

(

F

---

Source code

: I -> T -> R)

P

---

Source code

r

---

Source code

:
    (forall

i

---

Source code

x

---

Source code

, 0 <= F i x) -> (forall

i

---

Source code

, summable (F i)) ->
  \sum_(

i

---

Source code

<- r | P i) PosSum.psum (F i) =
    PosSum.psum (fun

x

---

Source code

=> \sum_(

i

---

Source code

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

psumID

---

Source code

S

---

Source code

(

P

---

Source code

: pred T) : summable S ->
  PosSum.psum S =
  PosSum.psum (fun

x

---

Source code

=> (P x)%:R * S x) + PosSum.psum (fun

x

---

Source code

=> (~~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

psum_finseq

---

Source code

S

---

Source code

(

r

---

Source code

: seq T) : uniq r -> {subset [pred

x

---

Source code

| S x != 0] <= r} ->
  PosSum.psum S = \sum_(

x

---

Source code

<- r) `|S x|.

Proof.

move=> eq_r ler; set s := RHS; have h J: uniq J -> \sum_(

x

---

Source code

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

x

---

Source code

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

__admitted__psumB

---

Source code

:= psumB (only parsing).

Section PSumReindex.
Context {

R

---

Source code

: realType} {

T

---

Source code

U

---

Source code

: choiceType}.
Context (

S

---

Source code

: T -> R) (

P

---

Source code

: pred T) (

h

---

Source code

: U -> T).

Lemma

reindex_psum_onto

---

Source code

h'

---

Source code

:
     (forall

x

---

Source code

, S x != 0 -> x \in P)
  -> (forall

i

---

Source code

, i \in P -> omap h (h' i) = Some i)
  -> (forall

i

---

Source code

, h i \in P -> h' (h i) = Some i)
  -> PosSum.psum S = PosSum.psum (fun

x

---

Source code

: 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

---

Source code

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

i

---

Source code

=> S (h i) == 0)) /= big1 ?add0r //.
  by move=> y /eqP->; rewrite normr0.
have uqpJ: uniq (pmap h' [seq j |

j

---

Source code

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

---

Source code

<- J & S j != 0]) => //.
apply/eqP; rewrite -(big_map h predT \`|S|) (bigID [pred

j

---

Source code

| 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

reindex_psum

---

Source code

:
     (forall

x

---

Source code

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

x

---

Source code

: 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 {

R

---

Source code

: realType} {

T

---

Source code

U

---

Source code

: choiceType} (

f

---

Source code

: T -> U).

Let

C

---

Source code

y

---

Source code

:= `[< exists

x

---

Source code

: T, f x == y >].

Lemma

partition_psum

---

Source code

(

S

---

Source code

: T -> R) : summable S ->
  PosSum.psum S = PosSum.psum (fun

y

---

Source code

=> PosSum.psum (fun

x

---

Source code

=> 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

x

---

Source code

y

---

Source code

:= `|S x| * (f x == y :> U)%:R.
  have smFy y: summable (F^~ y).
    by apply/summable_condr/summable_abs.
  set G := fun

y

---

Source code

: 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

y

---

Source code

=> 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

x

---

Source code

:= \sum_(

j

---

Source code

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

x

---

Source code

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

x

---

Source code

y

---

Source code

:= `|S x| * (f x == y)%:R.
  rewrite (eq_bigr (fun

y

---

Source code

=> 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

x

---

Source code

=> `|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

j

---

Source code

=> `|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

x

---

Source code

: 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

j

---

Source code

:= PosSum.psum (fun

x

---

Source code

=> `|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

x

---

Source code

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

partition_psum_cond

---

Source code

(

S

---

Source code

: T -> R) : summable S ->
  PosSum.psum S = PosSum.psum (fun

y

---

Source code

=> (C y)%:R * PosSum.psum (fun

x

---

Source code

=> 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 {

R

---

Source code

: realType} {

T

---

Source code

U

---

Source code

: choiceType}.

Lemma

psum_pair

---

Source code

(

S

---

Source code

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

x

---

Source code

=> PosSum.psum (fun

y

---

Source code

=> S (x, y))).

Proof.

move=> sblS; rewrite (partition_psum fst) //; apply/eq_psum.
move=> x /=; pose P := [pred

xy

---

Source code

: 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

psum_pair_swap

---

Source code

(

S

---

Source code

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

y

---

Source code

=> PosSum.psum (fun

x

---

Source code

=> S (x, y))).

Proof.

move=> sblS; rewrite (partition_psum snd) //; apply/eq_psum.
move=> y /=; pose P := [pred

xy

---

Source code

: 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 {

R

---

Source code

: realType} {

X

---

Source code

Y

---

Source code

: choiceType}.

Let

summable_pair_from_rows_psum

---

Source code

(

S

---

Source code

: X -> Y -> R) :
    (forall

x

---

Source code

, summable (S x)) -> summable (PosSum.psum \o S) ->
  summable (fun

xy

---

Source code

=> S xy.1 xy.2).

Proof.

move=> sumS sum_psumS.
exists (PosSum.psum (PosSum.psum \o S)) => J.
rewrite (big_fset_seq (fun

xy

---

Source code

=> `|S xy.1 xy.2|))/=.
rewrite (partition_big_imfset _ fst J (fun

xy

---

Source code

=> `|S xy.1 xy.2|))/=.
pose J1 := [fset xy.1 |

xy

---

Source code

in J]%fset.
have := gerfin_psum J1 sum_psumS.
rewrite (big_fset_seq (fun

x

---

Source code

=> `|PosSum.psum (S x)|))/=.
apply: le_trans; apply: ler_sum => x _.
rewrite ger0_norm ?ge0_psum//.
pose F := [fset

xy

---

Source code

in J | xy.1 == x]%fset.
rewrite [leLHS](_ : _ = \sum_(

xy

---

Source code

<- F) `|S x xy.2|).
  by rewrite /F big_fset /=; apply: eq_bigr => xy /eqP ->.
rewrite -(big_map snd predT (fun

y

---

Source code

=> `|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

interchange_psum

---

Source code

(

S

---

Source code

: X -> Y -> R) :
    (forall

x

---

Source code

, summable (S x)) -> summable (PosSum.psum \o S) ->
  PosSum.psum (PosSum.psum \o S) =
  PosSum.psum (fun

y

---

Source code

=> PosSum.psum (S ^~ y)).

Proof.

move=> row_summable rows_summable.
pose P (

xy

---

Source code

: 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

__admitted__interchange_psum

---

Source code

:= interchange_psum (only parsing).

Section SumTheory.
Context {

R

---

Source code

: realType} {

T

---

Source code

: choiceType}.

Implicit Types (S : T -> R).

Lemma

psum_sum

---

Source code

S

---

Source code

: (forall

x

---

Source code

, 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

le_sum

---

Source code

S1

---

Source code

S2

---

Source code

: 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

sum0

---

Source code

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

Proof.

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

Lemma

sumN

---

Source code

S

---

Source code

: sum (- S) = - sum S.

Proof.

by rewrite /sum funrnegN funrposN opprB. Qed.

Lemma

sumZ

---

Source code

S

---

Source code

c

---

Source code

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

Proof.

rewrite (eq_sum (F2 := fun

x

---

Source code

=> 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

sumID

---

Source code

S

---

Source code

(

P

---

Source code

: pred T) :
  summable S -> sum S =
    sum (fun

x

---

Source code

=> (P x)%:R * S x) + sum (fun

x

---

Source code

=> (~~ 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

sum_finseq

---

Source code

S

---

Source code

(

r

---

Source code

: seq T) :
  uniq r -> {subset [pred

x

---

Source code

| S x != 0] <= r} ->
    sum S = \sum_(

x

---

Source code

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

sum_seq1

---

Source code

S

---

Source code

x

---

Source code

: (forall

y

---

Source code

, 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 _.