Feature esum psum esum only

CHANGELOG_UNRELEASED.md

@@ -92,6 +92,25 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+- in `realsum.v`:
+  + lemma `esum_psum`
+  + lemma `sum_sum`
+
+- in `constructive_ereal.v`:
+  + definition `esg`
+  + lemmas `numEesg`, `gte0_esg`, `lte0_esg`, `esg0`
+
+- in `esum.v`:
+  + lemmas `esum_eq0P`, `esumZ`, `esum_esum'`
+  + lemmas `ge0_funeneg`, `ge0_funepos`, `funepos_cst0`, `funeneg_cst0`,
+    `le_funepos`
+  + definition `sum`
+  + lemmas `sum0`, `eq_sum`, `esum_unit`, `sum_unit`
+  + lemmas `esum_sum'`, `sum_ge0`, `le_sum`, `sumN`, `sumZ`
+  + lemmas `summable_le_sum`, `summable_esum_funepos`, `summable_sumN`,
+    `summableZ`, `summable_sumZ`
+  + lemmas `ereal_sup_comm`
+  + lemmas `esupZl`, `esupZl_range`, `esup_add`, `ereal_sup_sum`, `esum_esup_comm`
 
 ### Changed
 
@@ -182,6 +201,18 @@
   + 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`:
+  + 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 `ge0_funrneg`, `ge0_funrpos`
+    * lemmas `le_funrpos_norm`, `funrpos_le`
+    * definition `sum`
+    * lemmas `summable_funrpos`, `summable_funrneg`
+  + lemma `sum0` (now uses `cst`)
 
 ### Renamed
 
@@ -252,6 +283,9 @@
 - in `simple_functions.v`:
   + lemmas `fctD`, `fctN`, `fctM`, `fctZ`
 
+- in `ereal.v`:
+  + lemmas `ge0_mule_fsumr`, `ge0_mule_fsuml`
+
 ### Deprecated
 
 - file `charge.v` (use `measure.v` and/or `lebesgue_integral.v`)
@@ -263,6 +297,12 @@
 - 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`
+
 ### Infrastructure
 
 ### Misc

experimental_reals/distr.v

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