natural logarithme for extended real numbers

CHANGELOG.md

@@ -8031,5 +8031,3 @@ All norms and absolute values have been unified, both in their denotation `|_| a
 - NIX support
   + see `config.nix`, `default.nix`
   + for the CI also
-
-### Misc

CHANGELOG_UNRELEASED.md

@@ -86,6 +86,18 @@
            `le0_nondecreasing_set_nonincreasing_integral`,
 	   `le0_nondecreasing_set_cvg_integral`
 
+- in `exp.v`:
+  + lemma `norm_expR`
+  + lemmas `expeR_eqy`
+  + lemmas `lt0_powR1`, `powR_eq1`
+  + definition `lne`
+  + lemmas `le0_lneNy`, `lne_EFin`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`, 
+    `lne_inj`, `lneV`, `lne_div`, `lte_lne`, `lee_lne`, `lneXn`, `le_lne1Dx`, 
+    `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `le1_lne_le0`
+
+- in `constructive_ereal.v`:
+  + lemma `expe0`, `mule0n`, `muleS`
+
 ### Changed
 
 - in `convex.v`:

reals/constructive_ereal.v

@@ -726,8 +726,12 @@ Proof. by elim: n => //= n ->. Qed.
 Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
 Proof. by elim: n => //= n ->. Qed.
 
+Lemma mule0n x : x *+ 0 = 0. Proof. by []. Qed.
+
 Lemma mule2n x : x *+ 2 = x + x. Proof. by []. Qed.
 
+Lemma expe0 x : x ^+ 0 = 1. Proof. by []. Qed.
+
 Lemma expe2 x : x ^+ 2 = x * x. Proof. by []. Qed.
 
 Lemma leeN2 : {mono @oppe R : x y /~ x <= y}.
@@ -862,6 +866,9 @@ Lemma addeC : commutative (S := \bar R) +%E. Proof. exact: addrC. Qed.
 
 Lemma adde0 : right_id (0 : \bar R) +%E. Proof. exact: addr0. Qed.
 
+Lemma muleS x n : x *+ n.+1 = x + x *+ n.
+Proof. by case: n => //=; rewrite adde0. Qed.
+
 Lemma add0e : left_id (0 : \bar R) +%E. Proof. exact: add0r. Qed.
 
 Lemma addeA : associative (S := \bar R) +%E. Proof. exact: addrA. Qed.

theories/exp.v

@@ -21,7 +21,8 @@ From mathcomp Require Import realfun interval_inference convex.
 (*   pseries_diffs f i == (i + 1) * f (i + 1)                                 *)
 (*                                                                            *)
 (*             expeR x == extended real number-valued exponential function    *)
-(*                ln x == the natural logarithm                               *)
+(*                ln x == the natural logarithm, in ring_scope                *)
+(*                lne x == the natural logarithm, in ereal_scope              *)
 (*              s `^ r == power function, in ring_scope (assumes s >= 0)      *)
 (*              e `^ r == power function, in ereal_scope (assumes e >= 0)     *)
 (*          riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type   *)
@@ -468,7 +469,7 @@ Proof. by rewrite expRD expRN. Qed.
 Lemma ltr_expR : {mono (@expR R) : x y / x < y}.
 Proof.
 move=> x y.
-by  rewrite -[in LHS](subrK x y) expRD ltr_pMl ?expR_gt0 // expR_gt1 subr_gt0.
+by rewrite -[in LHS](subrK x y) expRD ltr_pMl ?expR_gt0 // expR_gt1 subr_gt0.
 Qed.
 
 Lemma ler_expR : {mono (@expR R) : x y / x <= y}.
@@ -547,6 +548,9 @@ have /expR_total_gt1[y [H1y H2y H3y]] : 1 <= x^-1 by rewrite ltW // !invf_cp1.
 by exists (-y); rewrite expRN H3y invrK.
 Qed.
 
+Lemma norm_expR : normr \o expR = (expR : R -> R).
+Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.
+
 Local Open Scope convex_scope.
 Lemma convex_expR (t : {i01 R}) (a b : R^o) :
   expR (a <| t |> b) <= (expR a : R^o) <| t |> (expR b : R^o).
@@ -604,7 +608,6 @@ Canonical expR_inum (i : Itv.t) (x : Itv.def (@Itv.num_sem R) i) :=
   Itv.mk (num_spec_expR x).
 
 End expR.
-
 #[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRM_natl`")]
 Notation expRMm := expRM_natl (only parsing).
 
@@ -628,6 +631,9 @@ Proof. by case: x => //= r; rewrite lte_fin expR_gt0. Qed.
 Lemma expeR_eq0 x : (expeR x == 0) = (x == -oo).
 Proof. by case: x => //= [r|]; rewrite ?eqxx// eqe expR_eq0. Qed.
 
+Lemma expeR_eqy x : (expeR x == +oo) = (x == +oo).
+Proof. by case: x. Qed.
+
 Lemma expeRD x y : expeR (x + y) = expeR x * expeR y.
 Proof.
 case: x => /= [r| |]; last by rewrite mul0e.
@@ -645,15 +651,15 @@ case : x => //= [r|]; last by rewrite addeNy.
 by rewrite -EFinD !lee_fin; exact: expR_ge1Dx.
 Qed.
 
-Lemma ltr_expeR : {mono expeR : x y / x < y}.
+Lemma lte_expeR : {mono expeR : x y / x < y}.
 Proof.
 move=> [r| |] [s| |]//=; rewrite ?ltry//.
 - by rewrite !lte_fin ltr_expR.
 - by rewrite !ltNge lee_fin expR_ge0 leNye.
 - by rewrite lte_fin expR_gt0 ltNye.
 Qed.
 
-Lemma ler_expeR : {mono expeR : x y / x <= y}.
+Lemma lee_expeR : {mono expeR : x y / x <= y}.
 Proof.
 move=> [r| |] [s| |]//=; rewrite ?leey ?lexx//.
 - by rewrite !lee_fin ler_expR.
@@ -677,6 +683,10 @@ by rewrite lte_fin => /expR_total[y <-]; exists y%:E.
 Qed.
 
 End expeR.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed `lte_expeR`")]
+Notation ltr_expeR := lte_expeR (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed `lee_expeR`")]
+Notation ler_expeR := lee_expeR (only parsing).
 
 Section Ln.
 Variable R : realType.
@@ -771,7 +781,7 @@ Proof.
 by move=> x_gt1; rewrite -ltr_expR expR0 lnK // qualifE/= (lt_trans _ x_gt1).
 Qed.
 
-Lemma ln_le0 (x : R) : x <= 1 -> ln x <= 0.
+Lemma ln_le0 x : x <= 1 -> ln x <= 0.
 Proof.
 have [x0|x0 x1] := leP x 0; first by rewrite ln0.
 by rewrite -ler_expR expR0 lnK.
@@ -1118,9 +1128,134 @@ move=> x_gt0; split.
 by rewrite -derive1E powR_derive1// in_itv andbT.
 Qed.
 
+Lemma lt0_powR1 x p : x < 0 -> x `^ p = 1.
+Proof.
+by move=> x0; rewrite /powR lt_eqF// (ln0 (ltW x0)) mulr0 expR0.
+Qed.
+
+Lemma powR_eq1 x p : (x `^ p == 1) = [|| (x == 1), (x < 0) | (p == 0)].
+Proof.
+have [->/=|x1] := eqVneq x 1; first by rewrite powR1 eqxx.
+have [->|p0]/= := eqVneq p 0; first by rewrite powRr0 eqxx orbT.
+have [x0|x0|->]/= := ltgtP x 0; first by rewrite lt0_powR1// eqxx.
+- rewrite /powR (gt_eqF x0)// -expR0; apply/negP => /eqP/expR_inj/eqP.
+  rewrite mulf_eq0 (negbTE p0)/= -ln1 => /eqP/ln_inj => /(_ _ _)/eqP.
+  by rewrite (negbTE x1) falseE; apply => //; rewrite posrE.
+- by rewrite powR0// eq_sym oner_eq0.
+Qed.
+
 End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.
 
+Section Lne.
+Variable R : realType.
+Implicit Types (x : \bar R) (r : R).
+Local Open Scope ereal_scope.
+
+Definition lne x :=
+  match x with
+  | r%:E => if (r <= 0)%R then -oo else (ln r)%:E
+  | +oo => +oo
+  | -oo => -oo
+  end.
+
+Lemma le0_lneNy x : x <= 0 -> lne x = -oo.
+Proof.
+by move: x => [r| |]//=; case: ifPn => //; rewrite lee_fin => /negbTE ->.
+Qed.
+
+Lemma lne_EFin r : (0 < r)%R -> lne (r%:E) = (ln r)%:E.
+Proof. by move=> /=; case: ifPn => //; rewrite leNgt => /negbTE ->. Qed.
+
+Lemma expeRK : cancel expeR lne.
+Proof. by case=> //=[x|]; rewrite ?lexx// leNgt expR_gt0/= expRK. Qed.
+
+Lemma lneK : {in `[0, +oo], cancel lne (@expeR R)}.
+Proof.
+move=> [r|//|//]; rewrite in_itv => //= /andP[]; rewrite lee_fin.
+by rewrite le_eqVlt => /predU1P[<- _|r0 _]; rewrite ?lexx// leNgt r0/= lnK.
+Qed.
+
+Lemma lneK_eq x : (expeR (lne x) == x) = (0 <= x).
+Proof.
+move: x => [r| |]//=; last by rewrite eqxx leey.
+case: ifPn => [r0|]/=; first by rewrite eq_le !lee_fin r0 andbT.
+by rewrite -ltNge => r0; rewrite eqe lnK_eq lee_fin le_eqVlt r0 orbT.
+Qed.
+
+Lemma lne1 : lne 1 = 0. Proof. by rewrite lne_EFin//= ln1. Qed.
+
+Lemma lneM : {in `]0, +oo] &, {morph lne : x y / x * y >-> x + y}}.
+Proof.
+move=> x y /[!in_itv]/= /[!@leey R]/= /[!andbT] x0 y0.
+by apply: expeR_inj; rewrite expeRD !lneK// in_itv/= leey ltW ?mule_gt0.
+Qed.
+
+Lemma lne_inj : {in `[0, +oo] &, injective lne}.
+Proof. by move=> x y /lneK {2}<- /lneK {2}<- ->. Qed.
+
+Lemma lneV r : (0 < r)%R -> lne r^-1%:E = - lne (r%:E).
+Proof. by move=> r0; rewrite !lne_EFin ?gt_eqF ?invr_gt0// lnV. Qed.
+
+Lemma lne_div : {in `]0, +oo] &, {morph lne : x y / x / y >-> x - y}}.
+Proof.
+move=> [x| |] [y| |]//; rewrite !in_itv/= !leey !andbT ?lte_fin => x0 y0.
+- rewrite inver// !gt_eqF//= pmulr_rle0// invr_le0 leNgt y0/=.
+  by rewrite leNgt x0/= ln_div.
+- by rewrite mulr0 lexx leNgt x0/=.
+- by rewrite inver !gt_eqF// leNgt y0/= gt0_mulye// lte_fin invr_gt0.
+- by rewrite invey mule0/= lexx.
+Qed.
+
+Lemma lte_lne : {in `[0, +oo] &, {mono lne : x y / x < y}}.
+Proof. by move => x y x0 y0; rewrite -lte_expeR !lneK. Qed.
+
+Lemma lee_lne : {in `[0, +oo] &, {mono lne : x y / x <= y}}.
+Proof. by move=> x y x_gt0 y_gt0; rewrite -lee_expeR !lneK. Qed.
+
+Lemma lneXn n x : 0 < x -> lne (x ^+ n) = lne x *+ n.
+Proof.
+elim: n x => [x x0|n ih x x0]; first by rewrite expe0 mule0n lne1.
+by rewrite expeS lneM ?ih ?muleS// in_itv/= ?expe_gt0// ?x0/= leey.
+Qed.
+
+Lemma le_lne1Dx x : - 1%E <= x -> lne (1 + x) <= x.
+Proof.
+move=> ?; rewrite -lee_expeR lneK ?expeR_ge1Dx //.
+by rewrite in_itv //= leey andbT addrC -(oppeK 1) sube_ge0.
+Qed.
+
+Lemma lne_sublinear x : 0 < x < +oo -> lne x < x.
+Proof.
+case: x => [r| |]//; rewrite ?ltxx ?andbF// lte_fin => /andP[r0 _].
+by rewrite lne_EFin// lte_fin ln_sublinear.
+Qed.
+
+Lemma lne_ge0 x : 1 <= x -> 0 <= lne x.
+Proof.
+case: x => [r||]//; rewrite ?leey// lee_fin => r1.
+by rewrite lne_EFin// ?(lt_le_trans _ r1)// lee_fin ln_ge0.
+Qed.
+
+Lemma lne_lt0 x : 0 < x < 1 -> lne x < 0.
+Proof.
+by move=> /andP[? ?]; rewrite -lte_expeR expeR0 lneK ?in_itv//= leey andbT ?ltW.
+Qed.
+
+Lemma lne_gt0 x : 1 < x -> 0 < lne x.
+Proof.
+move=> x1; rewrite -lte_expeR expeR0 lneK// in_itv/= leey andbT.
+by rewrite (le_trans _ (ltW x1)).
+Qed.
+
+Fact le1_lne_le0 x : x <= 1 -> lne x <= 0.
+Proof.
+move: x => [r r1| |]//=.
+by rewrite /lne; case: ifPn => // r0; rewrite lee_fin ln_le0.
+Qed.
+
+End Lne.
+
 Section poweR.
 Local Open Scope ereal_scope.
 Context {R : realType}.