Merge pull request #374 from proux01/dual-ereal

Dual ereal
math-comp · Nov 4, 2021 · 2f2359f · 2f2359f
2 parents d05ff31 + 87c5444
commit 2f2359f
Show file tree

Hide file tree

Showing 2 changed files with 792 additions and 4 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -100,6 +100,39 @@
   + lemmas `mule_le0_ge0`, `mule_ge0_le0`, `pmule_rle0`, `pmule_lle0`,
     `nmule_lle0`, `nmule_rle0`
   + lemma `sube0`
+  + lemmas `adde_le0`, `sume_le0`, `oppe_ge0`, `oppe_le0`,
+    `lte_opp`, `gee_addl`, `gee_addr`, `lte_addr`,
+    `gte_subl`, `gte_subr`, `lte_le_sub`, `lee_sum_npos_subset`,
+    `lee_sum_npos`, `lee_sum_npos_ord`, `lee_sum_npos_natr`,
+    `lee_sum_npos_natl`, `lee_sum_npos_subfset`, `lee_opp`,
+    `le0_muleDl`, `le0_muleDr`, `le0_sume_distrl`, `le0_sume_distrr`,
+    `adde_defNN`, `minEFin`, `mine_ninftyl`, `mine_ninftyr`, `mine_pinftyl`,
+    `mine_pinftyr`, `oppe_max`, `oppe_min`, `mineMr`, `mineMl`
+  + definitions `dual_adde`
+  + notations for the above in scope `ereal_dual_scope` delimited by `dE`
+  + lemmas `dual_addeE`, `dual_sumeE`, `dual_addeE_def`, `daddEFin`,
+    `dsumEFin`, `dsubEFin`, `dadde0`, `dadd0e`, `daddeC`, `daddeA`,
+    `daddeAC`, `daddeCA`, `daddeACA`, `doppeD`, `dsube0`, `dsub0e`, `daddeK`,
+    `dfin_numD`, `dreal_of_extendedD`, `dsubeK`, `dsube_eq`,
+    `dsubee`, `dadde_eq_pinfty`, `daddooe`, `dadde_Neq_pinfty`,
+    `dadde_Neq_ninfty`, `desum_fset_pinfty`, `desum_pinfty`,
+    `desum_fset_ninfty`, `desum_ninfty`, `dadde_ge0`, `dadde_le0`,
+    `dsume_ge0`, `dsume_le0`, `dsube_lt0`, `dsubre_le0`,
+    `dsuber_le0`, `dsube_ge0`, `lte_dadd`, `lee_daddl`, `lee_daddr`,
+    `gee_daddl`, `gee_daddr`, `lte_daddl`, `lte_daddr`, `gte_dsubl`,
+    `gte_dsubr`, `lte_dadd2lE`, `lee_dadd2l`, `lee_dadd2lE`,
+    `lee_dadd2r`, `lee_dadd`, `lte_le_dadd`, `lee_dsub`,
+    `lte_le_dsub`, `lee_dsum`, `lee_dsum_nneg_subset`,
+    `lee_dsum_npos_subset`, `lee_dsum_nneg`, `lee_dsum_npos`,
+    `lee_dsum_nneg_ord`, `lee_dsum_npos_ord`, `lee_dsum_nneg_natr`,
+    `lee_dsum_npos_natr`, `lee_dsum_nneg_natl`, `lee_dsum_npos_natl`,
+    `lee_dsum_nneg_subfset`, `lee_dsum_npos_subfset`,
+    `lte_dsubl_addr`, `lte_dsubl_addl`, `lte_dsubr_addr`,
+    `lee_dsubr_addr`, `lee_dsubl_addr`, `ge0_dsume_distrl`, `dmulrEDr`,
+    `dmulrEDl`, `dge0_mulreDr`, `dge0_mulreDl`, `dle0_mulreDr`, `dle0_mulreDl`,
+    `ge0_dsume_distrr`, `le0_dsume_distrl`, `le0_dsume_distrr`,
+    `lee_abs_dadd`, `lee_abs_dsum`, `lee_abs_dsub`, `dadde_minl`, `dadde_minr`,
+    `lee_dadde`, `lte_spdaddr`
 - in `normedtype.v`:
   + lemma `mule_continuous`
 - in `cardinality.v`: