Feature esum psum esum only

CHANGELOG_UNRELEASED.md

@@ -92,6 +92,27 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+- in `realsum.v`:
+  + lemma `esum_psum`
+  + lemma `esumEsum`
+
+- 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`
@@ -128,12 +149,6 @@
     * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
   + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
 
-### Changed
-
-- moved from `measurable_structure.v` to `classical_sets.v`:
-  + definition `preimage_set_system`
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
-    `preimage_set_system_id`
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
@@ -159,6 +174,10 @@
 - 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`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -222,6 +241,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`
 
 ### Renamed
 
@@ -264,6 +307,9 @@
 - in `measure_function.v`:
   + `isFinite` -> `isFinNumFun`
 
+- in `esum.v`:
+  + `esum_sum` -> ` exchange_esum_sum`
+
 ### Generalized
 
 - in `measurable_structure.v`:
@@ -292,6 +338,12 @@
 - in `simple_functions.v`:
   + lemmas `fctD`, `fctN`, `fctM`, `fctZ`
 
+- 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`)
@@ -303,6 +355,13 @@
 - in `measurable_structure.v`:
   + lemmas `measurable_prod_g_measurableType`, `measurable_prod_g_measurableTypeR`
 
+- in `realsum.v`:
+  + definitions `fpos`, `fneg` (use `funrpos`, `funrneg` instead)
+  + lemmas `fnegN`, `fposN`
+  + lemmas `ge0_pos`, `ge0_neg`
+  + lemma `fposBfneg`
+  + lemma `funrpos_le`
+
 ### Infrastructure
 
 ### Misc

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

@@ -1264,5 +1264,3 @@ End Jensen.
 End Jensen.
 
 Notation convex f := (convexon \-inf \+inf f).
-
-(* -------------------------------------------------------------------- *)