proposition: Lemma sin_fast0_correct : forall prec x, F.toX x = Xreal (toR x) -> (Rabs (toR x) <= /2)%R -> contains (I.convert (sin_fast0 prec x)) (Xreal (sin (toR x))).
proof: Proof. intros prec x Rx Bx. unfold sin_fast0. rewrite sin_sinc. replace (sinc (toR x)) with (1 - (1 - sinc (toR x)))%R by ring. rewrite Rmult_comm. set (xi := I.bnd x x). assert (Ix: contains (I.convert xi) (Xreal (toR x))). unfold xi. rewrite I.bnd_correct, Rx. split ; apply Rle_refl. apply F'.valid_lb_real ; now rewrite F.real_correct, Rx. apply F'.valid_ub_real ; now rewrite F.real_correct, Rx. apply J.mul_correct with (2 := Ix). apply J.sub_correct. now apply I.fromZ_small_correct. set (x2i := I.sqr prec xi). pose (Si := fun x => sum_f_R0 (fun n : nat => ((-1) ^ n / INR (fact (2 * n + 1)) * x ^ (2 * n))%R)). assert (Hexit : forall k powi divi, contains (I.convert powi) (Xreal (toR x ^ (2 * k))) -> contains (I.convert divi) (Xreal (INR (fact (2 * (k + 1) + 1)))) -> contains (I.convert (I.bnd F.zero (I.upper (I.div prec (I.mul prec powi x2i) divi)))) (Xreal ((-1) ^ (k + 1) * (sinc (toR x) - Si (toR x) k)))). intros k powi divi Hpow Hdiv. assert (Hne : not_empty (I.convert (I.div prec (I.mul prec powi x2i) divi))). { exists ((F.toR x ^ (2 * k) * (F.toR x * F.toR x)) / INR (fact (2 * (k + 1) + 1)))%R. now apply J.div_correct; [apply J.mul_correct; [|apply J.sqr_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 + 1) * (sinc (toR x) - Si (toR x) k) <= toR x ^ (2 * (k + 1)) / INR (fact (2 * (k + 1) + 1)))%R). replace (Si (toR x) k) with (sum_f_R0 (tg_alt (fun n => / INR (fact (2 * n + 1)) * toR x ^ (2 * n))%R) k). unfold Rdiv. rewrite (Rmult_comm (toR x ^ _)). replace (k + 1) with (S k) by ring. apply alternated_series_ineq'. apply Un_decreasing_sinc. lra. destruct (Req_dec (toR x) 0) as [Zx|Zx]. rewrite Zx. intros eps Heps. exists 1%nat. intros n Hn. rewrite pow_ne_zero by (clear -Hn ; lia). unfold R_dist, Rminus. now rewrite Rmult_0_r, Rplus_opp_r, Rabs_R0. rewrite <- (Rmult_0_l (/toR x)). apply Un_cv_ext with (fun n : nat => (/ INR (fact (2 * n + 1)) * toR x ^ (2 * n + 1) * / toR x)%R). intros n. rewrite pow_add. field. split. apply Rgt_not_eq. apply INR_fact_lt_0. exact Zx. apply CV_mult. apply (Un_cv_subseq (fun n => (/ INR (fact n) * toR x ^ n)%R)). clear ; intros n ; lia. eapply Un_cv_ext. intros n. apply Rmult_comm. apply cv_speed_pow_fact. intros eps Heps. exists 0. intros _ _. unfold R_dist, Rminus. now rewrite Rplus_opp_r, Rabs_R0. unfold sinc. case exist_sin. intro l. change (projT1 _) with l. apply Un_cv_ext. intros n. apply sum_eq. intros i _. unfold sin_n, tg_alt. rewrite pow_Rsqr. apply Rmult_assoc. unfold Si, tg_alt. apply sum_eq. intros i _. apply sym_eq, Rmult_assoc. apply (conj (proj1 A)). assert (Hx2 := J.sqr_correct prec _ _ Ix). assert (H1 := J.mul_correct prec _ _ _ _ Hpow Hx2). 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. replace (2 * (k + 1)) with (2 * k + 2) by ring. now rewrite pow_add, Rsqr_pow2. generalize (F.scale c1 (F.ZtoS (Z.neg (F.prec prec)))) (Pos.to_nat (F.prec prec)). intros thre n. replace 1%R with (Si (toR x) 0) by (unfold Si ; simpl ; field). refine (_ (I.fromZ_small_correct 1 _) (I.fromZ_small_correct 6 _) (I.fromZ_small_correct 4 _)) ; [|easy..]. fold i1 i6 i4. generalize i1 i6 i4. intros powi divi facti. change 1%R with (pow (toR x) (2 * 0)). change 4%Z with (Z_of_nat (2 * (0 + 1) + 2)). change 6%Z with (Z_of_nat (fact (2 * (0 + 1) + 1))). rewrite <- 2!INR_IZR_INZ. replace (Si (toR x) 0%nat - sinc (toR x))%R with ((-1) * 1 * (sinc (toR x) - Si (toR x) 0%nat))%R by ring. change (-1 * 1)%R with (pow (-1) (0 + 1)). rewrite <- (Nat.sub_diag n) at 2 4 8 11 13. 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 cos_fast0_aux. cut (contains (I.convert (I.bnd F.zero (I.upper (I.div prec (I.mul prec powi x2i) divi)))) (Xreal ((-1) ^ (n - 0 + 1) * (sinc (toR x) - Si (toR x) (n - 0))))). now destruct F'.cmp. now apply Hexit. simpl cos_fast0_aux. set (powi' := I.mul prec powi x2i). set (divi' := I.mul prec divi (I.mul prec facti (I.add prec facti i1))). set (facti' := I.add prec facti i2). specialize (IHm powi' divi' facti'). assert (H: forall p, n - S m + S p = n - m + p). intros p. clear -Hm ; lia. cut (contains (I.convert (I.sub prec (I.div prec powi' divi) (cos_fast0_aux prec thre powi' x2i facti' divi' m))) (Xreal ((-1) ^ (n - S m + 1) * (sinc (toR x) - Si (toR x) (n - S m))))). case F'.cmp ; try easy. intros H'. now apply Hexit. replace ((-1) ^ (n - S m + 1) * (sinc (toR x) - Si (toR x) (n - S m)%nat))%R with ((-1) ^ (n - S m + 1) * (-1) ^ S (n - S m) * (toR x) ^ (2 * S (n - S m)) * / INR (fact (2 * S (n - S m) + 1)) - (((-1) * (-1) ^ (n - S m + 1)) * (sinc (toR x) - (Si (toR x) (n - S m)%nat + ((-1) ^ S (n - S m) * / INR (fact (2 * S (n - S m) + 1)) * (toR x) ^ (2 * S (n - S m)))))))%R by ring. assert (Hpow': contains (I.convert powi') (Xreal (toR x ^ (2 * (n - S m + 1))))). replace (2 * (n - S m + 1)) with (2 * (n - S m) + 2) by ring. rewrite pow_add, <- Rsqr_pow2. apply J.mul_correct with (1 := Hpow). now apply J.sqr_correct. apply J.sub_correct. rewrite <- pow_add. replace (n - S m + 1 + S (n - S m)) with (2 * (n - S m + 1)) by (clear -Hm ; lia). rewrite pow_1_even, Rmult_1_l. replace (S (n - S m)) with (n - S m + 1) by now rewrite Nat.add_comm. now apply J.div_correct. evar_last. apply IHm. clear -Hm ; lia. now rewrite <- (Nat.add_0_r (n - m)), <- H. rewrite <- H. replace (2 * (n - S m + 2) + 1) with (S (S (2 * (n - S m + 1) + 1))) by ring. rewrite 2!fact_simpl. rewrite 2!mult_INR, <- Rmult_assoc, Rmult_comm. apply J.mul_correct with (1 := Hdiv). rewrite Rmult_comm. apply J.mul_correct. now rewrite <- Nat.add_1_r, <- Nat.add_assoc. replace (S (S (2 * (n - S m + 1) + 1))) with (2 * (n - S m + 1) + 2 + 1) by ring. rewrite plus_INR. apply J.add_correct with (1 := Hfact). now apply I.fromZ_small_correct. rewrite <- H. replace (2 * (n - S m + 2) + 2) with (2 * (n - S m + 1) + 2 + 2) by ring. rewrite plus_INR. apply J.add_correct with (1 := Hfact). now apply I.fromZ_small_correct. apply f_equal. change (Si (toR x) (n - S m)%nat + (-1) ^ S (n - S m) * / INR (fact (2 * S (n - S m) + 1)) * toR x ^ (2 * S (n - S m)))%R with (Si (toR x) (S (n - S m))). change (-1 * (-1) ^ (n - S m + 1))%R with ((-1) ^ (S (n - S m + 1)))%R. rewrite <- plus_Sn_m. now rewrite <-Nat.sub_succ_l. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float