From ee12aba894e8949a32daa9d2ee72b3a440c0609f Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 31 Mar 2023 20:09:42 +0900 Subject: [PATCH] gen exp_fun (#876) * gen exp_fun - rename to power_pow - fix doc - add scope to notation Co-authored-by: Alessandro Bruni Co-authored-by: Takafumi Saikawa * 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 Co-authored-by: Takafumi Saikawa Co-authored-by: Alessandro Bruni --- CHANGELOG_UNRELEASED.md | 21 +++++ theories/exp.v | 153 ++++++++++++++++++++++++++++-------- theories/lebesgue_measure.v | 34 +++++++- 3 files changed, 173 insertions(+), 35 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6ac6932cc..a759e22b4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/theories/exp.v b/theories/exp.v index 367daac7c..e59b890fa 100644 --- a/theories/exp.v +++ b/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. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 94a5f5e7d..7e1dc431f 100644 --- a/theories/lebesgue_measure.v +++ b/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.