Feature esum psum esum only (math-comp#1978)

* Add missing lemmas for distr

* use fun{r,e}{pos,neg} instead of f{pos,neg}

* esum lemmas from PR math-comp#1954

* new definition of esum

* prove __admitted__psumB

---------

Co-authored-by: Lionel Blatter <lionel.blatter@wanadoo.fr>
Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

Author: 3 people

CHANGELOG_UNRELEASED.md

@@ -112,6 +112,27 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+- in `realsum.v`:
+  + lemma `esum_psum`
+  + lemma `esum_sum`
+
+- in `constructive_ereal.v`:
+  + definition `esg`
+  + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0`
+
+- in `esum.v`:
+  + lemmas `esum_eq0P`, `esumZ`, `exchange_esum`
+  + lemmas `le_esum`, `esumN`
+  + lemmas `summable_le_esum`, `summable_esum_funepos`, `summable_esumN`,
+    `summableZ`, `summable_esumZ`
+  + lemmas `esum_if_eq_op`
+  + lemmas `exchange_esum_ereal_sup`
+
+- in `ereal.v`:
+  + lemmas `exchange_ereal_sup`, `ge0_ereal_supZl`, `ge0_ereal_supZl_range`
+
+- in `sequences.v`:
+  + lemmas `ereal_supD`, `ereal_sup_sum`
 
 - in `reals.v`:
   + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
@@ -151,6 +172,12 @@
 - in `lebesgue_stieltjes_measure.v`:
   + definition `lebesgue_display`
 
+- in `realsum.v`:
+  + lemma `esum_summableP`
+
+- in `esum.v`:
+  + lemma `fsetsTE`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -182,6 +209,13 @@
 - new files `signed_measure.v` and `radon_nikodym.v`
   + with the contents of `charge.v` (deprecated)
 
+- in `esum.v`:
+  + lemma `ge0_esum`
+  + lemma `esum_ge`
+
+- in `realsum.v`:
+  + lemma `__admitted__psumB` proved and renamed to `psumB`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -245,6 +279,30 @@
   + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`,
     `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
     `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
+- in `realsum.v`:
+  + the following now use `funrpos` and `funrneg`:
+    * definition `sum`
+    * lemmas `summable_funrpos`, `summable_funrneg`
+  + lemma `sum0` (now uses `cst`)
+
+- moved from `realsum` to `numfun.v`:
+  + now use `funrpos` and `funrneg`:
+    * lemmas `eq_funrpos`, `eq_funrneg`
+    * lemma `fpos0` (renamed to `funrpos_cst0`)
+    * lemma `fneg0` (renamed to `funrneg_cst0`)
+    * lemmas `funrposZ`, `funrnegZ`
+    * lemmas `funrpos_natrM`, `funrneg_natrM`
+    * lemmas `le_funrpos_norm`
+
+- moved from `numfun.v` to `unstable.v`:
+  + notations `nondecreasing_fun`, `nonincreasing_fun`,
+    `decreasing_fun`, `increasing_fun`
+
+- in `esum.v`:
+  + definition `esum`
+  + lemma `esum_fset`
+  + lemma `esum_ge` -> `PosEsum.pos_esum_ge`
+  + lemma `le_esum` -> `PosEsum.le_pos_esum`
 
 - moved from `normed_module.v` to `metric_structure.v`
   + lemma `squeeze_cvgr`
@@ -296,6 +354,11 @@
 
 - in `topology_structure.v`:
   + `closure_setC` -> `closureC`
+- in `esum.v`:
+  + `esum_sum` -> ` exchange_esum_sum`
+
+- in `realsum.v`:
+  + `psum` -> `PosSum.psum`
 
 ### Generalized
 
@@ -328,6 +391,12 @@
   generalized from `realType` to `sigmaRingType d'`, adding a display parameter `d'`;
     generalized from `realType` to `sigmaRingType d'`, adding a display parameter `d'`;
 
+- in `ereal.v`:
+  + lemmas `ge0_mule_fsumr`, `ge0_mule_fsuml`
+
+- in `esum.v`:
+  + lemma `esum_set1`
+
 ### Deprecated
 
 - file `charge.v` (use `measure.v` and/or `lebesgue_integral.v`)
@@ -362,6 +431,12 @@
 
 - in `random_variable.v`:
   + notation `expectationM` (deprecated since 1.8.0)
+- in `realsum.v`:
+  + definitions `fpos`, `fneg` (use `funrpos`, `funrneg` instead)
+  + lemmas `fnegN`, `fposN`
+  + lemmas `ge0_pos`, `ge0_neg`
+  + lemma `fposBfneg`
+  + lemma `funrpos_le`
 
 ### Infrastructure
 

classical/unstable.v

@@ -16,6 +16,10 @@ From mathcomp Require Import vector archimedean interval.
 (* ```                                                                        *)
 (*                 swap x := (x.2, x.1)                                       *)
 (*           map_pair f x := (f x.1, f x.2)                                   *)
+(*    nondecreasing_fun f == the function f is non-decreasing                 *)
+(*    nonincreasing_fun f == the function f is non-increasing                 *)
+(*       increasing_fun f == the function f is (strictly) increasing          *)
+(*       decreasing_fun f == the function f is (strictly) decreasing          *)
 (*          monotonic A f := {in A &, {homo f : x y / x <= y}} \/             *)
 (*                           {in A &, {homo f : x y /~ x <= y}}               *)
 (*   strict_monotonic A f := {in A &, {homo f : x y / x < y}} \/              *)
@@ -197,6 +201,15 @@ rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
 by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
 Qed.
 
+Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n <= m)%O})
+  (at level 10).
+Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O})
+  (at level 10).
+Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O})
+  (at level 10).
+Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O})
+  (at level 10).
+
 Definition monotonic d (T : porderType d) d' (T' : porderType d')
     (pT : predType T) (A : pT) (f : T -> T') :=
   {in A &, nondecreasing f} \/ {in A &, {homo f : x y /~ (x <= y)%O}}.

experimental_reals/distr.v

@@ -46,7 +46,7 @@ Structure distr := Distr {
   mu :> T -> R;
   _  :  forall x, 0 <= mu x;
   _  :  summable mu;
-  _  :  psum mu <= 1
+  _  :  PosSum.psum mu <= 1
 }.
 
 Definition distr_of & phant R & phant T := distr.
@@ -63,7 +63,7 @@ Context {R : realType} (T : choiceType) (mu : {distr T / R}).
 Lemma ge0_mu : forall x, 0 <= mu x.
 Proof. by case: mu. Qed.
 
-Lemma le1_mu : psum mu <= 1.
+Lemma le1_mu : PosSum.psum mu <= 1.
 Proof. by case: mu. Qed.
 
 Lemma summable_mu : summable mu.
@@ -119,7 +119,7 @@ Proof. by apply: (iffP idP) => /eqP. Qed.
 Lemma dinsuppPn mu x : reflect (mu x = 0) (x \notin dinsupp mu).
 Proof. by rewrite -topredE /dinsupp /= negbK; apply/eqP. Qed.
 
-Definition pr   mu E   := psum (fun x => (E x)%:R * mu x).
+Definition pr   mu E   := PosSum.psum (fun x => (E x)%:R * mu x).
 Definition prc  mu E A := pr mu [predI E & A] / pr mu A.
 Definition esp  mu f   := sum (fun x => f x * mu x).
 Definition espc mu f A := sum (fun x => f x * prc mu (pred1 x) A).
@@ -153,7 +153,7 @@ move=> s /h /(le_trans _); apply; rewrite le_eqVlt; apply/orP.
 by left; apply/eqP/eq_bigr=> i _; rewrite ger0_norm ?isd1.
 Qed.
 
-Local Lemma isd3 : psum mu <= 1.
+Local Lemma isd3 : PosSum.psum mu <= 1.
 Proof.
 rewrite psumE; [apply/isd1 | apply/isd2 | apply: ge_sup].
   by exists 0, fset0; rewrite big_fset0.
@@ -181,7 +181,7 @@ Qed.
 Lemma le1_mu1
   {R : realType} {T : choiceType} (mu : {distr T / R}) x : mu x <= 1.
 Proof.
-apply/(@le_trans _ _ (psum mu)) => //; rewrite -[mu x]ger0_norm//.
+apply/(@le_trans _ _ (PosSum.psum mu)) => //; rewrite -[mu x]ger0_norm//.
 by apply/ger1_psum.
 Qed.
 
@@ -356,7 +356,7 @@ Implicit Types (T U : choiceType).
 Section Bind.
 Context {T U : choiceType} (f : T -> distr U) (mu : distr T).
 
-Definition mlet := fun y : U => psum (fun x => mu x * f x y).
+Definition mlet := fun y : U => PosSum.psum (fun x => mu x * f x y).
 
 Lemma isd_mlet : isdistr mlet.
 Proof.
@@ -373,7 +373,7 @@ Qed.
 
 Definition dlet := locked (mkdistr isd_mlet).
 
-Lemma dletE y : dlet y = psum (fun x => mu x * f x y).
+Lemma dletE y : dlet y = PosSum.psum (fun x => mu x * f x y).
 Proof. by unlock dlet. Qed.
 End Bind.
 
@@ -511,7 +511,7 @@ Lemma __deprecated__dlet_dlet (mu : {distr T / R}) :
 Proof.
 move=> z; unlock dlet => /=; rewrite /mlet /=.
 pose S y x := mu x * (f1 x y * f2 y z).
-rewrite (eq_psum (F2 := fun y => psum (S^~ y))) => [x|].
+rewrite (eq_psum (F2 := fun y => PosSum.psum (S^~ y))) => [x|].
   by rewrite -psumZ //; apply/eq_psum => y /=.
 rewrite __admitted__interchange_psum.
 + by move=> x; apply/summableZ/summable_mlet.
@@ -713,7 +713,7 @@ Section MarginalsTh.
 Variable (T U V : choiceType).
 
 Lemma dmargin_psumE (mu : {distr T / R}) (f : T -> U) y :
-  (dmargin f mu) y = psum (fun x => (f x == y)%:R * mu x).
+  (dmargin f mu) y = PosSum.psum (fun x => (f x == y)%:R * mu x).
 Proof.
 rewrite dmarginE dletE; apply/eq_psum => x //=.
 by rewrite mulrC dunit1E.
@@ -812,7 +812,7 @@ Section DFst.
 Context {R : realType} {T U : choiceType}.
 
 Lemma dfstE (mu : {distr (T * U) /  R}) x :
-  dfst mu x = psum (fun y => mu (x, y)).
+  dfst mu x = PosSum.psum (fun y => mu (x, y)).
 Proof.
 rewrite dmargin_psumE /=; pose h y : T * U := (x, y).
 rewrite (reindex_psum (P := [pred z | z.1 == x]) (h := h)) /=.
@@ -837,7 +837,7 @@ Section DSnd.
 Context {R : realType} {T U : choiceType}.
 
 Lemma __deprecated__dsndE (mu : {distr (T * U) / R}) y :
-  dsnd mu y = psum (fun x => mu (x, y)).
+  dsnd mu y = PosSum.psum (fun x => mu (x, y)).
 Proof. by rewrite -__deprecated__dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.
 
 Lemma summable_snd (mu : {distr (T * U) / R}) y :
@@ -878,7 +878,7 @@ Qed.
 Lemma pr_exp mu (E : pred T) : \P_[mu] E = \E_[mu] (fun m => (E m)%:R).
 Proof. by rewrite /pr psum_sum // => x; rewrite mulr_ge0 // ler0n. Qed.
 
-Lemma pr_predT mu : \P_[mu] predT = psum mu.
+Lemma pr_predT mu : \P_[mu] predT = PosSum.psum mu.
 Proof. by apply/eq_psum=> x; rewrite mul1r. Qed.
 
 Lemma pr_dunit E x : \P_[dunit x] E = (E x)%:R :> R.
@@ -963,7 +963,7 @@ Proof.
 rewrite /esp -psum_sum => [x|]; first by rewrite mulr_ge0 ?ge0_pr.
 rewrite /pr; unlock dlet => /=; rewrite /mlet /=.
 pose F x y := (E x)%:R * (mu y * f y x).
-transitivity (psum (fun x => psum (fun y => F x y))); rewrite {}/F.
+transitivity (PosSum.psum (fun x => PosSum.psum (fun y => F x y))); rewrite {}/F.
   by apply/eq_psum => x; rewrite -psumZ ?ler0n.
 rewrite __admitted__interchange_psum /=; last first.
   apply/eq_psum=> y /=; rewrite mulrC -psumZ //.
@@ -1048,7 +1048,7 @@ by move/ler_pdivrMr=> ->; rewrite mul1r le_in_pr // => x _ /andP[].
 Qed.
 
 Lemma prc_sum A mu : 0 < \P_[mu] A ->
-  psum (fun x => \P_[mu, A] (pred1 x)) = 1.
+  PosSum.psum (fun x => \P_[mu, A] (pred1 x)) = 1.
 Proof.
 move=> gt0_pE; rewrite psumZr ?(invr_ge0, ge0_pr) //.
 rewrite (eq_psum (F2 := (fun x => (A x)%:R * mu x))); last first.
@@ -1264,5 +1264,3 @@ End Jensen.
 End Jensen.
 
 Notation convex f := (convexon \-inf \+inf f).
-
-(* -------------------------------------------------------------------- *)