proposition: Lemma pre_cos_bound : forall (a:R) (n:nat), - 2 <= a -> a <= 2 -> cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1)).
proof: Proof. assert (H:(forall (a:R) (n:nat), 0 <= a -> a <= 2 -> cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1))) -> forall (a:R) (n:nat), - 2 <= a -> a <= 2 -> cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1))). { intros; destruct (total_order_T 0 a) as [[Hlt|Heq]|Hgt];try (apply H;lra). assert (0 < - a) by lra. cut (forall (x:R) (n:nat), cos_approx x n = cos_approx (- x) n). { intro; rewrite H3; rewrite (H3 a (2 * (n + 1))%nat); rewrite cos_sym; apply H;lra. } intros; unfold cos_approx; apply sum_eq; intros; unfold cos_term; do 2 rewrite pow_Rsqr; rewrite Rsqr_neg; unfold Rdiv; reflexivity. } intros a n; apply H. intros; unfold cos_approx. rewrite (decomp_sum (cos_term a0) (2 * n0 + 1)). 2:lia. rewrite (decomp_sum (cos_term a0) (2 * (n0 + 1))). 2:lia. replace (cos_term a0 0) with 1. 2:{ unfold cos_term; simpl; unfold Rdiv; rewrite Rinv_1; ring. } assert (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * n0 + 1)) <= cos a0 - 1 /\ cos a0 - 1 <= sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * (n0 + 1))) -> 1 + sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * n0 + 1)) <= cos a0 /\ cos a0 <= 1 + sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * (n0 + 1)))). { intro; elim H2; intros; split; apply Rplus_le_reg_l with (-(1)); rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite (Rplus_comm (-1));assumption. } apply H2. set (Un := fun n:nat => a0 ^ (2 * S n) / INR (fact (2 * S n))). replace (pred (2 * n0 + 1)) with (2 * n0)%nat by lia. replace (pred (2 * (n0 + 1))) with (S (2 * n0)) by lia. replace (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (2 * n0)) with (- sum_f_R0 (tg_alt Un) (2 * n0)). 2:{ replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ]; apply sum_eq; intros; unfold cos_term, Un, tg_alt; change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. } replace (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (S (2 * n0))) with (- sum_f_R0 (tg_alt Un) (S (2 * n0))). 2:{ replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold cos_term, Un, tg_alt; change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. } assert (sum_f_R0 (tg_alt Un) (S (2 * n0)) <= 1 - cos a0 <= sum_f_R0 (tg_alt Un) (2 * n0) -> - sum_f_R0 (tg_alt Un) (2 * n0) <= cos a0 - 1 <= - sum_f_R0 (tg_alt Un) (S (2 * n0))) by lra. apply H3. apply alternated_series_ineq. - unfold Un_decreasing; intro; unfold Un. assert ((2 * S (S n1))%nat = S (S (2 * S n1))) by lia. rewrite H4; replace (a0 ^ S (S (2 * S n1))) with (a0 ^ (2 * S n1) * (a0 * a0)) by (simpl;ring). unfold Rdiv; rewrite Rmult_assoc; apply Rmult_le_compat_l. { apply pow_le; assumption. } apply Rmult_le_reg_l with (INR (fact (S (S (2 * S n1))))). { apply INR_fact_lt_0. } rewrite <- H4; rewrite (Rmult_comm (INR (fact (2 * S (S n1))))); rewrite Rmult_assoc; rewrite Rinv_l. 2:(pose proof (INR_fact_lt_0 (2 * S (S n1)));lra). rewrite Rmult_1_r; rewrite H4; do 2 rewrite fact_simpl; do 2 rewrite mult_INR; repeat rewrite Rmult_assoc; rewrite Rinv_r. 2:(pose proof (INR_fact_lt_0 (2 * S n1));lra). rewrite Rmult_1_r; do 2 rewrite S_INR; rewrite mult_INR; repeat rewrite S_INR; simpl; replace (((0 + 1 + 1) * (INR n1 + 1) + 1 + 1) * ((0 + 1 + 1) * (INR n1 + 1) + 1)) with (4 * INR n1 * INR n1 + 14 * INR n1 + 12); [ idtac | ring ]. apply Rle_trans with 12. { nra. } pose proof (pos_INR n1);nra. - assert (H4 := cv_speed_pow_fact a0); unfold Un; unfold Un_cv in H4; unfold Rdist in H4; unfold Un_cv; unfold Rdist; intros; elim (H4 eps H5); intros N H6; exists N; intros. apply H6; nia. - unfold cos. destruct (exist_cos (Rsqr a0)) as (x,p). unfold cos_in, infinite_sum, Rdist in p; unfold Un_cv, Rdist; intros. destruct (p _ H4) as (N,H6). exists N; intros. replace (sum_f_R0 (tg_alt Un) n1) with (1 - sum_f_R0 (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)). { unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive; repeat rewrite Rplus_assoc; rewrite (Rplus_comm 1); rewrite (Rplus_comm (-(1))); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- Rabs_Ropp; rewrite Ropp_plus_distr; rewrite Ropp_involutive; unfold Rminus in H6; apply H6. lia. } rewrite (decomp_sum (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)). 2:lia. replace (cos_n 0) with 1. 2:{ unfold cos_n; unfold Rdiv; simpl; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. } simpl; rewrite Rmult_1_r; unfold Rminus; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; replace (- sum_f_R0 (fun i:nat => cos_n (S i) * (Rsqr a0 * Rsqr a0 ^ i)) n1) with (-1 * sum_f_R0 (fun i:nat => cos_n (S i) * (Rsqr a0 * Rsqr a0 ^ i)) n1); [ idtac | ring ]; rewrite scal_sum; apply sum_eq; intros; unfold cos_n, Un, tg_alt. replace ((-1) ^ S i) with (- (-1) ^ i) by (simpl;ring). replace (a0 ^ (2 * S i)) with (Rsqr a0 * Rsqr a0 ^ i) by (rewrite pow_Rsqr; reflexivity). unfold Rdiv; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Lia Lra