diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d197de96c..2f9f22edf 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -70,6 +70,10 @@ - in `measure.v`: + definition `ess_sup`, lemma `ess_sup_ge0` +- in `exp.v`: + + lemma `gt0_ltr_powR` + + lemma `powR_injective` + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized @@ -91,6 +95,8 @@ - in `measure.v`: + implicits of `measurable_fst` and `measurable_snd` +- in `exp.v`: + + `gt0_ler_powR` now uses `Num.nneg` ### Renamed @@ -101,6 +107,9 @@ + `lee_opp` -> `leeN2` + `lte_opp` -> `lteN2` +- in `exp.v`: + + `gt0_ler_powR` -> `ge0_ler_powR` + ### Generalized ### Deprecated diff --git a/theories/exp.v b/theories/exp.v index 4ed2fffee..e5ac2a6c4 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -664,11 +664,20 @@ move=> a1 x y xy. by rewrite /powR gt_eqF ?(lt_le_trans _ a1)// ler_expR ler_wpmul2r ?ln_ge0. Qed. -Lemma gt0_ler_powR (r : R) : 0 <= r -> - {in `[0, +oo[ &, {homo powR ^~ r : x y / x <= y >-> x <= y}}. +Lemma powR_injective r : 0 < r -> {in Num.nneg &, injective (powR ^~ r)}. +Proof. +move=> r0 x y x0 y0; rewrite /powR; case: ifPn => [/eqP ->|xneq0]. + by case: ifPn => [/eqP ->//|_ /eqP]; rewrite (gt_eqF r0) eq_sym expR_eq0. +case: ifPn => [/eqP -> /eqP|yneq0]; first by rewrite (gt_eqF r0) expR_eq0. +by move/expR_inj/mulfI => /(_ (negbT (gt_eqF r0))); apply: ln_inj; + rewrite posrE lt_neqAle eq_sym (xneq0,yneq0). +Qed. + +Lemma ge0_ler_powR (r : R) : 0 <= r -> + {in Num.nneg &, {homo powR ^~ r : x y / x <= y >-> x <= y}}. Proof. rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !powRr0. -move=> a0 x y; rewrite !in_itv/= !andbT !le_eqVlt => /predU1P[<-|x0]. +move=> a0 x y; rewrite 2!nnegrE !le_eqVlt => /predU1P[<-|x0]. move=> /predU1P[<- _|y0 _]; first by rewrite eqxx. by rewrite !powR0 ?(gt_eqF a0)// powR_gt0 ?orbT. move=> /predU1P[<-|y0]; first by rewrite gt_eqF//= ltNge (ltW x0). @@ -676,6 +685,14 @@ 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 Num.nneg &, {homo powR ^~ r : x y / x < y >-> x < y}}. +Proof. +move=> r0 x y x0 y0 xy; have := ge0_ler_powR (ltW r0) x0 y0 (ltW xy). +rewrite le_eqVlt => /orP[/eqP/(powR_injective r0 x0 y0)/eqP|//]. +by rewrite lt_eqF. +Qed. + Lemma powRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r. Proof. rewrite /powR mulf_eq0. @@ -786,6 +803,9 @@ Qed. End PowR. Notation "a `^ x" := (powR a x) : ring_scope. +#[deprecated(since="mathcomp-analysis 0.6.5", note="renamed `ge0_ler_powR`")] +Notation gt0_ler_powR := ge0_ler_powR. + Section poweR. Local Open Scope ereal_scope. Context {R : realType}.