natural logarithm for the extended reals and some simple lemmas

CHANGELOG.md

@@ -43,9 +43,15 @@ Latest releases: [[1.11.0] - 2025-05-02](#1110---2025-05-02), [[1.10.0] - 2025-0
   + lemma `cvge_ninftyP`
 
 - in `exp.v`:
-  + lemma `poweRE`
-  + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1`
-  + Instance `is_derive1_powR`
+  + lemma `norm_expR`
+  + lemmas `expeR_eqy`
+  + lemmas `lt0_ln`
+  + lemmas `lt0_powR`, `powR_eq1`
+  + Section `Lne`
+  + definition `lne`
+  + lemmas `lne0`, `lner`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`, 
+    `lne_inj`, `lneV`, `lne_div`, `ltr_lne`, `ler_lne`, `lneXn`, `le_lne1Dx`, 
+    `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `lne_le0_le0`
 
 - in `measure.v`:
   + lemmas `mnormalize_id`, `measurable_fun_eqP`

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

reals/reals.v

@@ -38,7 +38,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Corelib Require Import Setoid.
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.

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   *)
@@ -535,7 +536,7 @@ case: (lerP 1 x) => [/expR_total_gt1[y [_ _ Hy]]|x_lt1 x_gt0].
 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).
@@ -616,7 +617,7 @@ 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 => //= [r|]. Qed. 
 Lemma expeRD x y : expeR (x + y) = expeR x * expeR y.
 Proof.
 case: x => /= [r| |]; last by rewrite mul0e.
@@ -765,7 +766,7 @@ Proof.
 have [x0|x0 x1] := leP x 0; first by rewrite ln0.
 by rewrite -ler_expR expR0 lnK.
 Qed.
-
+Lemma lt0_ln (x : R) : x < 0 -> ln x = 0. Proof. move=> x0; rewrite /ln/= getPN//= => y /eqP eqx; by move: x0; rewrite -eqx le_gtF// expR_ge0. Qed.
 Lemma continuous_ln x : 0 < x -> {for x, continuous ln}.
 Proof.
 move=> x_gt0; rewrite -[x]lnK//.
@@ -1105,9 +1106,136 @@ move=> x_gt0; split.
 by rewrite -derive1E powR_derive1// in_itv andbT.
 Qed.
 
+Lemma lt0_powR {x} {p} : (x < 0)%R -> x `^ p = 1.
+Proof.
+move => lts0; rewrite /powR; case : ifP => /eqP eqs0.
+- by rewrite eqs0 in lts0; move : lts0; rewrite ltxx.
+- move : lts0; rewrite lt_def => /andP [? les0].
+  by rewrite (ln0 les0) 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 eq_refl.
+have [-> | p0] := eqVneq p 0; rewrite ?powRr0 ? eq_refl orbC //=.
+case : (ltgtP x 0) => [x0 | x0 | ->]; first by rewrite (lt0_powR x0) eq_refl.
+  + rewrite /powR [X in if X then _ else _]eq_sym (lt_eqF x0).
+    rewrite -expR0; apply /negP => /eqP /expR_inj /eqP.
+    rewrite mulf_eq0 (negbTE p0) -ln1 //= => /eqP /(ln_inj x0 ltr01) /eqP.
+    by rewrite (negbTE x1).
+  + 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.
+
+  Local Open Scope ereal_scope.
+
+  Definition lne x := 
+  match x with
+  | x'%:E => if x' == 0%R then -oo else (ln x')%:E
+  | +oo => +oo
+  | -oo => 0 
+  end.
+
+  Lemma lne0 x : x < 0 -> lne x = 0.
+  Proof.
+  by move: x => [x||]//=; rewrite lte_fin => ?; rewrite lt_eqF ?ln0 ?ltW.
+  Qed.
+
+  Lemma lner r : (r != 0)%R -> lne (r%:E) = (ln r)%:E.
+  Proof. by move => /negbTE //= ->. Qed.
+
+  Lemma expeRK : cancel expeR lne.
+  Proof. by case=> //=[x|]; rewrite ?eqxx ?gt_eqF ?expR_gt0 ?expRK. Qed.
+
+  (*x  \is Num.pos -> exp (ln x) = x*)
+  Lemma lneK x : 0 < x ->  expeR (lne x) = x.
+  (* {in Num.pos, cancel lne (@expeR R)}.*)
+  Proof.
+  case : x => [r|//|]; last by rewrite ltNge leNye.
+  by rewrite /expeR/lne; case: ifPn => [/eqP ->|_ ?]; rewrite ?lnK.
+  Qed.
+
+  Lemma lneK_eq x : (expeR (lne x) == x) = (0 <= x).
+  Proof.
+  case: x => //=[r|]; last by rewrite eqxx leey.
+  case: ifPn => /=[/eqP->|r0]; first by rewrite eqxx lexx.
+  by rewrite eqe lnK_eq lee_fin lt_neqAle eq_sym r0.
+  Qed.  
+
+  Lemma lne1 : lne 1 = 0.
+  Proof. by rewrite lner //= ln1. Qed.  
+
+  Lemma lneM x y : 0 < x -> 0 < y -> lne (x * y) = (lne x + lne y).
+  Proof. 
+  by move => x0 y0; apply expeR_inj; rewrite expeRD !lneK// mule_gt0.
+  Qed. 
+
+  Lemma lne_inj x y : 0 < x -> 0 < y -> lne x = lne y -> x = y.
+  Proof. by move=> /lneK {2}<- /lneK {2}<- ->. Qed. 
+
+  Lemma lneV (r : R) : (0 < r)%R -> lne (r%R^-1)%:E = - lne (r%:E).
+  Proof. by move=> r0; rewrite !lner ?gt_eqF ?invr_gt0// lnV. Qed.
+
+  Lemma lne_div x y : 
+    0 < x -> 0 < y -> lne (x * (fine y)^-1%:E) = lne x - lne y.
+  Proof.
+  case: x => //[x|]; case: y => //[y|]; rewrite ?lte_fin => a0 b0/=.
+  - by rewrite !ifF ?gt_eqF ?divr_gt0// ln_div.
+  - by rewrite ifT ?invr0 ?mulr0// addeNy.
+  - by rewrite ifF ?gt0_mulye ?lte_fin ?invr_gt0// gt_eqF.
+  - by rewrite invr0 mule0/= eqxx addeNy.
+  Qed.  
+
+  Lemma ltr_lne x y : 0 < x -> 0 < y -> (lne x < lne y) = (x < y).
+  Proof. by move => x_gt0 y_gt0; rewrite -ltr_expeR !lneK. Qed. 
+
+  Lemma ler_lne x y :  0 < x -> 0 < y -> (lne x <= lne y) = (x <= y).
+  Proof. by move=> x_gt0 y_gt0; rewrite -ler_expeR !lneK. Qed.
+
+  Lemma lneXn n x : 0 < x -> lne (x ^+ n) = lne x *+ n.
+  Proof.
+  case: n => [/=|]; first by rewrite ifF ?ln1// gt_eqF.
+  case: x => //[r|] n; rewrite ?lte_fin => x0.
+  - by rewrite -EFin_expe /lne !gt_eqF// -?EFin_natmul ?exprn_gt0// lnXn.
+  - case: n => //n; rewrite expeS gt0_mulye ?expe_gt0// ?enatmul_pinfty.
+  - by case: n => //n; rewrite expeS gt0_mulye ?expe_gt0// ?enatmul_pinfty.
+  Qed.
+
+  Lemma le_lne1Dx x : -(1) < x -> lne (1 + x) <= x.
+  Proof.
+  by move=> ?; rewrite -ler_expeR lneK ?expeR_ge1Dx// addrC -(oppeK 1) sube_gt0.
+  Qed.
+
+  Lemma lne_sublinear x : 0 < x < +oo -> lne x < x.
+  Proof.
+  by case: x => [?||] /andP [? _]//; rewrite /lne gt_eqF// lte_fin ln_sublinear.
+  Qed.
+
+  Lemma lne_ge0 x : 1 <= x -> 0 <= lne x.
+  Proof.
+  case: x => [r rge1||]//; rewrite /lne//.
+  by rewrite gt_eqF ?(lt_le_trans ltr01)// lee_fin// ln_ge0.
+  Qed.
+
+  Lemma lne_lt0 x : 0 < x < 1 -> lne x < 0.
+  Proof.
+  by move => /andP [x_gt0 x_lt1]; rewrite -ltr_expeR expeR0 lneK.
+  Qed.
+
+  Lemma lne_gt0 x : 1 < x -> 0 < lne x.
+  Proof. by move=> x_gt1; rewrite -ltr_expeR expeR0 lneK// (lt_trans _ x_gt1). Qed.
+
+  Fact lne_le0_le0 x : x <= 1 -> lne x <= 0.
+  Proof. by move: x => [r||]//?; rewrite /lne; case: ifPn => //?; exact: ln_le0. Qed.
+
+End Lne.
+
 Section poweR.
 Local Open Scope ereal_scope.
 Context {R : realType}.
@@ -1324,4 +1452,4 @@ move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))).
 by move/contra_not; apply; exact: dvg_harmonic.
 Qed.
 
-End riemannR_series.
+End riemannR_series.