proposition: Lemma expn_fast0_correct : forall prec x, F.toX x = Xreal (toR x) -> (0 <= toR x <= /2)%R -> contains (I.convert (expn_fast0 prec x)) (Xreal (exp (- toR x))).
proof: Proof. intros prec x Rx Bx. unfold expn_fast0. replace (exp (-toR x)) with (1 - (toR x - (- (1 - toR x) + exp (-toR x))))%R by ring. apply J.sub_correct. now apply I.fromZ_small_correct. set (xi := I.bnd x x). assert (Ix: contains (I.convert xi) (Xreal (toR x))). unfold xi. rewrite I.bnd_correct, Rx. 2: now apply I.valid_lb_real; rewrite Rx. 2: now apply I.valid_ub_real; rewrite Rx. split ; apply Rle_refl. apply J.sub_correct with (1 := Ix). assert (Hexit : forall k powi divi, contains (I.convert powi) (Xreal (toR x ^ (k + 1))) -> contains (I.convert divi) (Xreal (INR (fact (k + 2)))) -> contains (I.convert (I.bnd F.zero (I.upper (I.div prec (I.mul prec powi xi) divi)))) (Xreal ((-1) ^ k * (exp (- toR x) + - E1 (- toR x) (k + 1))))). intros k powi divi Hpow Hdiv. assert (Hne : not_empty (I.convert (I.div prec (I.mul prec powi xi) divi))). { exists ((F.toR x ^ (k + 1) * F.toR x)/ INR (fact (k + 2)))%R. now apply J.div_correct; [apply J.mul_correct|]. } rewrite I.bnd_correct. 2: now apply I.valid_lb_real; rewrite F.zero_correct. 2: now apply I.valid_ub_upper. rewrite F.zero_correct, I.upper_correct by easy. assert (A: (0 <= (-1) ^ k * (exp (- toR x) + - E1 (- toR x) (k + 1)) <= toR x ^ (k + 2) / INR (fact (k + 2)))%R). replace ((-1) ^ k)%R with ((-1) * ((-1) * (-1) ^ k))%R by ring. change ((-1) * ((-1) * (-1) ^ k))%R with ((-1) ^ (S (S k)))%R. unfold Rdiv. rewrite (Rmult_comm (toR x ^ (k + 2))). replace (E1 (- toR x) (k + 1)) with (sum_f_R0 (tg_alt (fun n => / INR (fact n) * toR x ^ n)%R) (k + 1)). rewrite <- (plus_n_Sm _ 1). replace (S k) with (k + 1) by ring. apply alternated_series_ineq'. apply Un_decreasing_exp. split. apply Bx. lra. eapply Un_cv_ext. intros n. apply Rmult_comm. apply cv_speed_pow_fact. generalize (E1_cvg (- toR x)). apply Un_cv_ext. intros n. unfold E1, tg_alt. apply sum_eq. intros i _. rewrite (Rmult_comm _ (toR x ^ i)), <- Rmult_assoc. rewrite <- Rpow_mult_distr. rewrite Rmult_comm. apply (f_equal (fun v => (v ^ i * _)%R)). ring. unfold E1, tg_alt. apply sum_eq. intros i _. unfold Rdiv. rewrite Rmult_comm, Rmult_assoc. rewrite <- Rpow_mult_distr. apply (f_equal (fun v => (_ * v ^ i)%R)). ring. apply (conj (proj1 A)). assert (H1 := J.mul_correct prec _ _ _ _ Hpow Ix). assert (H2 := J.div_correct prec _ _ _ _ H1 Hdiv). destruct (I.convert (I.div prec _ _)) as [|l [|u]] ; try easy. apply Rle_trans with (1 := proj2 A). apply Rle_trans with (2 := proj2 H2). apply Req_le, Rmult_eq_compat_r. rewrite <- plus_n_Sm. apply Rmult_comm. generalize (F.scale c1 (F.ZtoS (Z.neg (F.prec prec)))) (Pos.to_nat (F.prec prec)). intros thre n. replace (1 - toR x)%R with (E1 (- toR x) (0 + 1)) by (unfold E1 ; simpl ; field). refine (_ Ix (I.fromZ_small_correct 2 _) (I.fromZ_small_correct 3 _)) ; [|easy..]. fold i2 i3. generalize i2 i3. generalize xi at 1 2. intros powi divi facti. rewrite <- (pow_1 (toR x)) at 1. rewrite Rplus_comm. change 1 with (0 + 1) at 1. change 3%Z with (Z_of_nat (0 + 3)). change 2%Z with (Z_of_nat (fact (0 + 2))). rewrite <- 2!INR_IZR_INZ. rewrite <- (Rmult_1_l (_ + _)). change 1%R with ((-1)^0)%R. rewrite <- (Nat.sub_diag n) at 1 3 5 7 8. generalize (Nat.le_refl n). generalize n at 1 4 6 8 9 11 13. intros m. revert powi divi facti. induction m as [|m IHm] ; intros powi divi facti Hm Hpow Hdiv Hfact. simpl expn_fast0_aux. cut (contains (I.convert (I.bnd F.zero (I.upper (I.div prec (I.mul prec powi xi) divi)))) (Xreal ((-1) ^ (n - 0) * (exp (- toR x) + - E1 (- toR x) (n - 0 + 1))))). now destruct F'.cmp. now apply Hexit. simpl expn_fast0_aux. set (powi' := I.mul prec powi xi). set (divi' := I.mul prec divi facti). set (facti' := I.add prec facti i1). specialize (IHm powi' divi' facti'). assert (H: forall p, n - m + p = n - S m + p + 1). intros p. clear -Hm ; lia. cut (contains (I.convert (I.sub prec (I.div prec powi' divi) (expn_fast0_aux prec thre powi' xi facti' divi' m))) (Xreal ((-1) ^ (n - S m) * (exp (- toR x) + - E1 (- toR x) (n - S m + 1))))). case F'.cmp ; try easy. intros H'. now apply Hexit. replace ((-1) ^ (n - S m) * (exp (- toR x) + - E1 (- toR x) (n - S m + 1)))%R with ((toR x) ^ (n - m + 1) * / INR (fact (n - m + 1)) - (((-1) * (-1) ^ (n - S m)) * (exp (- toR x) + - E1 (- toR x) (n - S m + 1)) + / INR (fact (n - m + 1)) * (toR x) ^ (n - m + 1)))%R by ring. change (-1 * (-1) ^ (n - S m))%R with ((-1) ^ (S (n - S m)))%R. rewrite <-Nat.sub_succ_l with (1 := Hm). simpl (S n - S m). assert (Hpow': contains (I.convert powi') (Xreal (toR x ^ (n - m + 1)))). rewrite H. rewrite pow_add, pow_1. now apply J.mul_correct. apply J.sub_correct. apply J.div_correct with (1 := Hpow'). now rewrite H, <-Nat.add_assoc. evar_last. apply IHm. clear -Hm ; lia. exact Hpow'. rewrite H. rewrite Nat.add_comm, fact_simpl. rewrite Nat.mul_comm, mult_INR. apply J.mul_correct with (1 := Hdiv). now rewrite plus_n_Sm. rewrite H. rewrite plus_INR. apply J.add_correct with (1 := Hfact). now apply I.fromZ_small_correct. apply f_equal. rewrite 2!Rmult_plus_distr_l. rewrite Rplus_assoc. apply f_equal. rewrite <- plus_n_Sm at 1. unfold E1. change (sum_f_R0 (fun k : nat => / INR (fact k) * (- toR x) ^ k) (S (n - m + 0)))%R with (sum_f_R0 (fun k : nat => / INR (fact k) * (- toR x) ^ k) (n - m + 0) + / INR (fact (S (n - m + 0))) * (- toR x) ^ (S (n - m + 0)))%R. rewrite H, <-Nat.add_assoc at 1. rewrite Ropp_plus_distr, Rmult_plus_distr_l. apply f_equal. rewrite <- Ropp_mult_distr_r_reverse. rewrite (Rmult_comm (_ ^ _)), Rmult_assoc. rewrite plus_n_Sm. apply f_equal. replace (- (- toR x) ^ (n - m + 1) * (-1) ^ (n - m))%R with ((- toR x) ^ (n - m + 1) * ((-1) * (-1) ^ (n - m)))%R by ring. change (-1 * (-1) ^ (n - m))%R with ((-1) ^ (S (n - m)))%R . rewrite <- plus_n_Sm, <- plus_n_O. rewrite <- Rpow_mult_distr. now replace (- toR x * -1)%R with (toR x) by ring. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float