proposition: Theorem RND_Min_Pos_canonic : forall r : R, (0 <= r)%R -> Fcanonic radix b (RND_Min_Pos r).
proof: Proof. intros r H1; unfold RND_Min_Pos in |- *. generalize ln_radix_pos; intros W. case (Rle_dec (firstNormalPos radix b p) r); intros H2. cut (0 < r)%R; [ intros V | idtac ]. 2: apply Rlt_le_trans with (2 := H2); rewrite firstNormalPos_eq; auto with real zarith. left; split. apply RND_Min_Pos_bounded_aux; auto. apply Zgt_succ_le; apply Z.lt_gt. apply lt_IZR. apply Rle_lt_trans with (2 := IRNDD_correct2 (ln r / ln radix + (- Z.pred p)%Z)). apply Rplus_le_reg_l with (Z.pred p). apply Rmult_le_reg_l with (ln radix). apply ln_radix_pos. apply Rle_trans with (ln r). apply exp_le_inv. rewrite exp_ln; auto. replace (Z.pred p + (- dExp b)%Z)%R with (IZR (Z.pred p + - dExp b)). rewrite exp_ln_powerRZ; auto with zarith. apply Rle_trans with (2 := H2). rewrite firstNormalPos_eq; auto with real. rewrite plus_IZR; rewrite Ropp_Ropp_IZR; ring. rewrite Ropp_Ropp_IZR; right; field; auto with real. rewrite <- exp_ln_powerRZ; auto with zarith. pattern r at 1 in |- *; rewrite <- (exp_ln r); auto. apply exp_increasing. rewrite plus_IZR. apply Rle_lt_trans with (ln radix * (ln r / ln radix + (- Z.pred p)%Z - 1 + p))%R. rewrite Ropp_Ropp_IZR; unfold Z.pred in |- *; rewrite plus_IZR; simpl in |- *. right; field; auto with real. apply Rmult_lt_compat_l; auto with real. apply Rplus_lt_compat_r; auto with real. apply IRNDD_correct3. simpl in |- *; rewrite pGivesBound; apply le_IZR; simpl in |- *. 2: apply powerRZ_lt, IZR_lt; lia. rewrite Zpower_nat_Z_powerRZ; rewrite Z.abs_eq. 2: apply le_IZR; rewrite mult_IZR; simpl in |- *. 2: apply Rmult_le_pos. 2: apply IZR_le; auto with real zarith. 2: apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith. 2: apply powerRZ_le, IZR_lt; lia. rewrite mult_IZR; pattern (Z_of_nat p) at 1 in |- *; replace (Z_of_nat p) with (1 + Z.pred p)%Z. 2: unfold Z.pred in |- *; ring. rewrite powerRZ_add; try apply IZR_neq; auto with zarith real; simpl in |- *; ring_simplify (radix * 1)%R. apply Rmult_le_compat_l; auto with zarith real. apply IZR_le; lia. rewrite <- inj_pred; auto with zarith. rewrite <- Zpower_nat_Z_powerRZ; apply IZR_le. apply Zgt_succ_le; apply Z.lt_gt; apply lt_IZR; rewrite Ropp_Ropp_IZR. apply Rle_lt_trans with (r * powerRZ radix (- IRNDD (ln r / ln radix + - pred p)))%R. 2: apply IRNDD_correct2. rewrite <- exp_ln_powerRZ; auto with zarith. rewrite Zpower_nat_Z_powerRZ; rewrite Ropp_Ropp_IZR. apply Rle_trans with (r * exp (ln radix * - (ln r / ln radix + - pred p)))%R. pattern r at 1 in |- *; rewrite <- (exp_ln r); auto; rewrite <- exp_plus. replace (ln r + ln radix * - (ln r / ln radix + - pred p))%R with (ln radix * pred p)%R. 2: field; auto with real. rewrite exp_ln_powerRZ; auto with real zarith. apply Rmult_le_compat_l; auto with real. apply exp_monotone; auto with real. apply Rmult_le_compat_l; auto with real. apply Ropp_le_contravar; apply IRNDD_correct1. cut (r < powerRZ radix (Z.pred p + - dExp b))%R; [ intros H3 | idtac ]. 2: rewrite <- firstNormalPos_eq; auto with real. right; split. pattern (dExp b) at 2 in |- *; replace (Z_of_N (dExp b)) with (- - dExp b)%Z; auto with zarith. apply RND_Min_Pos_bounded_aux; auto with zarith. apply Rlt_trans with (1 := H3); apply Rlt_powerRZ; try apply IZR_lt; auto with real zarith. split; [ simpl in |- *; auto | idtac ]. simpl in |- *; rewrite pGivesBound; apply lt_IZR. rewrite Zpower_nat_Z_powerRZ; rewrite <- Rabs_Zabs. rewrite mult_IZR; rewrite Rabs_right; [ idtac | apply Rle_ge; apply Rmult_le_pos]. 2: apply IZR_le; lia. 2: apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith. 2: apply powerRZ_le, IZR_lt; lia. apply Rle_lt_trans with (radix * (r * powerRZ radix (dExp b)))%R; auto with real zarith. apply Rmult_le_compat_l; try apply IZR_le; auto with zarith. apply IRNDD_correct1. apply Rlt_le_trans with (radix * (powerRZ radix (Z.pred p + - dExp b) * powerRZ radix (dExp b)))%R; auto with real zarith. apply Rmult_lt_compat_l. apply IZR_lt; lia. apply Rmult_lt_compat_r; auto with real. apply powerRZ_lt, IZR_lt; lia. rewrite <- powerRZ_add; try apply IZR_neq; auto with zarith real. pattern (IZR radix) at 1 in |- *; replace (IZR radix) with (powerRZ radix 1); [ rewrite <- powerRZ_add; try apply IZR_neq | simpl in |- * ]; auto with zarith real; unfold Z.pred in |- *. ring_simplify (1 + (p + -1 + - dExp b + dExp b))%Z; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz