proposition: Theorem BoundedL: forall (r:R) (x:float) (e:Z), (e <=Fexp x)%Z -> (-dExp b <= e)%Z -> (FtoRradix x=r)%R -> (Rabs r < powerRZ radix (e+p))%R -> (exists x':float, (FtoRradix x'=r) /\ (Fbounded b x') /\ Fexp x'=e).
proof: Proof. intros. exists (Float (Fnum x*Zpower_nat radix (Z.abs_nat (Fexp x -e)))%Z e). split. rewrite <- H1; unfold FtoRradix, FtoR; simpl. rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ. rewrite Rmult_assoc; rewrite <- powerRZ_add. replace (Z.abs_nat (Fexp x - e) + e)%Z with (Fexp x); auto with real. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply IZR_neq; lia. split;[idtac|simpl; auto]. split; simpl; auto. apply lt_IZR. rewrite pGivesBound; rewrite <- Rabs_Zabs; rewrite mult_IZR. repeat rewrite Zpower_nat_Z_powerRZ. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. rewrite Rabs_mult; rewrite (Rabs_right ( powerRZ radix (Fexp x - e))). 2: apply Rle_ge, powerRZ_le, IZR_lt; lia. apply Rmult_lt_reg_l with (powerRZ radix e); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite <- powerRZ_add. apply Rle_lt_trans with (2:=H2); rewrite <- H1. unfold FtoRradix, FtoR; rewrite Rabs_mult. rewrite (Rabs_right (powerRZ radix (Fexp x))). 2: apply Rle_ge; auto with real zarith. right; apply trans_eq with (Rabs (Fnum x)*(powerRZ radix e*powerRZ radix (Fexp x-e)))%R;[ring|idtac]. rewrite <- powerRZ_add. ring_simplify (e+(Fexp x-e))%Z; auto with real. apply IZR_neq; lia. apply powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz