proposition: Theorem ErrFmaApprox_1_aux: Fnormal radix bo z -> Fnormal radix bo w -> (Rabs (z+w-(a*x+b)) <= (3*radix/2+/2)*powerRZ radix (2-2*p)*Rabs z)%R.
proof: Proof. intros M1 M2. apply Rle_trans with (3*powerRZ radix (2-2*p)*Rabs z)%R. assert (FtoRradix t=uh-z)%R. elim tBounded with bo radix p a x b ph pl uh z; auto. fold FtoRradix; intros t' T; elim T; intros T1 T2; clear T. rewrite <- T2; unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite T2; auto. assert (Rabs (z + w - (a * x + b)) <= (Fulp bo radix p w))%R. replace (z + w - (a * x + b))%R with (-((t+v)-w))%R. 2: rewrite H; replace (a*x)%R with (a*x-0)%R; auto with real; rewrite <- Case1. 2: rewrite ulDef; replace (FtoRradix v) with (FtoRradix pl). 2: rewrite plDef; ring. 2: unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. 2: apply ClosestRoundedModeP with p; auto with zarith. 2: replace (FtoR radix pl) with (pl+ul)%R; auto;fold FtoRradix; rewrite Case1; auto with real. rewrite Rabs_Ropp; apply Rlt_le; unfold FtoRradix. apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Rle_trans with (1:=H0). apply Rle_trans with (Rabs (FtoR radix w) * powerRZ radix (Z.succ (- p)))%R. apply FulpLe2; auto with zarith. elim M2; auto. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. fold FtoRradix; apply Rle_trans with ((3*(powerRZ radix (Z.succ (-p))*Rabs z))* powerRZ radix (Z.succ (- p)))%R. 2: unfold Z.succ; replace (2-2*p)%Z with (1+1+-p+-p)%Z; auto with zarith. 2: repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; right; ring. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (3*Fulp bo radix p z)%R. 2: apply Rmult_le_compat_l; auto with real zarith. 2: rewrite Rmult_comm; unfold FtoRradix; apply FulpLe2; auto with zarith. 2: elim M1; auto. 2: rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. assert (0 < 1- powerRZ radix (Z.succ (- p)))%R. assert (powerRZ radix (Z.succ (- p)) < 1)%R; auto with real. apply Rlt_le_trans with (powerRZ radix (Z.succ (-1))); unfold Z.succ; auto with zarith real. apply Rlt_powerRZ; try apply IZR_lt; lia. now apply Rlt_Rminus. apply Rmult_le_reg_l with (1- powerRZ radix (Z.succ (- p)))%R; auto with real. apply Rle_trans with (Fulp bo radix p z). apply Rplus_le_reg_l with (powerRZ radix (Z.succ (- p))*Rabs w)%R. apply Rle_trans with (Rabs w);[right; ring|idtac]. pattern (FtoRradix w) at 1; replace (FtoRradix w) with ((z+w-(a*x+b))+((a*x+b)-z))%R; [idtac|ring]. apply Rle_trans with (Rabs (z+w-(a*x+b))+Rabs (((a*x+b)-z)))%R; [apply Rabs_triang|idtac]. apply Rplus_le_compat. apply Rle_trans with (1:=H0). rewrite Rmult_comm; unfold FtoRradix; apply FulpLe2; auto with zarith. elim M2; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. apply Rlt_le; unfold FtoRradix. apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Rle_trans with (1*Fulp bo radix p z)%R; auto with real. unfold Fulp; rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rplus_le_reg_l with (-1+3*powerRZ radix (Z.succ (- p)))%R. apply Rle_trans with (3 * powerRZ radix (Z.succ (- p)))%R;[right; ring|idtac]. ring_simplify ( -1 + 3 * powerRZ radix (Z.succ (- p)) + (1 - powerRZ radix (Z.succ (- p))) * 3)%R. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_trans with (powerRZ radix (2+Z.succ (-p))); auto with real zarith. 2: unfold Z.succ; apply Rle_powerRZ; auto with real zarith. 2: apply IZR_le; lia. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. ring_simplify (radix*1)%R; apply Rle_trans with 4%R. auto with real zarith. rewrite <- mult_IZR; apply IZR_le. apply Z.le_trans with (2*2)%Z. auto with zarith. apply Zmult_le_compat; auto with zarith. simpl; auto with real. apply Rmult_le_compat_r; auto with real. apply Rabs_pos. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (3 * radix / 2)%R; auto with real. apply Rmult_le_reg_l with (IZR 2); auto with real zarith. apply Rle_trans with (radix*3)%R;[apply Rmult_le_compat_r; auto with real zarith| right; simpl; field; auto with real]. apply IZR_le; lia. apply Rle_trans with (3 * radix / 2+0)%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz