Commit 4bb55b24 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Removed absolute value from ln_beta.

parent 43d3e2cc
...@@ -655,7 +655,7 @@ Qed. ...@@ -655,7 +655,7 @@ Qed.
Lemma ln_beta : Lemma ln_beta :
forall x : R, forall x : R,
{e | (0 < x)%R -> (epow (e - 1)%Z <= x < epow e)%R}. {e | (x <> 0)%R -> (epow (e - 1)%Z <= Rabs x < epow e)%R}.
Proof. Proof.
intros x. intros x.
set (fact := ln (Z2R (radix_val r))). set (fact := ln (Z2R (radix_val r))).
...@@ -670,8 +670,11 @@ now apply Zlt_le_trans with (2 := radix_prop r). ...@@ -670,8 +670,11 @@ now apply Zlt_le_trans with (2 := radix_prop r).
apply (Z2R_lt 0). apply (Z2R_lt 0).
now apply Zlt_le_trans with (2 := radix_prop r). now apply Zlt_le_trans with (2 := radix_prop r).
(* . *) (* . *)
exists (Zfloor (ln x / fact) + 1)%Z. exists (Zfloor (ln (Rabs x) / fact) + 1)%Z.
intros Hx. intros Hx'.
generalize (Rabs_pos_lt _ Hx'). clear Hx'.
generalize (Rabs x). clear x.
intros x Hx.
rewrite 2!epow_exp. rewrite 2!epow_exp.
fold fact. fold fact.
pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)). pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)).
...@@ -723,16 +726,32 @@ Qed. ...@@ -723,16 +726,32 @@ Qed.
Lemma ln_beta_unique : Lemma ln_beta_unique :
forall (x : R) (e : Z), forall (x : R) (e : Z),
(epow (e - 1) <= x < epow e)%R -> (epow (e - 1) <= Rabs x < epow e)%R ->
projT1 (ln_beta x) = e. projT1 (ln_beta x) = e.
Proof. Proof.
intros x e1 Hx1. intros x e1 He.
destruct (Req_dec x 0) as [Hx|Hx].
elim Rle_not_lt with (1 := proj1 He).
rewrite Hx, Rabs_R0.
apply epow_gt_0.
destruct (ln_beta x) as (e2, Hx2). destruct (ln_beta x) as (e2, Hx2).
apply epow_unique with (2 := Hx1).
simpl. simpl.
apply Hx2. apply epow_unique with (2 := He).
apply Rlt_le_trans with (2 := proj1 Hx1). now apply Hx2.
apply epow_gt_0. Qed.
Lemma ln_beta_opp :
forall x,
projT1 (ln_beta (-x)) = projT1 (ln_beta x).
Proof.
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
now rewrite Hx, Ropp_0.
destruct (ln_beta x) as (e, He).
simpl.
specialize (He Hx).
apply ln_beta_unique.
now rewrite Rabs_Ropp.
Qed. Qed.
Lemma ln_beta_monotone : Lemma ln_beta_monotone :
...@@ -745,10 +764,15 @@ destruct (ln_beta x) as (ex, Hx). ...@@ -745,10 +764,15 @@ destruct (ln_beta x) as (ex, Hx).
destruct (ln_beta y) as (ey, Hy). destruct (ln_beta y) as (ey, Hy).
simpl. simpl.
apply epow_lt_epow. apply epow_lt_epow.
specialize (Hx H0x). specialize (Hx (Rgt_not_eq _ _ H0x)).
specialize (Hy (Rlt_le_trans _ _ _ H0x Hxy)). specialize (Hy (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ H0x Hxy))).
apply Rle_lt_trans with (1 := proj1 Hx). apply Rle_lt_trans with (1 := proj1 Hx).
now apply Rle_lt_trans with (2 := proj2 Hy). apply Rle_lt_trans with (2 := proj2 Hy).
rewrite 2!Rabs_pos_eq.
exact Hxy.
apply Rle_trans with (2 := Hxy).
now apply Rlt_le.
now apply Rlt_le.
Qed. Qed.
Lemma Zpower_pos_gt_0 : Lemma Zpower_pos_gt_0 :
...@@ -792,31 +816,34 @@ Lemma Zln_beta : ...@@ -792,31 +816,34 @@ Lemma Zln_beta :
{e | (Zpower (radix_val r) (e - 1) <= Zabs x < Zpower (radix_val r) e)%Z}. {e | (Zpower (radix_val r) (e - 1) <= Zabs x < Zpower (radix_val r) e)%Z}.
Proof. Proof.
intros x. intros x.
destruct (Z_le_lt_eq_dec 0 _ (Zabs_pos x)) as [Hx|Hx]. destruct (Z_eq_dec x 0) as [Hx|Hx].
(* . *) (* . *)
destruct (ln_beta (Z2R (Zabs x))) as (e, H). exists Z0.
specialize (H (Z2R_lt _ _ Hx)). rewrite Hx.
now split.
(* . *)
destruct (ln_beta (Z2R x)) as (e, H).
specialize (H (Z2R_neq _ _ Hx)).
exists e. exists e.
assert (He: (1 <= e)%Z). assert (He: (1 <= e)%Z).
apply (Zlt_le_succ 0). apply (Zlt_le_succ 0).
apply <- epow_lt. apply <- epow_lt.
apply Rle_lt_trans with (2 := proj2 H). apply Rle_lt_trans with (2 := proj2 H).
rewrite Rabs_Z2R.
apply (Z2R_le 1). apply (Z2R_le 1).
now apply (Zlt_le_succ 0). apply (Zlt_le_succ 0).
generalize (Zabs_spec x).
omega.
(* . . *) (* . . *)
split. split.
apply le_Z2R. apply le_Z2R.
rewrite Z2R_Zpower. rewrite Z2R_Zpower, <- Rabs_Z2R.
apply H. apply H.
now apply Zle_minus_le_0. now apply Zle_minus_le_0.
apply lt_Z2R. apply lt_Z2R.
rewrite Z2R_Zpower. rewrite Z2R_Zpower, <- Rabs_Z2R.
apply H. apply H.
now apply Zle_succ_le. now apply Zle_succ_le.
(* . *)
exists Z0.
rewrite <- Hx.
now split.
Qed. Qed.
End pow. End pow.
...@@ -67,9 +67,9 @@ now apply Zlt_le_weak. ...@@ -67,9 +67,9 @@ now apply Zlt_le_weak.
apply Zle_refl. apply Zle_refl.
rewrite Hx1. rewrite Hx1.
eexists ; repeat split. eexists ; repeat split.
destruct (ln_beta beta (Rabs x)) as (ex, Hx4). destruct (ln_beta beta x) as (ex, Hx4).
simpl in Hx2. simpl in Hx2.
specialize (Hx4 (Rabs_pos_lt x Hx3)). specialize (Hx4 Hx3).
apply lt_Z2R. apply lt_Z2R.
rewrite Z2R_Zpower. rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow (ex - prec)). apply Rmult_lt_reg_r with (bpow (ex - prec)).
...@@ -97,9 +97,9 @@ rewrite Hx4. ...@@ -97,9 +97,9 @@ rewrite Hx4.
apply generic_format_0. apply generic_format_0.
simpl in Hx2, Hx3. simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp. unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta (Rabs x)) as (ex, Hx5). destruct (ln_beta beta x) as (ex, Hx5).
simpl. simpl.
specialize (Hx5 (Rabs_pos_lt _ Hx4)). specialize (Hx5 Hx4).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ; destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2. rewrite H2 ; clear H2.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2). rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
...@@ -143,7 +143,7 @@ rewrite Hx4. ...@@ -143,7 +143,7 @@ rewrite Hx4.
eexists ; repeat split. eexists ; repeat split.
rewrite Hx5. clear Hx5. rewrite Hx5. clear Hx5.
rewrite <- Hx4. rewrite <- Hx4.
destruct (ln_beta beta (Rabs x)) as (ex, Hx5). destruct (ln_beta beta x) as (ex, Hx5).
unfold FLX_exp, FLT_exp. unfold FLX_exp, FLT_exp.
simpl. simpl.
apply sym_eq. apply sym_eq.
...@@ -151,8 +151,7 @@ apply Zmax_left. ...@@ -151,8 +151,7 @@ apply Zmax_left.
cut (emin + prec <= ex)%Z. omega. cut (emin + prec <= ex)%Z. omega.
apply epow_lt_epow with beta. apply epow_lt_epow with beta.
apply Rle_lt_trans with (1 := Hx1). apply Rle_lt_trans with (1 := Hx1).
apply Hx5. now apply Hx5.
now apply Rabs_pos_lt.
Qed. Qed.
Theorem FLT_format_FIX : Theorem FLT_format_FIX :
......
...@@ -100,11 +100,11 @@ now apply Zlt_le_trans with (2 := radix_prop beta). ...@@ -100,11 +100,11 @@ now apply Zlt_le_trans with (2 := radix_prop beta).
now apply Zlt_le_weak. now apply Zlt_le_weak.
apply generic_format_0. apply generic_format_0.
(* . *) (* . *)
destruct (ln_beta beta (Rabs x)) as (ex, Hx2). destruct (ln_beta beta x) as (ex, Hx2).
simpl. simpl.
specialize (Hx2 (Rabs_pos_lt _ Hx1)). specialize (Hx2 Hx1).
apply iff_trans with (generic_format beta (FIX_exp (ex - prec)) x). apply iff_trans with (generic_format beta (FIX_exp (ex - prec)) x).
assert (Hf: FLX_exp (projT1 (ln_beta beta (Rabs x))) = FIX_exp (ex - prec) (projT1 (ln_beta beta (Rabs x)))). assert (Hf: FLX_exp (projT1 (ln_beta beta x)) = FIX_exp (ex - prec) (projT1 (ln_beta beta x))).
unfold FIX_exp, FLX_exp. unfold FIX_exp, FLX_exp.
now rewrite ln_beta_unique with (1 := Hx2). now rewrite ln_beta_unique with (1 := Hx2).
split ; apply generic_format_fun_eq ; now rewrite Hf. split ; apply generic_format_fun_eq ; now rewrite Hf.
...@@ -149,18 +149,15 @@ intros H. ...@@ -149,18 +149,15 @@ intros H.
elim H. elim H.
rewrite H1, H3. rewrite H1, H3.
apply Rmult_0_l. apply Rmult_0_l.
destruct (ln_beta beta (Z2R (Zabs xm))) as (d,H4). destruct (ln_beta beta (Z2R xm)) as (d,H4).
assert (H5: (0 < Z2R (Zabs xm))%R). specialize (H4 (Z2R_neq _ _ H3)).
rewrite <- Rabs_Z2R.
apply Rabs_pos_lt.
now apply (Z2R_neq _ 0).
specialize (H4 H5). clear H5.
assert (H5: (0 <= prec - d)%Z). assert (H5: (0 <= prec - d)%Z).
cut (d - 1 < prec)%Z. omega. cut (d - 1 < prec)%Z. omega.
apply <- (epow_lt beta). apply <- (epow_lt beta).
apply Rle_lt_trans with (Z2R (Zabs xm)). apply Rle_lt_trans with (Rabs (Z2R xm)).
apply H4. apply H4.
rewrite <- Z2R_Zpower. rewrite <- Z2R_Zpower.
rewrite Rabs_Z2R.
now apply Z2R_lt. now apply Z2R_lt.
now apply Zlt_le_weak. now apply Zlt_le_weak.
exists (Float beta (xm * Zpower (radix_val beta) (prec - d)) (xe + d - prec)). exists (Float beta (xm * Zpower (radix_val beta) (prec - d)) (xe + d - prec)).
...@@ -183,7 +180,7 @@ rewrite Rabs_pos_eq. ...@@ -183,7 +180,7 @@ rewrite Rabs_pos_eq.
rewrite Rmult_assoc, <- epow_add. rewrite Rmult_assoc, <- epow_add.
ring_simplify (prec - 1 + (d - prec))%Z. ring_simplify (prec - 1 + (d - prec))%Z.
ring_simplify (prec - d + (d - prec))%Z. ring_simplify (prec - d + (d - prec))%Z.
now rewrite Rmult_1_r. now rewrite Rmult_1_r, <- Rabs_Z2R.
apply epow_ge_0. apply epow_ge_0.
exact H5. exact H5.
omega. omega.
...@@ -196,7 +193,7 @@ apply epow_gt_0. ...@@ -196,7 +193,7 @@ apply epow_gt_0.
rewrite Rmult_assoc, <- 2!epow_add. rewrite Rmult_assoc, <- 2!epow_add.
ring_simplify (prec + (d - prec))%Z. ring_simplify (prec + (d - prec))%Z.
ring_simplify (prec - d + (d - prec))%Z. ring_simplify (prec - d + (d - prec))%Z.
now rewrite Rmult_1_r. now rewrite Rmult_1_r, <- Rabs_Z2R.
apply epow_ge_0. apply epow_ge_0.
now apply Zlt_le_weak. now apply Zlt_le_weak.
exact H5. exact H5.
......
...@@ -63,9 +63,9 @@ split. ...@@ -63,9 +63,9 @@ split.
intros H. intros H.
now elim H. now elim H.
apply Zle_refl. apply Zle_refl.
destruct (ln_beta beta (Rabs x)) as (ex, Hx4). destruct (ln_beta beta x) as (ex, Hx4).
simpl in Hx2. simpl in Hx2.
specialize (Hx4 (Rabs_pos_lt x Hx3)). specialize (Hx4 Hx3).
unfold FTZ_exp in Hx2. unfold FTZ_exp in Hx2.
generalize (Zlt_cases (ex - prec) emin) Hx2. clear Hx2. generalize (Zlt_cases (ex - prec) emin) Hx2. clear Hx2.
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2. case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
...@@ -127,9 +127,9 @@ rewrite Hx4. ...@@ -127,9 +127,9 @@ rewrite Hx4.
apply generic_format_0. apply generic_format_0.
specialize (Hx2 Hx4). specialize (Hx2 Hx4).
unfold generic_format, canonic, FTZ_exp. unfold generic_format, canonic, FTZ_exp.
destruct (ln_beta beta (Rabs x)) as (ex, Hx6). destruct (ln_beta beta x) as (ex, Hx6).
simpl. simpl.
specialize (Hx6 (Rabs_pos_lt _ Hx4)). specialize (Hx6 Hx4).
generalize (Zlt_cases (ex - prec) emin). generalize (Zlt_cases (ex - prec) emin).
case (Zlt_bool (ex - prec) emin) ; intros H1. case (Zlt_bool (ex - prec) emin) ; intros H1.
elim (Rlt_not_ge _ _ (proj2 Hx6)). elim (Rlt_not_ge _ _ (proj2 Hx6)).
......
...@@ -22,7 +22,7 @@ Definition valid_exp := ...@@ -22,7 +22,7 @@ Definition valid_exp :=
Variable prop_exp : valid_exp. Variable prop_exp : valid_exp.
Definition canonic x (f : float beta) := Definition canonic x (f : float beta) :=
x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))). x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta x)).
Definition generic_format (x : R) := Definition generic_format (x : R) :=
exists f : float beta, exists f : float beta,
...@@ -83,11 +83,10 @@ simpl. ...@@ -83,11 +83,10 @@ simpl.
apply f_equal. apply f_equal.
apply sym_eq. apply sym_eq.
apply ln_beta_unique. apply ln_beta_unique.
rewrite Rabs_right. rewrite Rabs_pos_eq.
split. split.
exact Hbl. exact Hbl.
now apply Rle_lt_trans with (2 := Hx2). now apply Rle_lt_trans with (2 := Hx2).
apply Rle_ge.
apply Rle_trans with (2 := Hbl). apply Rle_trans with (2 := Hbl).
apply epow_ge_0. apply epow_ge_0.
split. split.
...@@ -142,10 +141,9 @@ intros g ((gm, ge), (Hg1, Hg2)) Hgx. ...@@ -142,10 +141,9 @@ intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le. apply Rnot_lt_le.
intros Hg3. intros Hg3.
destruct (ln_beta beta g) as (ge', Hg4). destruct (ln_beta beta g) as (ge', Hg4).
specialize (Hg4 Hg3). simpl in Hg2.
generalize Hg4. intros Hg5. specialize (Hg4 (Rgt_not_eq _ _ Hg3)).
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in Hg5. rewrite Rabs_pos_eq in Hg4.
rewrite ln_beta_unique with (1 := Hg5) in Hg2.
apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)). apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)).
apply Rle_trans with (bpow ge). apply Rle_trans with (bpow ge).
apply -> epow_le. apply -> epow_le.
...@@ -172,6 +170,7 @@ apply epow_gt_0. ...@@ -172,6 +170,7 @@ apply epow_gt_0.
rewrite Rmult_0_l. rewrite Rmult_0_l.
unfold F2R in Hg1. simpl in Hg1. unfold F2R in Hg1. simpl in Hg1.
now rewrite <- Hg1. now rewrite <- Hg1.
now apply Rlt_le.
(* - . . *) (* - . . *)
apply sym_eq. apply sym_eq.
apply Zfloor_imp. apply Zfloor_imp.
...@@ -296,9 +295,9 @@ apply Rnot_lt_le. ...@@ -296,9 +295,9 @@ apply Rnot_lt_le.
intros Hg3. intros Hg3.
assert (Hg4 : (g < 0)%R). assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx). now apply Rle_lt_trans with (1 := Hgx).
destruct (ln_beta beta (Rabs g)) as (ge', Hge). destruct (ln_beta beta g) as (ge', Hge).
simpl in Hg2. simpl in Hg2.
specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))). specialize (Hge (Rlt_not_eq _ _ Hg4)).
apply Rlt_not_le with (1 := Hg3). apply Rlt_not_le with (1 := Hg3).
rewrite Hg1. rewrite Hg1.
unfold F2R. simpl. unfold F2R. simpl.
...@@ -371,9 +370,9 @@ apply Rnot_lt_le. ...@@ -371,9 +370,9 @@ apply Rnot_lt_le.
intros Hg3. intros Hg3.
assert (Hg4 : (g < 0)%R). assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx). now apply Rle_lt_trans with (1 := Hgx).
destruct (ln_beta beta (Rabs g)) as (ge', Hge). destruct (ln_beta beta g) as (ge', Hge).
simpl in Hg2. simpl in Hg2.
specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))). specialize (Hge (Rlt_not_eq g 0 Hg4)).
rewrite (Rabs_left _ Hg4) in Hge. rewrite (Rabs_left _ Hg4) in Hge.
assert (Hge' : (ge' <= fexp ex)%Z). assert (Hge' : (ge' <= fexp ex)%Z).
cut (ge' - 1 < fexp ex)%Z. omega. cut (ge' - 1 < fexp ex)%Z. omega.
...@@ -465,11 +464,20 @@ Theorem canonic_sym : ...@@ -465,11 +464,20 @@ Theorem canonic_sym :
canonic x (Float beta m e) -> canonic x (Float beta m e) ->
canonic (-x) (Float beta (-m) e). canonic (-x) (Float beta (-m) e).
Proof. Proof.
intros x m e (H1,H2). intros x m e.
destruct (Req_dec x 0) as [Hx|Hx].
(* . *)
rewrite Hx, Ropp_0.
intros (H1,H2).
split.
now rewrite <- opp_F2R, <- H1, Ropp_0.
exact H2.
(* . *)
intros (H1,H2).
split. split.
rewrite H1. rewrite H1.
apply opp_F2R. apply opp_F2R.
now rewrite Rabs_Ropp. now rewrite ln_beta_opp.
Qed. Qed.
Theorem generic_format_sym : Theorem generic_format_sym :
...@@ -489,39 +497,32 @@ exact generic_format_0. ...@@ -489,39 +497,32 @@ exact generic_format_0.
exact generic_format_sym. exact generic_format_sym.
(* rounding down *) (* rounding down *)
exists (fun x => exists (fun x =>
match total_order_T 0 x with match Req_EM_T x 0 with
| inleft (left Hx) => | left Hx => R0
| right Hx =>
let e := fexp (projT1 (ln_beta beta x)) in let e := fexp (projT1 (ln_beta beta x)) in
F2R (Float beta (Zfloor (x * bpow (Zopp e))) e) F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
| inleft (right _) => R0
| inright Hx =>
let e := fexp (projT1 (ln_beta beta (-x))) in
F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
end). end).
intros x. intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx]. destruct (Req_EM_T x 0) as [Hx|Hx].
(* positive *) (* . *)
destruct (ln_beta beta x) as (ex, Hx').
simpl.
apply generic_DN_pt_pos.
now apply Hx'.
(* zero *)
split. split.
exists (Float beta 0 _) ; repeat split. apply generic_format_0.
unfold F2R. simpl. rewrite Hx.
now rewrite Rmult_0_l.
rewrite <- Hx.
split. split.
apply Rle_refl. apply Rle_refl.
intros g _ H. now intros g _ H.
exact H. (* . *)
(* negative *) destruct (ln_beta beta x) as (ex, H1).
destruct (ln_beta beta (- x)) as (ex, Hx').
simpl. simpl.
specialize (H1 Hx).
destruct (Rdichotomy _ _ Hx) as [H2|H2].
apply generic_DN_pt_neg. apply generic_DN_pt_neg.
apply Hx'. now rewrite <- Rabs_left.
rewrite <- Ropp_0. apply generic_DN_pt_pos.
now apply Ropp_lt_contravar. rewrite Rabs_right in H1.
exact H1.
now apply Rgt_ge.
Qed. Qed.
Theorem generic_DN_pt_small_pos : Theorem generic_DN_pt_small_pos :
...@@ -542,9 +543,9 @@ apply epow_ge_0. ...@@ -542,9 +543,9 @@ apply epow_ge_0.
intros g ((gm, ge), (Hg1, Hg2)) Hgx. intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le. apply Rnot_lt_le.
intros Hg3. intros Hg3.
destruct (ln_beta beta (Rabs g)) as (eg, Hg4). destruct (ln_beta beta g) as (eg, Hg4).
simpl in Hg2. simpl in Hg2.
specialize (Hg4 (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))). specialize (Hg4 (Rgt_not_eq g 0 Hg3)).
rewrite Rabs_right in Hg4. rewrite Rabs_right in Hg4.
apply Rle_not_lt with (1 := Hgx). apply Rle_not_lt with (1 := Hgx).
rewrite Hg1. rewrite Hg1.
...@@ -587,16 +588,15 @@ eexists ; repeat split. ...@@ -587,16 +588,15 @@ eexists ; repeat split.
simpl. simpl.
apply f_equal. apply f_equal.
apply sym_eq. apply sym_eq.
apply ln_beta_unique.
rewrite <- H. rewrite <- H.
apply ln_beta_unique.
split. split.
replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring. replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring.
apply RRle_abs. apply RRle_abs.
rewrite Rabs_right. rewrite Rabs_pos_eq.
apply -> epow_lt. apply -> epow_lt.
apply Zle_lt_succ. apply Zle_lt_succ.
apply Zle_refl. apply Zle_refl.
apply Rle_ge.
apply epow_ge_0. apply epow_ge_0.
split. split.
(* . *) (* . *)
...@@ -610,9 +610,9 @@ apply Rgt_not_eq. ...@@ -610,9 +610,9 @@ apply Rgt_not_eq.
apply Rlt_le_trans with (2 := Hgx). apply Rlt_le_trans with (2 := Hgx).
apply Rlt_le_trans with (2 := proj1 Hx). apply Rlt_le_trans with (2 := proj1 Hx).
apply epow_gt_0. apply epow_gt_0.
destruct (ln_beta beta (Rabs g)) as (eg, Hg3). destruct (ln_beta beta g) as (eg, Hg3).
simpl in Hg2. simpl in Hg2.
specialize (Hg3 (Rabs_pos_lt g H0)). specialize (Hg3 H0).
apply Rnot_lt_le. apply Rnot_lt_le.
intros Hgp. intros Hgp.
apply Rlt_not_le with (1 := Hgp). apply Rlt_not_le with (1 := Hgp).
...@@ -702,7 +702,7 @@ End RND_generic. ...@@ -702,7 +702,7 @@ End RND_generic.
Theorem canonic_fun_eq : Theorem canonic_fun_eq :
forall beta : radix, forall f1 f2 : Z -> Z, forall x f, forall beta : radix, forall f1 f2 : Z -> Z, forall x f,
f1 (projT1 (ln_beta beta (Rabs x))) = f2 (projT1 (ln_beta beta (Rabs x))) ->