proposition: Lemma ulp_sqr_ulp_lt: forall u, 0 < u -> (u < sqrt (IZR (radix_val beta)) * bpow (mag beta u-1)) -> ulp_flx (u * u) + ulp_flx u * ulp_flx u / 2 < 2 * u * ulp_flx u.
proof: Proof. Proof with auto with typeclass_instances. intros u Hu. rewrite 2!ulp_neq_0. 2: now apply Rgt_not_eq. 2: now apply Rgt_not_eq, Rmult_lt_0_compat. unfold cexp, FLX_exp. destruct (mag beta u) as (e,He); simpl. intros Cu. assert (He2:(bpow (e - 1) <= u < bpow e)). rewrite <- (Rabs_right u). apply He; auto with real. apply Rle_ge; now left. clear He. destruct (mag beta (u*u)) as (i,Hi); simpl. assert (Hi2:(bpow (i - 1) <= u*u < bpow i)). rewrite <- (Rabs_right (u*u)). apply Hi; auto with real. apply Rle_ge; apply Rmult_le_pos; auto with real. clear Hi. assert (i=2*e-1)%Z. assert (2*e-2 < i /\ i-1 < 2*e-1)%Z;[idtac|lia]. split;apply lt_bpow with beta. apply Rle_lt_trans with (2:=proj2 Hi2). replace (2*e-2)%Z with ((e-1)+(e-1))%Z by ring. rewrite bpow_plus. apply Rmult_le_compat; try apply bpow_ge_0; apply He2. apply Rle_lt_trans with (1:=proj1 Hi2). apply Rlt_le_trans with ((sqrt (IZR beta) * bpow (e - 1))*(sqrt (IZR beta) * bpow (e - 1))). apply Rlt_trans with ((sqrt (IZR beta) * bpow (e - 1))*u). now apply Rmult_lt_compat_r. apply Rmult_lt_compat_l. apply Rlt_trans with (1:=Hu); assumption. assumption. right; apply trans_eq with ((sqrt (IZR beta) * sqrt (IZR beta)) *(bpow (e - 1) * bpow (e - 1)));[ring|idtac]. rewrite <- bpow_plus. rewrite sqrt_sqrt. replace (IZR beta) with (bpow 1). rewrite <- bpow_plus. apply f_equal; ring. apply bpow_1. generalize (radix_gt_0 beta); intros. left; now apply IZR_lt. rewrite H. apply Rlt_le_trans with (2 * bpow (e-1) * bpow (e - prec)). change 2%R with (1 + 1)%R. rewrite Rmult_assoc, Rmult_plus_distr_r, Rmult_1_l. rewrite <- 2!bpow_plus. replace (e - 1 + (e - prec))%Z with (2 * e - 1 - prec)%Z by ring. apply Rplus_lt_compat_l. apply Rmult_lt_reg_l with 2%R; auto with real. apply Rle_lt_trans with (bpow (e - prec + (e - prec))). right; field. apply Rlt_le_trans with (1*bpow (2 * e - 1 - prec)). rewrite Rmult_1_l; apply bpow_lt. lia. apply Rmult_le_compat_r; auto with real. apply bpow_ge_0. apply Rmult_le_compat_r. apply bpow_ge_0. apply Rmult_le_compat_l; auto with real. apply He2. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)