Feature esum psum esum only

.github/workflows/nix-action-9.0-2.5.0.yml

@@ -423,7 +423,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -477,9 +477,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "9.0-2.5.0" --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "9.0-2.5.0" --argstr job "mathcomp-reals"
+        "9.0-2.5.0" --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 

.github/workflows/nix-action-9.0.yml

@@ -356,7 +356,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -410,9 +410,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" 
         --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" 
-        --argstr job "mathcomp-reals"
+        --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" 

.github/workflows/nix-action-9.1.yml

@@ -356,7 +356,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -410,9 +410,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" 
         --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" 
-        --argstr job "mathcomp-reals"
+        --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" 

.github/workflows/nix-action-master.yml

@@ -617,7 +617,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     - mathcomp-bigenough
     runs-on: ubuntu-latest
     steps:
@@ -672,9 +672,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "master" --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "master" --argstr job "mathcomp-reals"
+        "master" --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"cdb1bab419a46125ba129bd32e273b32d8f13f23"
+"6b32b8cd491ec44b75da86fb17e4353f2f102328"

.nix/rocq-overlays/mathcomp-analysis/default.nix

@@ -0,0 +1,125 @@
+{
+  lib,
+  mkRocqDerivation,
+  mathcomp,
+  mathcomp-finmap,
+  mathcomp-bigenough,
+  stdlib,
+  single ? false,
+  rocq-core,
+  version ? null,
+}@args:
+
+let
+  repo = "analysis";
+  owner = "math-comp";
+
+  release."1.16.0".sha256 = "sha256-L0dCbxEqxI8rFv6OOEoIT/U3GKX37ageU9yw2H6hrWY=";
+
+  defaultVersion =
+    let
+      case = rocq: mc: out: {
+        cases = [
+          rocq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ rocq-core.rocq-version mathcomp.version ]
+      [
+        (case (range "9.0" "9.1") (range "2.4.0" "2.5.0") "1.16.0")
+      ]
+      null;
+
+  # list of analysis packages sorted by dependency order
+  packages = {
+    "classical" = [ ];
+    "reals" = [ "classical" ];
+    "analysis" = [ "reals" ];
+    "experimental-reals" = [ "analysis" ];
+    "reals-stdlib" = [ "reals" ];
+    "analysis-stdlib" = [
+      "analysis"
+      "reals-stdlib"
+    ];
+  };
+
+  mathcomp_ =
+    package:
+    let
+      classical-deps = [
+        mathcomp.algebra
+        mathcomp-finmap
+      ];
+      experimental-reals-deps = [ mathcomp-bigenough ];
+      analysis-deps = [
+        mathcomp.field
+        mathcomp-bigenough
+      ];
+      intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
+      pkgpath =
+        let
+          case = case: out: { inherit case out; };
+        in
+        lib.switch package [
+          (case "single" ".")
+          (case "analysis" "theories")
+          (case "experimental-reals" "experimental_reals")
+          (case "reals-stdlib" "reals_stdlib")
+          (case "analysis-stdlib" "analysis_stdlib")
+        ] package;
+      pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
+      derivation = mkRocqDerivation {
+        inherit
+          version
+          pname
+          defaultVersion
+          release
+          repo
+          owner
+          ;
+
+        namePrefix = [
+          "rocq-core"
+          "mathcomp"
+        ];
+
+        propagatedBuildInputs =
+          intra-deps
+          ++ lib.optionals (lib.elem package [
+            "classical"
+            "single"
+          ]) classical-deps
+          ++ lib.optionals (lib.elem package [
+            "experimental-reals"
+            "single"
+          ]) experimental-reals-deps
+          ++ lib.optionals (lib.elem package [
+            "analysis"
+            "single"
+          ]) analysis-deps
+          ++ lib.optional (lib.elem package [
+            "reals-stdlib"
+            "analysis-stdlib"
+            "single"
+          ]) stdlib;
+
+        preBuild = ''
+          cd ${pkgpath}
+        '';
+
+        meta = {
+          description = "Analysis library compatible with Mathematical Components";
+          maintainers = [ lib.maintainers.cohencyril ];
+          license = lib.licenses.cecill-c;
+        };
+
+        passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
+      };
+    in
+    derivation;
+in
+mathcomp_ (if single then "single" else "analysis")

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).
-
-(* -------------------------------------------------------------------- *)