powere_pos lemmas

CHANGELOG_UNRELEASED.md

@@ -28,11 +28,11 @@
     `ae_pointwise_almost_uniform`.
 
 - in `exp.v`:
-  + lemmas `power_posrM`, `gt0_ler_power_pos`,
-    `gt0_power_pos`, `norm_power_pos`, `lt0_norm_power_pos`,
-    `power_posB`
-  + lemmas `powere_posrM`, `powere_posAC`, `gt0_powere_pos`,
-    `powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`, `powere_posB`
+  + lemmas `powRrM`, `gt0_ler_powR`,
+    `gt0_powR`, `norm_powR`, `lt0_norm_powR`,
+    `powRB`
+  + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`,
+    `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB`
 
 - in `mathcomp_extra.v`:
   + definition `min_fun`, notation `\min`
@@ -41,6 +41,14 @@
 - in `lebesgue_measure.v`:
   + lemmas `measurable_fun_ltr`, `measurable_minr`
 
+- in `exp.v`:
+  + notation `` e `^?(r +? s) ``
+  + lemmas `expR_eq0`, `powRN`
+  + definition `poweRD_def`
+  + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`,
+    `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def`
+  + lemmas `powR_eq0`, `poweR_eq0`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
@@ -49,20 +57,72 @@
 
 - moved from `functions.v` to `classical_sets.v`: `subsetP`.
 
+- in `exp.v`:
+  + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`)
+
 ### Renamed
 
 - in `boolp.v`:
   + `mextentionality` -> `mextensionality`
   + `extentionality` -> `extensionality`
+
 - in `exp.v`:
   + `expK` -> `expRK`
 
+- in `exp.v`:
+  + `power_pos_eq0` -> `powR_eq0_eq0`
+  + `power_pos_inv` -> `powR_invn`
+  + `powere_pos_eq0` -> `poweR_eq0_eq0`
+
+- in `exp.v`:
+  + `power_pos` -> `powR`
+  + `power_pos_ge0` -> `powR_ge0`
+  + `power_pos_gt0` -> `powR_gt0`
+  + `gt0_power_pos` -> `gt0_powR`
+  + `power_pos0` -> `powR0`
+  + `power_posr1` -> `powRr1`
+  + `power_posr0` -> `powRr0`
+  + `power_pos1` -> `powR1`
+  + `ler_power_pos` -> `ler_powR`
+  + `gt0_ler_power_pos` -> `gt0_ler_powR`
+  + `power_posM` -> `powRM`
+  + `power_posrM` -> `powRrM`
+  + `power_posAC` -> `powRAC`
+  + `power_posD` -> `powRD`
+  + `power_posN` -> `powRN`
+  + `power_posB` -> `powRB`
+  + `power_pos_mulrn` -> `powR_mulrn`
+  + `power_pos_inv1` -> `powR_inv1`
+  + `power_pos_intmul` -> `powR_intmul`
+  + `ln_power_pos` -> `ln_powR`
+  + `power12_sqrt` -> `powR12_sqrt`
+  + `norm_power_pos` -> `norm_powR`
+  + `lt0_norm_power_pos` -> `lt0_norm_powR`
+
+- in `lebesgue_measure.v`:
+  + `measurable_power_pos` -> `measurable_powR`
+
+- in `exp.v`:
+  + `powere_pos` -> `poweR`
+  + `powere_pos_EFin` -> `poweR_EFin`
+  + `powere_posyr` -> `poweRyr`
+  + `powere_pose0` -> `poweRe0`
+  + `powere_pose1` -> `poweRe1`
+  + `powere_posNyr` -> `poweRNyr`
+  + `powere_pos0r` -> `poweR0r`
+  + `powere_pos1r` -> `poweR1r`
+  + `fine_powere_pos` -> `fine_poweR`
+  + `powere_pos_ge0` -> `poweR_ge0`
+  + `powere_pos_gt0` -> `poweR_gt0`
+  + `powere_posM` -> `poweRM`
+  + `powere12_sqrt` -> `poweR12_sqrt`
+
 ### Generalized
 
 - in `exp.v`:
-  + lemmas `convex_expR`, `ler_power_pos`
+  + lemmas `convex_expR`, `ler_power_pos` (now `ler_powR`)
 - in `exp.v`:
-  + lemma `ln_power_pos`
+  + lemma `ln_power_pos` (now `ln_powR`)
 
 ### Deprecated
 

classical/all_classical.v

@@ -1,7 +1,7 @@
-From mathcomp.classical Require Export boolp.
-From mathcomp.classical Require Export classical_sets.
-From mathcomp.classical Require Export mathcomp_extra.
-From mathcomp.classical Require Export functions.
-From mathcomp.classical Require Export cardinality.
-From mathcomp.classical Require Export fsbigop.
-From mathcomp.classical Require Export set_interval.
+From mathcomp Require Export boolp.
+From mathcomp Require Export classical_sets.
+From mathcomp Require Export mathcomp_extra.
+From mathcomp Require Export functions.
+From mathcomp Require Export cardinality.
+From mathcomp Require Export fsbigop.
+From mathcomp Require Export set_interval.

classical/cardinality.v

@@ -1,8 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 
 (******************************************************************************)
 (*                              Cardinality                                   *)

classical/classical_sets.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
 From mathcomp Require Import ssrint interval.
-From mathcomp.classical Require Import mathcomp_extra boolp.
+From mathcomp Require Import mathcomp_extra boolp.
 
 (******************************************************************************)
 (* This file develops a basic theory of sets and types equipped with a        *)

classical/fsbigop.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
 
 (******************************************************************************)
 (*                     Finitely-supported big operators                       *)

classical/functions.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".

classical/set_interval.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
-From mathcomp.classical Require Import functions.
+From mathcomp Require Import functions.
 
 (******************************************************************************)
 (* This files contains lemmas about sets and intervals.                       *)

theories/Rstruct.v

@@ -372,7 +372,7 @@ Canonical R_rcfType := RcfType R Rreal_closed_axiom.
 End ssreal_struct.
 
 Local Open Scope ring_scope.
-From mathcomp.classical Require Import boolp classical_sets.
+From mathcomp Require Import boolp classical_sets.
 Require Import reals.
 
 Section ssreal_struct_contd.

theories/charge.v

@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets cardinality.
-From mathcomp.classical Require Import mathcomp_extra functions fsbigop.
-From mathcomp.classical Require Import set_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality.
+From mathcomp Require Import functions fsbigop set_interval.
 From HB Require Import structures.
 Require Import reals ereal signed topology numfun normedtype sequences.
 Require Import esum measure realfun lebesgue_measure lebesgue_integral.

theories/constructive_ereal.v

@@ -10,7 +10,7 @@
    incorporate it into mathcomp proper where it could then be used for
    bounds of intervals*)
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra.
 Require Import signed.
 
 (******************************************************************************)

theories/convex.v

@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets set_interval.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
-Require Import ereal reals signed topology prodnormedzmodule.
-Require Import normedtype derive realfun itv.
+From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
+From mathcomp Require Import functions cardinality.
+Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
+Require Import realfun itv.
 From HB Require Import structures.
 
 (******************************************************************************)

theories/derive.v

@@ -1,7 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
 
 (******************************************************************************)

theories/ereal.v

@@ -6,8 +6,8 @@
 (* -------------------------------------------------------------------- *)
 
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import boolp classical_sets functions fsbigop.
-From mathcomp.classical Require Import cardinality set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import fsbigop cardinality set_interval.
 Require Import reals signed topology.
 Require Export constructive_ereal.
 

theories/esum.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology sequences normedtype numfun.
 
 (******************************************************************************)