natural logarithm for the extended reals and some simple lemmas

CHANGELOG.md

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

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,17 @@
 
 ### Added
 
+- in `exp.v`:
+  + lemma `norm_expR`
+  + lemmas `expeR_eqy`
+  + lemmas `lt0_ln`
+  + lemmas `lt0_powR`, `powR_eq1`
+  + Section `Lne`
+  + definition `lne`
+  + lemmas `lne0`, `lne_EFin`, `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`
+
 ### Changed
 
 - in `sequences.v`:

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   *)
@@ -536,6 +537,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).
@@ -617,6 +621,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 => //= [r|]. Qed. 
+
 Lemma expeRD x y : expeR (x + y) = expeR x * expeR y.
 Proof.
 case: x => /= [r| |]; last by rewrite mul0e.
@@ -766,6 +773,12 @@ 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 +1118,141 @@ 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 lne_EFin 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.
+
+
+Lemma lneK : {in `[0, +oo], cancel lne (@expeR R)}.
+Proof.
+move=> //= x; case : x => [r|//|//]; rewrite in_itv => //= /andP [le0r _].
+by case: ifPn => [/eqP -> //=|r0]; rewrite /expeR ?lnK //= posrE lt_def r0.
+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 lne_EFin //= ln1. Qed.  
+
+Lemma lneM x y : 0 < x -> 0 < y -> lne (x * y) = (lne x + lne y).
+Proof. 
+by move=> ? ?;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 : R) : (0 < r)%R -> lne (r%R^-1)%:E = - lne (r%:E).
+Proof. by move=> r0; rewrite !lne_EFin ?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 : {in `[0, +oo]&, {mono lne : x y / x < y}}.
+Proof. by move => x y x_gt0 y_gt0; rewrite -ltr_expeR !lneK. Qed. 
+
+Lemma ler_lne :  {in `[0, +oo]&, {mono lne : x y / x <= y}}.
+Proof. by move=> x y 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%E <= x -> lne (1 + x) <= x.
+Proof.
+move=> ?; rewrite -ler_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.
+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.
+move => /andP [x_gt0 x_lt1]; rewrite -ltr_expeR expeR0 lneK ?in_itv //= !ltW //.
+by apply /(lt_trans x_lt1) /ltry.
+Qed.
+
+Lemma lne_gt0 x : 1 < x -> 0 < lne x.
+Proof. 
+move=> x_gt1; rewrite -ltr_expeR expeR0 lneK// ?(lt_trans _ x_gt1) in_itv //=.
+by rewrite leey andbT; apply /(le_trans lee01) /ltW. 
+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 +1469,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.