From efd64b541978e2a281be2f565a927e6043d5456c Mon Sep 17 00:00:00 2001 From: jmmarulang <78051861+jmmarulang@users.noreply.github.com> Date: Thu, 21 Nov 2024 07:34:48 +0000 Subject: [PATCH] modifinng exp.v for the new definition of poweR d --- theories/exp.v | 98 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 88 insertions(+), 10 deletions(-) diff --git a/theories/exp.v b/theories/exp.v index 2e2d30497..3210283bb 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -624,7 +624,7 @@ Implicit Types x : R. Notation exp := (@expR R). -Definition ln x : R := [get y | exp y == x ]. +Definition ln x : R := [get y | exp y == x ]. (*is this computable? *) Fact ln0 x : x <= 0 -> ln x = 0. Proof. @@ -996,7 +996,7 @@ Implicit Types (s r : R) (x y : \bar R). Definition poweR x r := match x with | x'%:E => (x' `^ r)%:E - | +oo => if r == 0%R then 1%E else +oo + | +oo => if r == 0%R then 1%E else if (r < 0)%R then 0 else +oo | -oo => if r == 0%R then 1%E else 0%E end. @@ -1005,38 +1005,81 @@ Local Notation "x `^ r" := (poweR x r). Lemma poweR_EFin s r : s%:E `^ r = (s `^ r)%:E. Proof. by []. Qed. +Lemma ltxy_ltyx s r : (s < r)%R -> (r < s)%R -> False. +Proof. + by move/(@lt_trans _ _ r s s); rewrite ltxx falseE. +Qed. + +Lemma poweRyr_lt0r r : (0 < r)%R -> +oo `^ r = +oo. +Proof. + move => pr; rewrite //= [_ == _](contra_neqF _ (lt0r_neq0 pr)); + last apply /eqP. case : ifP => //=. + move => r0. exfalso; apply (ltxy_ltyx pr r0). +Qed. + +Lemma poweRyr_ltr0 r : (r < 0)%R -> +oo `^ r = 0. +Proof. by move => r0; rewrite //= [_ == _](contra_neqF _ (ltr0_neq0 r0)); + last apply /eqP; rewrite r0. +Qed. + +(* Lemma poweRyr r : r != 0%R -> +oo `^ r = +oo. -Proof. by move/negbTE => /= ->. Qed. +Proof. + move/negbTE => /= ->. + Qed. +*) Lemma poweRe0 x : x `^ 0 = 1. Proof. by move: x => [x'| |]/=; rewrite ?powRr0// eqxx. Qed. Lemma poweRe1 x : 0 <= x -> x `^ 1 = x. Proof. -by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)). + move: x => [x'| |]//= x0; rewrite ?powRr1 //=. + rewrite (negbTE (oner_neq0 _)). + case : ifP => r0 //=. exfalso; apply (ltxy_ltyx r0 lte01). Qed. Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E. Proof. by case: x => // x xf; rewrite poweR_EFin powRN. Qed. + Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0. Proof. by move=> r0 /=; rewrite (negbTE r0). Qed. + Lemma poweR_eqy x r : x `^ r = +oo -> x = +oo. Proof. by case: x => [x| |] //=; case: ifP. Qed. +Lemma eqy_poweR_lt0r x r : (0 < r)%R -> x = +oo -> x `^ r = +oo. +Proof. + move: x => [| |]//= r0 _. rewrite gt_eqF //=. + case : ifP => f0 //=. exfalso; apply (ltxy_ltyx r0 f0). +Qed. +(* Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo. Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed. +*) Lemma poweR_lty x r : x < +oo -> x `^ r < +oo. Proof. by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry. Qed. +Lemma lty_poweRy_lt0r x r : (0 < r)%R -> x `^ r < +oo -> x < +oo. +Proof. + move : x => [s | | ] //=; + rewrite ?ltry//. + case : ifP; move/eqP => r0; + first by rewrite r0 [(_ < _)%R]ltxx. + by case : ifP => //=; move/ltxy_ltyx => //=. +Qed. + +(* Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo. Proof. by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (negbTE r0). Qed. +*) Lemma poweR0r r : r != 0%R -> 0 `^ r = 0. Proof. by move=> r0; rewrite poweR_EFin powR0. Qed. @@ -1045,16 +1088,32 @@ Lemma poweR1r r : 1 `^ r = 1. Proof. by rewrite poweR_EFin powR1. Qed. Lemma fine_poweR x r : fine (x `^ r) = ((fine x) `^ r)%R. Proof. -by move: x => [x| |]//=; case: ifPn => [/eqP ->|?]; rewrite ?powRr0 ?powR0. + move: x => [x| |]//=. + case : ifP => [/eqP -> |r0]; rewrite ?powRr0 //= (powR0 (contraFneq _ r0)); + last by move/eqP => //=. + - case : ifP => //=. + - case : ifP => [/eqP -> //= | r0]; rewrite ?powRr0 //= ?powR0 //=; + by rewrite (contraFneq _ r0); last by move/eqP => //=. Qed. Lemma poweR_ge0 x r : 0 <= x `^ r. -Proof. by move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; case: ifPn. Qed. +Proof. + move: x => [x| |]/=; rewrite ?lee_fin ?powR_ge0//; + repeat case : ifP => //=. +Qed. + +Lemma poweR_gt0 x r : 0 < x < +oo -> 0 < x `^ r. +Proof. + move: x => [x /andP [x0 xy]| /andP [x0 xy]|]//=. + move : x0; repeat apply lte_tofin; apply powR_gt0. +Qed. +(* Lemma poweR_gt0 x r : 0 < x -> 0 < x `^ r. Proof. by move: x => [x|_|]//=; [rewrite lte_fin; exact: powR_gt0|case: ifPn]. Qed. +*) Lemma gt0_poweR x r : (0 < r)%R -> 0 <= x -> 0 < x `^ r -> 0 < x. Proof. @@ -1062,25 +1121,44 @@ move=> r0; move: x => [x|//|]; rewrite ?leeNe_eq// lee_fin !lte_fin. exact: gt0_powR. Qed. +Lemma poweR_eq0 x r : 0 <= x < +oo -> (x `^ r == 0) = ((x == 0) && (r != 0%R)). +Proof. + move: x => [x _|/= /andP [_ ]|//]; + first by rewrite poweR_EFin eqe powR_eq0. + by rewrite ltxx. +Qed. + +(* Lemma poweR_eq0 x r : 0 <= x -> (x `^ r == 0) = ((x == 0) && (r != 0%R)). Proof. move: x => [x _|_/=|//]; first by rewrite poweR_EFin eqe powR_eq0. by case: ifP => //; rewrite onee_eq0. Qed. +*) +Lemma poweR_eq0_eq0 x r : 0 <= x < +oo -> x `^ r = 0 -> x = 0. +Proof. + by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. +Qed. +(* Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0. Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed. +*) Lemma gt0_ler_poweR r : (0 <= r)%R -> {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}. Proof. move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _]. -- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _]. - + by rewrite !lee_fin ge0_ler_powR. - + by case: eqP => [->|]; rewrite ?powRr0 ?leey. -- by rewrite leye_eq => /eqP ->. +- case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _]; + first by rewrite !lee_fin ge0_ler_powR. + case : ifP => /eqP H; rewrite ?H //= ?powRr0 //=; case : ifP => //= H0. + - rewrite le0r in r0; case : (orP r0) => //= /eqP => //=; + first by move => H1; exfalso; apply (ltxy_ltyx H0 (eqP H1)). + - apply (@leey _ (x `^ r)%:E). +- case : y => //=. Qed. + Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num. Proof. by move=> xfin; rewrite ge0_fin_numE ?poweR_lty ?ltey_eq ?xfin// poweR_ge0.