Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

modifying exp.v for a different definition of poweR #1404

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

modifying exp.v for a different definition of poweR #1404

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
efd64b5
modifinng exp.v for the new definition of poweR
jmmarulang Nov 21, 2024
e3309d0
Merge branch 'math-comp:master' into master
jmmarulang Nov 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
98 changes: 88 additions & 10 deletions theories/exp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand All @@ -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.
Expand All @@ -1045,42 +1088,77 @@ 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.
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.
Expand Down
Loading