Commit 8fd4c8c0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Generalize ln_beta_F2R.

parent 9d8706aa
......@@ -1771,6 +1771,28 @@ apply Rle_ge.
apply bpow_ge_0.
Qed.
Theorem ln_beta_mult_bpow :
forall x e, x <> R0 ->
(ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z.
Proof.
intros x e Zx.
destruct (ln_beta x) as (ex, Ex) ; simpl.
specialize (Ex Zx).
apply ln_beta_unique.
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow e)) by apply bpow_ge_0.
split.
replace (ex + e - 1)%Z with (ex - 1 + e)%Z by ring.
rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Ex.
rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
apply Ex.
Qed.
Theorem ln_beta_le_bpow :
forall x e,
x <> R0 ->
......
......@@ -417,23 +417,9 @@ Theorem ln_beta_F2R :
(ln_beta beta (F2R (Float beta m e)) = ln_beta beta (Z2R m) + e :> Z)%Z.
Proof.
intros m e H.
destruct (ln_beta beta (Z2R m)) as (d, Hd).
simpl.
specialize (Hd (Z2R_neq _ _ H)).
apply ln_beta_unique.
rewrite <- F2R_Zabs.
unfold F2R. simpl.
rewrite <- Z2R_abs in Hd.
split.
replace (d + e - 1)%Z with (d - 1 + e)%Z by ring.
rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Hd.
rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
apply Hd.
unfold F2R ; simpl.
apply ln_beta_mult_bpow.
exact (Z2R_neq m 0 H).
Qed.
Theorem float_distribution_pos :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment