rename powere_pos

CHANGELOG_UNRELEASED.md

@@ -31,8 +31,8 @@
   + lemmas `powRrM`, `gt0_ler_powR`,
     `gt0_powR`, `norm_powR`, `lt0_norm_powR`,
     `powRB`
-  + lemmas `powere_posrM`, `powere_posAC`, `gt0_powere_pos`,
-    `powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`, `powere_posB`
+  + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`,
+    `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB`
 
 - in `mathcomp_extra.v`:
   + definition `min_fun`, notation `\min`
@@ -44,9 +44,9 @@
 - in `exp.v`:
   + notation `` e `^?(r +? s) ``
   + lemmas `expR_eq0`, `powRN`
-  + definition `powere_posD_def`
-  + lemmas `powere_posD_defE`, `powere_posB_defE`, `add_neq0_powere_posD_def`,
-    `add_neq0_powere_posB_def`, `nneg_neq0_powere_posD_def`, `nneg_neq0_powere_posB_def`
+  + definition `poweRD_def`
+  + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`,
+    `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def`
 
 ### Changed
 
@@ -57,7 +57,7 @@
 - moved from `functions.v` to `classical_sets.v`: `subsetP`.
 
 - in `exp.v`:
-  + lemmas `power_pos_eq0` (now `powR_eq0`), `powere_pos_eq0`
+  + lemmas `power_pos_eq0` (now `powR_eq0`), `powere_pos_eq0` (now `poweR_eq0`)
   + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`)
 
 ### Renamed
@@ -72,7 +72,7 @@
 - in `exp.v`:
   + `power_pos_eq0` -> `powR_eq0_eq0`
   + `power_pos_inv` -> `powR_invn`
-  + `powere_pos_eq0` -> `powere_pos_eq0_eq0`
+  + `powere_pos_eq0` -> `poweR_eq0_eq0`
 
 - in `exp.v`:
   + `power_pos` -> `powR`
@@ -104,6 +104,22 @@
 - 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_pos_eq0` -> `poweR_eq0`
+  + `powere_posM` -> `poweRM`
+  + `powere12_sqrt` -> `poweR12_sqrt`
+
 ### Generalized
 
 - in `exp.v`:

theories/exp.v

@@ -755,158 +755,156 @@ Qed.
 End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.
 
-Section powere_pos.
+Section poweR.
 Local Open Scope ereal_scope.
 Context {R : realType}.
 Implicit Types (s r : R) (x y : \bar R).
 
-Definition powere_pos x r :=
+Definition poweR x r :=
   match x with
   | x'%:E => (x' `^ r)%:E
   | +oo => if r == 0%R then 1%E else +oo
   | -oo => if r == 0%R then 1%E else 0%E
   end.
 
-Local Notation "x `^ r" := (powere_pos x r).
+Local Notation "x `^ r" := (poweR x r).
 
-Lemma powere_pos_EFin s r : s%:E `^ r = (s `^ r)%:E.
+Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E.
 Proof. by []. Qed.
 
-Lemma powere_posyr r : r != 0%R -> +oo `^ r = +oo.
+Lemma poweRyr r : r != 0%R -> +oo `^ r = +oo.
 Proof. by move/negbTE => /= ->. Qed.
 
-Lemma powere_pose0 x : x `^ 0 = 1.
+Lemma poweRe0 x : x `^ 0 = 1.
 Proof. by move: x => [x'| |]/=; rewrite ?powRr0// eqxx. Qed.
 
-Lemma powere_pose1 x : 0 <= x -> x `^ 1 = x.
+Lemma poweRe1 x : 0 <= x -> x `^ 1 = x.
 Proof.
 by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)).
 Qed.
 
-Lemma powere_posNyr r : r != 0%R -> -oo `^ r = 0.
+Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.
 Proof. by move=> r0 /=; rewrite (negbTE r0). Qed.
 
-Lemma powere_pos_eqy x r : x `^ r = +oo -> x = +oo.
+Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo.
 Proof. by case: x => [x| |] //=; case: ifP. Qed.
 
-Lemma eqy_powere_pos x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
+Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
 Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed.
 
-Lemma powere_pos0r r : r != 0%R -> 0 `^ r = 0.
-Proof. by move=> r0; rewrite powere_pos_EFin powR0. Qed.
+Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.
+Proof. by move=> r0; rewrite poweR_EFin powR0. Qed.
 
-Lemma powere_pos1r r : 1 `^ r = 1.
-Proof. by rewrite powere_pos_EFin powR1. Qed.
+Lemma poweR1r r : 1 `^ r = 1. Proof. by rewrite poweR_EFin powR1. Qed.
 
-Lemma fine_powere_pos x r : fine (x `^ r) = ((fine x) `^ r)%R.
+Lemma fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R.
 Proof.
 by move: x => [x| |]//=; case: ifPn => [/eqP ->|?]; rewrite ?powRr0 ?powR0.
 Qed.
 
-Lemma powere_pos_ge0 x r : 0 <= x `^ r.
+Lemma poweR_ge0 x r : 0 <= x `^ r.
 Proof. by move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; case: ifPn. Qed.
 
-Lemma powere_pos_gt0 x r : 0 < x -> 0 < x `^ r.
+Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r.
 Proof.
 by move: x => [x|_|]//=; [rewrite lte_fin; exact: powR_gt0|case: ifPn].
 Qed.
 
-Lemma gt0_powere_pos x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.
+Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x.
 Proof.
 move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin.
 exact: gt0_powR.
 Qed.
 
-Lemma powere_pos_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).
+Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)).
 Proof.
-move: x => [x _|_/=|//].
-  by rewrite powere_pos_EFin eqe powR_eq0.
+move: x => [x _|_/=|//]; first by rewrite poweR_EFin eqe powR_eq0.
 by case: ifP => //; rewrite onee_eq0.
 Qed.
 
-Lemma powere_pos_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0.
-Proof. by move=> + /eqP => /powere_pos_eq0-> /andP[/eqP]. Qed.
+Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0.
+Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed.
 
-Lemma powere_posM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
+Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
 Proof.
-have [->|rN0] := eqVneq r 0%R; first by rewrite !powere_pose0 mule1.
+have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1.
 have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r = +oo `^ r * s%:E `^ r.
   case: ltgtP => // [s_gt0 _|<- _]; last first.
-    by rewrite mule0 powere_posyr// !powere_pos0r// mule0.
-  by rewrite gt0_mulye// powere_posyr// gt0_mulye// powere_pos_gt0.
+    by rewrite mule0 poweRyr// !poweR0r// mule0.
+  by rewrite gt0_mulye// poweRyr// gt0_mulye// poweR_gt0.
 case: x y => [x| |] [y| |]// x0 y0; first by rewrite /= -EFinM powRM.
 - by rewrite muleC powyrM// muleC.
 - by rewrite powyrM.
-- by rewrite mulyy !powere_posyr// mulyy.
+- by rewrite mulyy !poweRyr// mulyy.
 Qed.
 
-Lemma powere_posrM x r s : x `^ (r * s) = (x `^ r) `^ s.
+Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s.
 Proof.
-have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 !powere_pose0.
-have [->|r0] := eqVneq r 0%R; first by rewrite mul0r powere_pose0 powere_pos1r.
+have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 !poweRe0.
+have [->|r0] := eqVneq r 0%R; first by rewrite mul0r poweRe0 poweR1r.
 case: x => [x| |]//; first by rewrite /= powRrM.
-  by rewrite !powere_posyr// mulf_neq0.
-by rewrite !powere_posNyr ?powere_pos0r ?(negPf s0)// mulf_neq0.
+  by rewrite !poweRyr// mulf_neq0.
+by rewrite !poweRNyr ?poweR0r ?(negPf s0)// mulf_neq0.
 Qed.
 
-Lemma powere_posAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.
-Proof. by rewrite -!powere_posrM mulrC. Qed.
+Lemma poweRAC x r s : (x `^ r) `^ s = (x `^ s) `^ r.
+Proof. by rewrite -!poweRrM mulrC. Qed.
 
-Definition powere_posD_def x r s := ((r + s == 0)%R ==>
+Definition poweRD_def x r s := ((r + s == 0)%R ==>
   ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
-Notation "x `^?( r +? s )" := (powere_posD_def x r s) : ereal_scope.
+Notation "x `^?( r +? s )" := (poweRD_def x r s) : ereal_scope.
 
-Lemma powere_posD_defE x r s :
+Lemma poweRD_defE x r s :
   x `^?(r +? s) = ((r + s == 0)%R ==>
   ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
 Proof. by []. Qed.
 
-Lemma powere_posB_defE x r s :
+Lemma poweRB_defE x r s :
   x `^?(r +? - s) = ((r == s)%R ==>
   ((x != 0) && ((x \isn't a fin_num) ==> (r == 0%R) && (s == 0%R)))).
-Proof. by rewrite powere_posD_defE subr_eq0 oppr_eq0. Qed.
+Proof. by rewrite poweRD_defE subr_eq0 oppr_eq0. Qed.
 
-Lemma add_neq0_powere_posD_def x r s : (r + s != 0)%R -> x `^?(r +? s).
-Proof. by rewrite powere_posD_defE => /negPf->. Qed.
+Lemma add_neq0_poweRD_def x r s : (r + s != 0)%R -> x `^?(r +? s).
+Proof. by rewrite poweRD_defE => /negPf->. Qed.
 
-Lemma add_neq0_powere_posB_def x r s : (r != s)%R -> x `^?(r +? - s).
-Proof. by rewrite powere_posB_defE => /negPf->. Qed.
+Lemma add_neq0_poweRB_def x r s : (r != s)%R -> x `^?(r +? - s).
+Proof. by rewrite poweRB_defE => /negPf->. Qed.
 
-Lemma nneg_neq0_powere_posD_def x r s : x != 0 -> (r >= 0)%R -> (s >= 0)%R ->
+Lemma nneg_neq0_poweRD_def x r s : x != 0 -> (r >= 0)%R -> (s >= 0)%R ->
   x `^?(r +? s).
 Proof.
-move=> xN0 rge0 sge0; rewrite /powere_posD_def xN0/=.
+move=> xN0 rge0 sge0; rewrite /poweRD_def xN0/=.
 by case: ltgtP rge0 => // [r_gt0|<-]; case: ltgtP sge0 => // [s_gt0|<-]//=;
    rewrite ?addr0 ?add0r ?implybT// gt_eqF//= ?addr_gt0.
 Qed.
 
-Lemma nneg_neq0_powere_posB_def x r s : x != 0 -> (r >= 0)%R -> (s <= 0)%R ->
+Lemma nneg_neq0_poweRB_def x r s : x != 0 -> (r >= 0)%R -> (s <= 0)%R ->
   x `^?(r +? - s).
-Proof. by move=> *; rewrite nneg_neq0_powere_posD_def// oppr_ge0. Qed.
+Proof. by move=> *; rewrite nneg_neq0_poweRD_def// oppr_ge0. Qed.
 
-Lemma powere_posD x r s : x `^?(r +? s) -> x `^ (r + s) = x `^ r * x `^ s.
+Lemma poweRD x r s : x `^?(r +? s) -> x `^ (r + s) = x `^ r * x `^ s.
 Proof.
-rewrite /powere_posD_def.
-have [->|r0]/= := eqVneq r 0%R; first by rewrite add0r powere_pose0 mul1e.
-have [->|s0]/= := eqVneq s 0%R; first by rewrite addr0 powere_pose0 mule1.
+rewrite /poweRD_def.
+have [->|r0]/= := eqVneq r 0%R; first by rewrite add0r poweRe0 mul1e.
+have [->|s0]/= := eqVneq s 0%R; first by rewrite addr0 poweRe0 mule1.
 case: x => // [t|/=|/=]; rewrite ?(negPf r0, negPf s0, implybF); last 2 first.
 - by move=> /negPf->; rewrite mulyy.
 - by move=> /negPf->; rewrite mule0.
-rewrite !powere_pos_EFin eqe => /implyP/(_ _)/andP cnd.
+rewrite !poweR_EFin eqe => /implyP/(_ _)/andP cnd.
 by rewrite powRD//; apply/implyP => /cnd[].
 Qed.
 
-Lemma powere_posB x r s : x `^?(r +? - s) -> x `^ (r - s) = x `^ r * x `^ (- s).
-Proof. by move=> rs; rewrite powere_posD. Qed.
+Lemma poweRB x r s : x `^?(r +? - s) -> x `^ (r - s) = x `^ r * x `^ (- s).
+Proof. by move=> rs; rewrite poweRD. Qed.
 
-Lemma powere12_sqrt x : 0 <= x -> x `^ 2^-1 = sqrte x.
+Lemma poweR12_sqrt x : 0 <= x -> x `^ 2^-1 = sqrte x.
 Proof.
-move: x => [x|_|//]; last by rewrite powere_posyr.
+move: x => [x|_|//]; last by rewrite poweRyr.
 by rewrite lee_fin => x0 /=; rewrite powR12_sqrt.
 Qed.
 
-End powere_pos.
-Notation "a `^ x" := (powere_pos a x) : ereal_scope.
+End poweR.
+Notation "a `^ x" := (poweR a x) : ereal_scope.
 
 Section riemannR_series.
 Variable R : realType.