proposition: Lemma sqrt_error_N_round_ex_derive : forall x rx, (exists eps, (Rabs eps <= 1 - 1 / sqrt (1 + 2 * u_ro))%R /\ rx = (x * (1 + eps))%R) -> exists eps, (Rabs eps <= sqrt (1 + 2 * u_ro) - 1)%R /\ x = (rx * (1 + eps))%R.
proof: Proof. intros x rx (d, (Bd, Hd)). assert (H := Rabs_le_inv _ _ Bd). assert (H' := om1ds1p2u_ro_le_u_rod1pu_ro). assert (H'' := u_rod1pu_ro_le_u_ro beta prec). assert (H''' := u_ro_lt_1 beta prec prec_gt_0_). assert (Hpos := s1p2u_rom1_pos). destruct (Req_dec rx 0) as [Zfx|Nzfx]. { exists 0%R; split; [now rewrite Rabs_R0|]. rewrite Rplus_0_r, Rmult_1_r, Zfx; rewrite Zfx in Hd. destruct (Rmult_integral _ _ (sym_eq Hd)); lra. } destruct (Req_dec x 0) as [Zx|Nzx]. { now exfalso; revert Hd; rewrite Zx; rewrite Rmult_0_l. } set (d' := ((x - rx) / rx)%R). assert (Hd' : (Rabs d' <= sqrt (1 + 2 * u_ro) - 1)%R). { unfold d'; rewrite Hd. replace (_ / _)%R with (- d / (1 + d))%R; [|now field; split; lra]. unfold Rdiv; rewrite Rabs_mult, Rabs_Ropp. rewrite (Rabs_pos_eq (/ _)); [|apply Rlt_le, Rinv_0_lt_compat; lra]. apply (Rmult_le_reg_r (1 + d)); [lra|]. rewrite Rmult_assoc, Rinv_l, Rmult_1_r; [|lra]. apply (Rle_trans _ _ _ Bd). apply (Rle_trans _ ((sqrt (1 + 2 * u_ro) - 1) * (1/sqrt (1 + 2 * u_ro)))); [right; field|apply Rmult_le_compat_l]; lra. } now exists d'; split; [exact Hd'|]; unfold d'; field. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error