Lemma gt0_ltr_powR

math-comp · Sep 23, 2023 · 380181e · 380181e
1 parent de6bdd5
commit 380181e
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -70,6 +70,9 @@
 - in `measure.v`:
   + definition `ess_sup`, lemma `ess_sup_ge0`
 
+- in `exp.v`:
+  + lemma `gt0_ltr_powR`
+
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized

diff --git a/theories/exp.v b/theories/exp.v
@@ -676,6 +676,16 @@ move=> /predU1P[->//|xy]; first by rewrite eqxx.
 by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
 Qed.
 
+Lemma gt0_ltr_powR (r : R) : 0 < r ->
+  {in `[0, +oo[ &, {homo powR ^~ r : x y / x < y >-> x < y}}.
+Proof.
+move=> r0 x y; rewrite !in_itv/= !andbT !le_eqVlt => /predU1P[<-|x0].
+  move=> /predU1P[<-|y0 _]; first by rewrite ltxx//.
+  by rewrite powR0 ?(gt_eqF r0)// powR_gt0.
+move=> /predU1P[<-|y0]; first rewrite ltNge ltW//.
+by rewrite /powR !gt_eqF// ltr_expR ltr_pmul2l// ltr_ln.
+Qed.
+
 Lemma powRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
 Proof.
 rewrite /powR mulf_eq0.