gen exp_fun (#876)

* gen exp_fun

- rename to power_pow
- fix doc
- add scope to notation

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>

* add lemma power12_sqrt

* additional lemmas

* change power_pos so that 0^0=1

- so that power_pos and exprn coincide

* measurable_fun exp ln

* fix chaneglog

* add power_pos_intmul proposed by Pierre

* fix changelog

---------

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -70,6 +70,27 @@
   + lemmas `eq_bigmax`, `eq_bigmin` changed to respect `P` in the returned type.
 - in `measure.v`:
   + generalize `negligible` to `semiRingOfSetsType`
+- in `exp.v`:
+  + new lemmas `power_pos_ge0`, `power_pos0`, `power_pos_eq0`,
+    `power_posM`, `power_posAC`, `power12_sqrt`, `power_pos_inv1`,
+    `power_pos_inv`, `power_pos_intmul`
+- in `lebesgue_measure.v`:
+  + lemmas `measurable_fun_ln`, `measurable_fun_power_pos`
+
+### Changed
+
+- in `exp.v`:
+  + generalize `exp_fun` and rename to `power_pos`
+  + `exp_fun_gt0` has now a condition and is renamed to `power_pos_gt0`
+  + remove condition of `exp_funr0` and rename to `power_posr0`
+  + weaken condition of `exp_funr1` and rename to `power_posr1`
+  + weaken condition of `exp_fun_inv` and rename to `power_pos_inv`
+  + `exp_fun1` -> `power_pos1`
+  + rename `ler_exp_fun` to `ler_power_pos`
+  + `exp_funD` -> `power_posD`
+  + weaken condition of `exp_fun_mulrn` and rename to `power_pos_mulrn`
+  + the notation ``` `^ ``` has now scope `real_scope`
+  + weaken condition of `riemannR_gt0` and `dvg_riemannR`
 
 ### Renamed
 

theories/exp.v

@@ -19,7 +19,7 @@ Require Import signed topology normedtype landau sequences derive realfun.
 (*   pseries_diffs f i == (i + 1) * f (i + 1)                                 *)
 (*                                                                            *)
 (*                ln x == the natural logarithm                               *)
-(*              a `^ x == exponential functions                               *)
+(*              a `^ x == power function (assumes a >= 0)                     *)
 (*          riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type   *)
 (*                        of type realType                                    *)
 (*                                                                            *)
@@ -572,68 +572,155 @@ Unshelve. all: by end_near. Qed.
 
 End Ln.
 
-Section ExpFun.
+Section PowerPos.
 Variable R : realType.
 Implicit Types a x : R.
 
-Definition exp_fun a x := expR (x * ln a).
+Definition power_pos a x :=
+  if a == 0 then (x == 0)%:R else expR (x * ln a).
 
-Local Notation "a `^ x" := (exp_fun a x).
+Local Notation "a `^ x" := (power_pos a x).
 
-Lemma exp_fun_gt0 a x : 0 < a `^ x. Proof. by rewrite expR_gt0. Qed.
+Lemma power_pos_ge0 a x : 0 <= a `^ x.
+Proof. by rewrite /power_pos; case: ifPn => // _; exact: expR_ge0. Qed.
 
-Lemma exp_funr1 a : 0 < a -> a `^ 1 = a.
-Proof. by move=> a0; rewrite /exp_fun mul1r lnK. Qed.
+Lemma power_pos_gt0 a x : 0 < a -> 0 < a `^ x.
+Proof. by move=> a0; rewrite /power_pos gt_eqF// expR_gt0. Qed.
 
-Lemma exp_funr0 a : 0 < a -> a `^ 0 = 1.
-Proof. by move=> a0; rewrite /exp_fun mul0r expR0. Qed.
+Lemma power_posr1 a : 0 <= a -> a `^ 1 = a.
+Proof.
+move=> a0; rewrite /power_pos; case: ifPn => [/eqP->|a0'].
+  by rewrite oner_eq0.
+by rewrite mul1r lnK// posrE lt_neqAle eq_sym a0'.
+Qed.
+
+Lemma power_posr0 a : a `^ 0 = 1.
+Proof.
+by rewrite /power_pos; case: ifPn; rewrite ?eqxx// mul0r expR0.
+Qed.
+
+Lemma power_pos0 x : power_pos 0 x = (x == 0)%:R.
+Proof. by rewrite /power_pos eqxx. Qed.
+
+Lemma power_pos1 : power_pos 1 = fun=> 1.
+Proof. by apply/funext => x; rewrite /power_pos oner_eq0 ln1 mulr0 expR0. Qed.
 
-Lemma exp_fun1 : exp_fun 1 = fun=> 1.
-Proof. by rewrite funeqE => x; rewrite /exp_fun ln1 mulr0 expR0. Qed.
+Lemma power_pos_eq0 x p : x `^ p = 0 -> x = 0.
+Proof.
+rewrite /power_pos. have [->|_] := eqVneq x 0 => //.
+by move: (expR_gt0 (p * ln x)) => /gt_eqF /eqP.
+Qed.
 
-Lemma ler_exp_fun a : 1 < a -> {homo exp_fun a : x y / x <= y}.
-Proof. by move=> a1 x y xy; rewrite /exp_fun ler_expR ler_pmul2r // ln_gt0. Qed.
+Lemma ler_power_pos a : 1 < a -> {homo power_pos a : x y / x <= y}.
+Proof.
+move=> a1 x y xy.
+by rewrite /power_pos gt_eqF ?(le_lt_trans _ a1)// ler_expR ler_pmul2r// ln_gt0.
+Qed.
 
-Lemma exp_funD a : 0 < a -> {morph exp_fun a : x y / x + y >-> x * y}.
-Proof. by move=> a0 x y; rewrite [in LHS]/exp_fun mulrDl expRD. Qed.
+Lemma power_posM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
+Proof.
+rewrite 2!le_eqVlt.
+move=> /predU1P[<-|x0] /predU1P[<-|y0]; rewrite ?(mulr0, mul0r,power_pos0).
+- by rewrite -natrM; case: eqP.
+- by case: eqP => [->|]/=; rewrite ?mul0r ?power_posr0 ?mulr1.
+- by case: eqP => [->|]/=; rewrite ?mulr0 ?power_posr0 ?mulr1.
+- rewrite /power_pos mulf_eq0; case: eqP => [->|x0']/=.
+    rewrite (@gt_eqF _ _ y)//.
+    by case: eqP => /=; rewrite ?mul0r ?mul1r// => ->; rewrite mul0r expR0.
+  by rewrite gt_eqF// lnM ?posrE // -expRD mulrDr.
+Qed.
 
-Lemma exp_fun_inv a : 0 < a -> a `^ (-1) = a ^-1.
+Lemma power_posAC x y z : (x `^ y) `^ z = (x `^ z) `^ y.
 Proof.
-move=> a0.
+rewrite /power_pos.
+have [->/=|z0] := eqVneq z 0; rewrite ?mul0r.
+- have [->/=|y0] := eqVneq y 0; rewrite ?mul0r//=.
+  have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0//.
+  by rewrite oner_eq0 if_same ln1 mulr0 expR0.
+- have [->/=|y0] := eqVneq y 0; rewrite ?mul0r/=.
+    have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0//.
+    by rewrite oner_eq0 if_same ln1  mulr0 expR0.
+  have [x0|x0] := eqVneq x 0; rewrite ?eqxx ?oner_eq0 ?ln1 ?mulr0 ?expR0.
+    by [].
+  rewrite gt_eqF ?expR_gt0// gt_eqF; last by rewrite expR_gt0.
+  by rewrite !expK mulrCA.
+Qed.
+
+Lemma power_posD a : 0 < a -> {morph power_pos a : x y / x + y >-> x * y}.
+Proof. by move=> a0 x y; rewrite /power_pos gt_eqF// mulrDl expRD. Qed.
+
+Lemma power_pos_mulrn a n : 0 <= a -> a `^ n%:R = a ^+ n.
+Proof.
+move=> a0; elim: n => [|n ih].
+  by rewrite mulr0n expr0 power_posr0//; apply: lt0r_neq0.
+move: a0; rewrite le_eqVlt => /predU1P[<-|a0].
+  by rewrite !power_pos0 mulrn_eq0/= oner_eq0/= expr0n.
+by rewrite -natr1 power_posD// ih power_posr1// ?exprS 1?mulrC// ltW.
+Qed.
+
+Lemma power_pos_inv1 a : 0 <= a -> a `^ (-1) = a ^-1.
+Proof.
+rewrite le_eqVlt => /predU1P[<-|a0].
+  by rewrite power_pos0 invr0 oppr_eq0 oner_eq0.
 apply/(@mulrI _ a); first by rewrite unitfE gt_eqF.
-rewrite -[X in X * _ = _](exp_funr1 a0) -exp_funD // subrr exp_funr0 //.
-by rewrite divrr // unitfE gt_eqF.
+rewrite -[X in X * _ = _](power_posr1 (ltW a0)) -power_posD // subrr.
+by rewrite power_posr0 divff// gt_eqF.
 Qed.
 
-Lemma exp_fun_mulrn a n : 0 < a -> exp_fun a n%:R = a ^+ n.
+Lemma power_pos_inv a n : 0 <= a -> a `^ (- n%:R) = a ^- n.
 Proof.
-move=> a0; elim: n => [|n ih]; first by rewrite mulr0n expr0 exp_funr0.
-by rewrite -natr1 exprSr exp_funD// ih exp_funr1.
+move=> a0; elim: n => [|n ih].
+  by rewrite -mulNrn mulr0n power_posr0 -exprVn expr0.
+move: a0; rewrite le_eqVlt => /predU1P[<-|a0].
+  by rewrite power_pos0 oppr_eq0 mulrn_eq0 oner_eq0 orbF exprnN exp0rz oppr_eq0.
+rewrite -natr1 opprD power_posD// (power_pos_inv1 (ltW a0)) ih.
+by rewrite -[in RHS]exprVn exprS [in RHS]mulrC exprVn.
 Qed.
 
-End ExpFun.
-Notation "a `^ x" := (exp_fun a x).
+Lemma power_pos_intmul a (z : int) : 0 <= a -> a `^ z%:~R = a ^ z.
+Proof.
+move=> a0; have [z0|z0] := leP 0 z.
+  rewrite -[in RHS](gez0_abs z0) abszE -exprnP -power_pos_mulrn//.
+  by rewrite natr_absz -abszE gez0_abs.
+rewrite -(opprK z) (_ : - z = `|z|%N); last by rewrite ltz0_abs.
+by rewrite -exprnN -power_pos_inv// nmulrn.
+Qed.
+
+Lemma power12_sqrt a : 0 <= a -> a `^ (2^-1) = Num.sqrt a.
+Proof.
+rewrite le_eqVlt => /predU1P[<-|a0].
+  by rewrite power_pos0 sqrtr0 invr_eq0 pnatr_eq0.
+have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2.
+  rewrite sqr_sqrtr; last exact: ltW.
+  by rewrite /power_pos gt_eqF// -expRMm mulrA divrr ?mul1r ?unitfE// lnK.
+rewrite eqf_sqr => /predU1P[//|/eqP h].
+have : 0 < a `^ 2^-1 by apply: power_pos_gt0.
+by rewrite h oppr_gt0 ltNge sqrtr_ge0.
+Qed.
+
+End PowerPos.
+Notation "a `^ x" := (power_pos a x) : real_scope.
 
 Section riemannR_series.
 Variable R : realType.
 Implicit Types a : R.
-Local Open Scope ring_scope.
+Local Open Scope real_scope.
 
 Definition riemannR a : R ^nat := fun n => (n.+1%:R `^ a)^-1.
 Arguments riemannR a n /.
 
-Lemma riemannR_gt0 a i : 0 < a -> 0 < riemannR a i.
-Proof. move=> ?; by rewrite /riemannR invr_gt0 exp_fun_gt0. Qed.
+Lemma riemannR_gt0 a i : 0 <= a -> 0 < riemannR a i.
+Proof. by move=> ?; rewrite /riemannR invr_gt0 power_pos_gt0. Qed.
 
-Lemma dvg_riemannR a : 0 < a <= 1 -> ~ cvg (series (riemannR a)).
+Lemma dvg_riemannR a : 0 <= a <= 1 -> ~ cvg (series (riemannR a)).
 Proof.
-case/andP => a0; rewrite le_eqVlt => /orP[/eqP ->|a1].
+case/andP => a0; rewrite le_eqVlt => /predU1P[->|a1].
   rewrite (_ : riemannR 1 = harmonic); first exact: dvg_harmonic.
-  by rewrite funeqE => i /=; rewrite exp_funr1.
+  by rewrite funeqE => i /=; rewrite power_posr1.
 have : forall n, harmonic n <= riemannR a n.
-  case=> /= [|n]; first by rewrite exp_fun1 invr1.
-  rewrite -[leRHS]div1r ler_pdivl_mulr ?exp_fun_gt0 // mulrC ler_pdivr_mulr //.
-  by rewrite mul1r -[leRHS]exp_funr1 // (ler_exp_fun) // ?ltr1n // ltW.
+  case=> /= [|n]; first by rewrite power_pos1 invr1.
+  rewrite -[leRHS]div1r ler_pdivl_mulr ?power_pos_gt0 // mulrC ler_pdivr_mulr //.
+  by rewrite mul1r -[leRHS]power_posr1 // (ler_power_pos) // ?ltr1n // ltW.
 move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))).
 by move/contra_not; apply; exact: dvg_harmonic.
 Qed.

theories/lebesgue_measure.v

@@ -5,7 +5,7 @@ From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
 Require Import reals ereal signed topology numfun normedtype.
 From HB Require Import structures.
-Require Import sequences esum measure real_interval realfun.
+Require Import sequences esum measure real_interval realfun exp.
 
 (******************************************************************************)
 (*                            Lebesgue Measure                                *)
@@ -1630,7 +1630,7 @@ rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK.
 by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE.
 Qed.
 
-Lemma measurable_fun_max  D f g :
+Lemma measurable_fun_max D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g).
 Proof.
 move=> mf mg mD; apply (measurability (RGenCInfty.measurableE R)) => //.
@@ -1700,6 +1700,36 @@ Qed.
 
 End measurable_fun_realType.
 
+Lemma measurable_fun_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R).
+Proof.
+rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first.
+  by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=;
+    rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP].
+apply/measurable_funU; [exact: measurable_itv|exact: measurable_itv|split].
+- apply/(@measurable_restrict _ _ _ _ _ setT)=> //; first exact: measurable_itv.
+  rewrite (_ : _ \_ _ = cst (0:R)); first exact: measurable_fun_cst.
+  apply/funext => y; rewrite patchE.
+  by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW.
+- have : {in `]0, +oo[%classic, continuous (@ln R)}.
+    by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln.
+  rewrite -continuous_open_subspace; last exact: interval_open.
+  by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv.
+Qed.
+
+Lemma measurable_fun_power_pos (R : realType) p :
+  measurable_fun [set: R] (@power_pos R ^~ p).
+Proof.
+apply: measurable_fun_if => //.
+- apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//.
+  by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx.
+- exact: measurable_fun_cst.
+- rewrite setTI; apply: (@measurable_fun_comp _ _ _ _ _ _ setT) => //.
+    by apply: continuous_measurable_fun; exact: continuous_expR.
+  rewrite (_ : _ @^-1` _ = [set~ 0]); last first.
+    by apply/seteqP; split => [x [/negP/negP/eqP]|x x0]//=; exact/negbTE/eqP.
+  by apply: measurable_funrM; exact: measurable_fun_ln.
+Qed.
+
 Section standard_emeasurable_fun.
 Variable R : realType.