proposition: Lemma Alt_first_term_bound : forall f l N n, Un_decreasing f -> Un_cv f 0 -> Un_cv (sum_f_R0 (tg_alt f)) l -> (N <= n)%nat -> Rdist (sum_f_R0 (tg_alt f) n) l <= f N.
proof: Proof. intros f l. assert (WLOG : forall n P, (forall k, (0 < k)%nat -> P k) -> ((forall k, (0 < k)%nat -> P k) -> P 0%nat) -> P n). { clear. intros [ | n] P Hs Ho;[solve[apply Ho, Hs] | apply Hs; auto with arith]. } intros N; pattern N; apply WLOG; clear N. 2:{ clear WLOG; intros Hyp [ | n] decr to0 cv _. { generalize (alternated_series_ineq f l 0 decr to0 cv). unfold Rdist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r. assert (f 1%nat <= f 0%nat) by apply decr. intros [A B]; rewrite Rabs_pos_eq; lra. } apply Rle_trans with (f 1%nat). { apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv). lia. } solve[apply decr]. } intros [ | N] Npos n decr to0 cv nN. { lia. } assert (decr' : Un_decreasing (fun i => f (S N + i)%nat)). { intros k; replace (S N+S k)%nat with (S (S N+k)) by ring. apply (decr (S N + k)%nat). } assert (to' : Un_cv (fun i => f (S N + i)%nat) 0). { intros eps ep; destruct (to0 eps ep) as [M PM]. exists M; intros k kM; apply PM; lia. } assert (cv' : Un_cv (sum_f_R0 (tg_alt (fun i => ((-1) ^ S N * f(S N + i)%nat)))) (l - sum_f_R0 (tg_alt f) N)). { intros eps ep; destruct (cv eps ep) as [M PM]; exists M. intros n' nM. match goal with |- ?C => set (U := C) end. assert (nM' : (n' + S N >= M)%nat) by lia. generalize (PM _ nM'); unfold Rdist. rewrite (tech2 (tg_alt f) N (n' + S N)). 2:lia. assert (t : forall a b c, (a + b) - c = b - (c - a)) by (intros; ring). rewrite t; clear t; unfold U, Rdist; clear U. replace (n' + S N - S N)%nat with n' by lia. rewrite <- (sum_eq (tg_alt (fun i => (-1) ^ S N * f(S N + i)%nat))). { tauto. } intros i _; unfold tg_alt. rewrite <- Rmult_assoc, <- pow_add, !(Nat.add_comm i); reflexivity. } assert (cv'' : Un_cv (sum_f_R0 (tg_alt (fun i => f (S N + i)%nat))) ((-1) ^ S N * (l - sum_f_R0 (tg_alt f) N))). { apply (Un_cv_ext (fun n => (-1) ^ S N * sum_f_R0 (tg_alt (fun i : nat => (-1) ^ S N * f (S N + i)%nat)) n)). { intros n0; rewrite scal_sum; apply sum_eq; intros i _. unfold tg_alt; ring_simplify; replace (((-1) ^ S N) ^ 2) with 1. { ring. } rewrite <- pow_mult, Nat.mul_comm, pow_mult; replace ((-1) ^2) with 1 by ring. rewrite pow1; reflexivity. } apply CV_mult. { solve[intros eps ep; exists 0%nat; intros; rewrite Rdist_eq; auto]. } assumption. } destruct (even_odd_cor N) as [p [Neven | Nodd]]. - rewrite Neven; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B C]. case (even_odd_cor n) as [p' [neven | nodd]]. + rewrite neven. destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold Rdist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (p <= p')%nat) by lia. assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist). apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l). { unfold Rminus; apply Rplus_le_compat_r; exact t. } match goal with _ : ?a <= l, _ : l <= ?b |- _ => replace (f (S (2 * p))) with (b - a) by (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); lra end. + rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold Rdist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr; [ | lra]. assert (dist : (p <= p')%nat) by lia. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). { unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar. solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)]. } unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc. unfold tg_alt at 2; rewrite pow_1_odd; lra. - rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _]. destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C]. assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring. case (even_odd_cor n) as [p' [neven | nodd]]. + rewrite neven; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold Rdist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (S p < S p')%nat) by lia. apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l). { unfold Rminus; apply Rplus_le_compat_r, (decreasing_prop _ _ _ (CV_ALT_step1 f decr)). lia. } rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even. lra. + rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold Rdist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | lra]. rewrite Ropp_minus_distr. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). { unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr)); lia. } generalize C; rewrite keep, tech5; unfold tg_alt. rewrite <- keep, pow_1_even. lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia