proposition: Lemma err_sqrt_: forall x y e, 0 <= y -> e <= /2 -> err x y e -> bpow (emin+prec-1) < round_flt (sqrt x) -> err (round_flt (sqrt x)) (sqrt y) (eps+(1+eps)*(/2*e+/4*e*e)).
proof: Proof. Proof with auto with typeclass_instances. intros x y e Hy He H Y. replace (round_flt (sqrt x) - sqrt y) with ((round_flt (sqrt x) - sqrt x)+(sqrt x - sqrt y)) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rle_trans with (eps*Rabs (sqrt x)+Rabs (sqrt x - sqrt y)). apply Rplus_le_compat_r. replace eps with (/ 2 * Raux.bpow beta (- prec + 1)). apply relative_error_N_FLT... rewrite Rabs_right. 2: apply Rle_ge, sqrt_pos. case (Rle_or_lt (bpow (emin + prec - 1)) (sqrt x)); intros Y1. assumption. contradict Y; apply Rle_not_lt. apply round_le_generic... apply generic_format_bpow. unfold FLT_exp. replace (emin + prec - 1 + 1 - prec)%Z with emin by ring. rewrite Z.max_l; lia. now left. apply f_equal; apply f_equal; ring. rewrite Rmult_plus_distr_r. apply Rle_trans with (eps*Rabs (sqrt y) + (1+eps)*Rabs (sqrt x - sqrt y)). pattern (sqrt x) at 1; replace (sqrt x) with ((sqrt x-sqrt y)+sqrt y) by ring. apply Rle_trans with (eps * Rabs (sqrt x - sqrt y) + eps*Rabs (sqrt y) + Rabs (sqrt x - sqrt y)). apply Rplus_le_compat_r. rewrite <- Rmult_plus_distr_l. apply Rmult_le_compat_l. apply epsPos. apply Rabs_triang. right; ring. apply Rplus_le_compat_l. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Fourier_util.Rle_zero_pos_plus1, epsPos. case (Req_dec y 0); intros Hy'. replace x with 0. rewrite Hy', sqrt_0, Rminus_0_r, Rabs_R0, Rmult_0_r. now apply Req_le. case (Req_dec x 0). easy. intros H1. absurd (Rabs x = 0). now apply Rabs_no_R0. assert (Rabs x <= 0). replace x with (x-y). replace 0 with (e*Rabs y). exact H. rewrite Hy', Rabs_R0; ring. rewrite Hy'; ring. case H0; try easy. intros K; contradict K. apply Rle_not_lt, Rabs_pos. replace (sqrt x - sqrt y) with (sqrt y*(sqrt (1+(x-y)/y) - 1)). rewrite Rabs_mult, Rmult_comm. apply Rmult_le_compat_r. apply Rabs_pos. assert ((Rabs ((x - y) / y) <= e)). apply Rmult_le_reg_r with (Rabs y). case (Rabs_pos y); [easy|intros H'; contradict H'; apply sym_not_eq; now apply Rabs_no_R0]. apply Rle_trans with (2:=H). rewrite <- Rabs_mult; right. apply f_equal; now field. apply Rle_trans with (Rabs ((x - y) / y) /2 + Rabs ((x - y) / y)*Rabs ((x - y) / y)/4). apply sqrt_var_maj_2. apply Rle_trans with (2:=He); assumption. apply Rplus_le_compat. unfold Rdiv; rewrite Rmult_comm. apply Rmult_le_compat_l; try assumption. auto with real. unfold Rdiv; rewrite Rmult_comm. rewrite Rmult_assoc. apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real. apply Rmult_le_compat; try apply Rabs_pos; try apply H0. rewrite Rmult_minus_distr_l, Rmult_1_r. apply f_equal2;[idtac|reflexivity]. rewrite <- sqrt_mult. apply f_equal. now field. exact Hy. apply Rmult_le_reg_l with y. case Hy; [easy|intros H'; contradict H'; now apply sym_not_eq]. apply Rplus_le_reg_l with (-(x-y)). apply Rle_trans with (-(x-y)). right; ring. apply Rle_trans with (1:=RRle_abs _). rewrite Rabs_Ropp. apply Rle_trans with (1:=H). apply Rle_trans with (1*Rabs y). apply Rmult_le_compat_r. apply Rabs_pos. lra. rewrite Rabs_pos_eq by easy. right; now field. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)