Added theorem ln_beta_le and simplified some proofs.

src/Calc/Fcalc_digits.v

@@ -411,17 +411,13 @@ apply Zplus_lt_compat.
 now apply Zplus_lt_compat.
 now apply Zmult_lt_0_compat.
 rewrite 3!digits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
-destruct (ln_beta beta (Z2R (x + y + x * y))) as (exy, Hexy). simpl.
-specialize (Hexy (Rgt_not_eq _ _ Hxy)).
+apply ln_beta_le with (1 := Rgt_not_eq _ _ Hxy).
+rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy).
 destruct (ln_beta beta (Z2R x)) as (ex, Hex). simpl.
 specialize (Hex (Rgt_not_eq _ _ (Z2R_lt _ _ Hx))).
 destruct (ln_beta beta (Z2R y)) as (ey, Hey). simpl.
 specialize (Hey (Rgt_not_eq _ _ (Z2R_lt _ _ Hy))).
-eapply bpow_lt_bpow.
 apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R.
-apply Rle_lt_trans with (Z2R (x + y + x * y)).
-rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Hxy)).
-apply Hexy.
 rewrite <- Z2R_mult.
 apply Z2R_lt.
 apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z.

src/Core/Fcore_Raux.v

@@ -2125,6 +2125,19 @@ apply Rle_ge.
 apply bpow_ge_0.
 Qed.
 
+Theorem ln_beta_le :
+  forall x e,
+  x <> R0 ->
+  (Rabs x < bpow e)%R ->
+  (ln_beta x <= e)%Z.
+Proof.
+intros x e Zx Hx.
+destruct (ln_beta x) as (ex, Ex) ; simpl.
+specialize (Ex Zx).
+apply bpow_lt_bpow.
+now apply Rle_lt_trans with (Rabs x).
+Qed.
+
 Theorem ln_beta_Z2R_le :
   forall m e,
   m <> Z0 ->
@@ -2132,10 +2145,8 @@ Theorem ln_beta_Z2R_le :
   (ln_beta (Z2R m) <= e)%Z.
 Proof.
 intros m e Zm Hm.
-destruct (ln_beta (Z2R m)) as (e',E) ; simpl.
-specialize (E (Z2R_neq m 0 Zm)).
-apply bpow_lt_bpow.
-apply Rle_lt_trans with (1 := proj1 E).
+apply ln_beta_le.
+exact (Z2R_neq m 0 Zm).
 destruct (Zle_or_lt 0 e).
 rewrite <- Z2R_abs, <- Z2R_Zpower with (1 := H).
 now apply Z2R_lt.

src/Prop/Fprop_Sterbenz.v

@@ -74,10 +74,7 @@ rewrite <- Pxy, plus_F2R, <- Hx, <- Hy.
 unfold canonic_exponent.
 replace exy with (fexp (Zmin ex ey)).
 apply monotone_exp.
-apply bpow_lt_bpow with beta.
-apply Rle_lt_trans with (2 := Hxy).
-destruct (ln_beta beta (x + y)) as (exy', Exy). simpl.
-now apply Exy.
+now apply ln_beta_le.
 replace exy with (Fexp (Fplus beta fx fy)) by exact (f_equal Fexp Pxy).
 rewrite Fexp_Fplus.
 simpl. clear -monotone_exp.

src/Prop/Fprop_div_sqrt_error.v

@@ -50,15 +50,9 @@ rewrite <- Hz.
 apply Zle_trans with (Zmin (Fexp fx) (Fexp fy)).
 unfold canonic_exponent, FLX_exp.
 rewrite plus_F2R, <- Hx, <- Hy.
-destruct (ln_beta beta (x+y)); simpl.
-specialize (a H).
-apply Zmin_case.
 apply Zplus_le_reg_l with prec; ring_simplify.
-apply (bpow_lt_bpow beta).
-now apply Rle_lt_trans with (1:=proj1 a).
-apply Zplus_le_reg_l with prec; ring_simplify.
-apply (bpow_lt_bpow beta).
-now apply Rle_lt_trans with (1:=proj1 a).
+apply ln_beta_le with (1 := H).
+now apply Zmin_case.
 rewrite <- Fexp_Fplus, Hz.
 apply Zle_refl.
 Qed.

src/Prop/Fprop_mult_error.v

@@ -123,17 +123,12 @@ clear Hr.
 apply Zle_trans with (cexp (x * y)%R - prec)%Z.
 unfold canonic_exponent, FLX_exp.
 apply Zplus_le_compat_r.
-rewrite ln_beta_unique with (1 := Her).
 rewrite ln_beta_unique with (1 := Hexy).
-apply (bpow_lt_bpow beta).
-apply Rle_lt_trans with (1 := proj1 Her).
-apply Rlt_le_trans with (ulp beta (FLX_exp prec) (x * y)).
+apply ln_beta_le with (1 := Hz).
+replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)).
 apply ulp_error...
-unfold ulp.
-apply bpow_le.
-unfold canonic_exponent, FLX_exp.
-rewrite ln_beta_unique with (1 := Hexy).
-apply Zle_refl.
+unfold ulp, canonic_exponent.
+now rewrite ln_beta_unique with (1 := Hexy).
 apply Hc1.
 reflexivity.
 Qed.