Commit 3cc94cb2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Prove bpow_ln_beta_gt and abs_scaled_mantissa_lt_bpow.

parent 536a724e
......@@ -1822,6 +1822,18 @@ rewrite Zx, Rabs_R0.
apply bpow_gt_0.
Qed.
Theorem bpow_ln_beta_gt :
forall x,
(Rabs x < bpow (ln_beta x))%R.
Proof.
intros x.
destruct (Req_dec x 0) as [Zx|Zx].
rewrite Zx, Rabs_R0.
apply bpow_gt_0.
destruct (ln_beta x) as (ex, Ex) ; simpl.
now apply Ex.
Qed.
Theorem ln_beta_le_Zpower :
forall m e,
m <> Z0 ->
......
......@@ -349,6 +349,21 @@ now apply Rle_lt_trans with (2 := Ex).
now rewrite (proj2 (proj2 (valid_exp _) He)).
Qed.
Theorem abs_scaled_mantissa_lt_bpow :
forall x,
(Rabs (scaled_mantissa x) < bpow (ln_beta beta x - canonic_exp x))%R.
Proof.
intros x.
destruct (Req_dec x 0) as [Zx|Zx].
rewrite Zx, scaled_mantissa_0, Rabs_R0.
apply bpow_gt_0.
apply Rlt_le_trans with (1 := bpow_ln_beta_gt beta _).
apply bpow_le.
unfold scaled_mantissa.
rewrite ln_beta_mult_bpow with (1 := Zx).
apply Zle_refl.
Qed.
Theorem ln_beta_generic_gt :
forall x, (x <> 0)%R ->
generic_format x ->
......
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