proposition: Theorem Underf_Err2_aux: forall (r:R) (x1:float), vNum b=vNum b' -> (dExp b <= dExp b')%Z -> (Fcanonic radix b x1) -> (Closest b radix r x1) -> (exists x2:float, (Underf_Err x1 x2 r (3/4)%R) /\ (Closest b' radix r x2)).
proof: Proof. intros. assert (ZH: (0 < 3/4)%R). apply Rmult_lt_reg_l with 4%R; auto with real. ring_simplify (4*0)%R; apply Rlt_le_trans with 3%R; auto with real. right; field; auto with real. case (Zle_lt_or_eq (-(dExp b))%Z (Fexp x1)). elim H2; intros I1 I2; elim I1; auto. intros I. exists x1; split. split; auto. assert (Fbounded b x1);[elim H2; auto|idtac]. split. split; auto with zarith. elim H3; intros; rewrite <- H; auto. split;[idtac|intros; auto with real]. ring_simplify (x1-x1)%R; rewrite Rabs_R0. apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. split;[elim H2; intros T T'; elim T; intros; split; try rewrite <- H; auto with zarith|idtac]. intros f H3. case (Zle_or_lt (-(dExp b)) (Fexp f)); intros. elim H2; intros T1 T2; apply T2. elim H3; intros; split; try rewrite H; auto with zarith. fold FtoRradix; replace (f-r)%R with (-((x1-f)-(x1-r)))%R;[rewrite Rabs_Ropp|ring]. apply Rle_trans with (Rabs (x1 - f) - Rabs (x1 - r))%R;[idtac|apply Rabs_triang_inv]. apply Rplus_le_reg_l with (Rabs (x1-r)). apply Rle_trans with (2*(Rabs (x1-r)))%R;[right; simpl; ring|idtac]. apply Rle_trans with (Rabs (x1 - f));[idtac|right; ring]. apply Rle_trans with (Fulp b radix p x1). replace (x1-r)%R with (-(r-x1))%R;[rewrite Rabs_Ropp|ring]. unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith. apply Rle_trans with (powerRZ radix (Fexp x1));[right; unfold FtoR; simpl; ring|idtac]. apply Rle_trans with ((Rabs x1)-Rabs f)%R;[idtac|apply Rabs_triang_inv]. apply Rplus_le_reg_l with (Rabs f). apply Rle_trans with (Rabs x1);[idtac|right;ring]. apply Rle_trans with (powerRZ radix (p-2+Fexp x1)+powerRZ radix (p-2+Fexp x1))%R. apply Rplus_le_compat. apply Rle_trans with (FtoRradix (Float (Zpos (vNum b')) (Fexp f))). apply Rlt_le; unfold FtoRradix; apply MaxFloat; auto. unfold FtoRradix, FtoR; rewrite <- H; rewrite pGivesBound;simpl. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add. apply Rle_powerRZ; try apply IZR_le; auto with zarith real. apply IZR_neq; lia. apply Rle_powerRZ; try apply IZR_le; auto with zarith real. apply Rle_trans with (2*powerRZ radix (p - 2 + Fexp x1))%R;[right; ring|idtac]. apply Rle_trans with (radix*powerRZ radix (p - 2 + Fexp x1))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl. rewrite powerRZ_add. rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. case H1; intros T. elim T; intros H5 H6. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. apply IZR_lt; lia. apply Rle_trans with (IZR (Zpos (vNum b))). right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ. unfold Zminus; rewrite powerRZ_add; simpl. ring_simplify (radix*1)%R; field; auto with real zarith. apply IZR_neq; lia. apply IZR_neq; lia. apply Rle_trans with (IZR(Z.abs (radix * Fnum x1))); auto with real zarith. apply IZR_le; auto with zarith real. rewrite Zabs_Zmult; rewrite Z.abs_eq; auto with zarith real. right; rewrite mult_IZR; ring. elim T; intros T1 T2; elim T2; intros T3 T4. absurd (- dExp b < Fexp x1)%Z; auto with zarith. apply IZR_neq; lia. intros I. generalize ClosestTotal; unfold TotalP. intros T; elim T with b' radix p r; auto. 2: rewrite <- H; auto. intros x2 H3'; clear T. case (Zle_or_lt (-(dExp b)) (Fexp x2)); intros. exists x1; split. split; auto. assert (Fbounded b x1);[elim H2; auto|idtac]. split. elim H4; intros; split; try lia. split;[idtac|intros; auto with real]. ring_simplify (x1-x1)%R; rewrite Rabs_R0; apply Rlt_le. apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. split. elim H2; intros T1 T2; elim T1; intros; split; try rewrite <- H; auto with zarith. intros f H4. apply Rle_trans with (Rabs (FtoR radix x2 - r)). elim H2; intros T1 T2; apply T2. elim H3'; intros T1' T2'; elim T1'; intros; split; try rewrite H; auto with zarith. elim H3'; intros T1 T2; apply T2; auto. exists x2; split; auto. split; auto. split;[elim H3'; auto|idtac]. split. replace (x1-x2)%R with ((-(r-x1))+(r-x2))%R;[idtac|ring]. apply Rle_trans with (1:=Rabs_triang (-(r-x1))%R (r-x2)%R). rewrite Rabs_Ropp; apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (2 * (Rabs (r - x1)) + 2 *Rabs (r - x2))%R;[right; ring|idtac]. apply Rle_trans with ( powerRZ radix (- dExp b)+ (/2)*powerRZ radix (- dExp b))%R;[idtac|simpl; right; field]. apply Rplus_le_compat. apply Rle_trans with (Fulp b radix p x1). unfold FtoRradix; apply ClosestUlp; auto. rewrite CanonicFulp; auto. rewrite <- I; unfold FtoR; simpl; right; ring. apply Rle_trans with (Fulp b' radix p x2). unfold FtoRradix; apply ClosestUlp; auto. rewrite <- H; auto. apply Rle_trans with (powerRZ radix (Fexp x2)). unfold Fulp; apply Rle_powerRZ; try lia. apply IZR_le; lia. apply FcanonicLeastExp with radix b' p; try lia. rewrite FnormalizeCorrect; auto with zarith real. elim H3'; auto. apply FnormalizeCanonic; try lia. elim H3'; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (- dExp b));[idtac|right; field; auto with real]. apply Rle_trans with (radix * powerRZ radix (Fexp x2))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. apply Rle_trans with (powerRZ radix (Fexp x2+1)). rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; ring. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. intros H5; absurd ((Fexp x2 < - dExp b)%Z); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz