proposition: Lemma Datan_is_datan : forall (N : nat) (x : R), -1 <= x -> x < 1 -> derivable_pt_lim (fun x => sum_f_R0 (tg_alt (Ratan_seq x)) N) x (sum_f_R0 (tg_alt (Datan_seq x)) N).
proof: Proof. assert (Tool : forall N, (-1) ^ (S (2 * N)) = - 1). { intro n ; induction n. { simpl ; field. } replace ((-1) ^ S (2 * S n)) with ((-1) ^ 2 * (-1) ^ S (2*n)). { rewrite IHn ; field. } rewrite <- pow_add. replace (2 + S (2 * n))%nat with (S (2 * S n))%nat. { reflexivity. } lia. } intros N x x_lb x_ub. induction N. { unfold Datan_seq, Ratan_seq, tg_alt ; simpl. intros eps eps_pos. elim (derivable_pt_lim_id x eps eps_pos) ; intros delta Hdelta ; exists delta. intros h hneq h_b. replace (1 * ((x + h) * 1 / 1) - 1 * (x * 1 / 1)) with (id (x + h) - id x). { rewrite Rmult_1_r. apply Hdelta ; assumption. } unfold id ; field ; assumption. } intros eps eps_pos. assert (eps_3_pos : (eps/3) > 0) by lra. elim (IHN (eps/3) eps_3_pos) ; intros delta1 Hdelta1. assert (Main : derivable_pt_lim (fun x =>tg_alt (Ratan_seq x) (S N)) x ((tg_alt (Datan_seq x)) (S N))). { clear -Tool ; intros eps' eps'_pos. elim (derivable_pt_lim_pow x (2 * (S N) + 1) eps' eps'_pos) ; intros delta Hdelta ; exists delta. intros h h_neq h_b ; unfold tg_alt, Ratan_seq, Datan_seq. replace (((-1) ^ S N * ((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1)) - (-1) ^ S N * (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h - (-1) ^ S N * x ^ (2 * S N)) with (((-1)^(S N)) * ((((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1)) - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h - x ^ (2 * S N))) by (field ; split ; [apply Rgt_not_eq |] ; intuition). rewrite Rabs_mult ; rewrite pow_1_abs ; rewrite Rmult_1_l. replace (((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1) - x ^ (2 * S N + 1) / INR (2 * S N + 1)) / h - x ^ (2 * S N)) with ((/INR (2* S N + 1)) * (((x + h) ^ (2 * S N + 1) - x ^ (2 * S N + 1)) / h - INR (2 * S N + 1) * x ^ pred (2 * S N + 1))). { rewrite Rabs_mult. case (Req_dec (((x + h) ^ (2 * S N + 1) - x ^ (2 * S N + 1)) / h - INR (2 * S N + 1) * x ^ pred (2 * S N + 1)) 0) ; intro Heq. { rewrite Heq ; rewrite Rabs_R0 ; rewrite Rmult_0_r ; assumption. } apply Rlt_trans with (r2:=Rabs (((x + h) ^ (2 * S N + 1) - x ^ (2 * S N + 1)) / h - INR (2 * S N + 1) * x ^ pred (2 * S N + 1))). 2:{ apply Hdelta; assumption. } rewrite <- Rmult_1_l ; apply Rmult_lt_compat_r. { apply Rabs_pos_lt ; assumption. } rewrite Rabs_right. { replace 1 with (/1) by field. apply Rinv_0_lt_contravar. { lra. } apply lt_1_INR; lia. } apply Rgt_ge ; replace (INR (2 * S N + 1)) with (INR (2*S N) + 1) ; [apply RiemannInt.RinvN_pos | ]. replace (2 * S N + 1)%nat with (S (2 * S N))%nat by lia. rewrite S_INR ; reflexivity. } rewrite Rmult_minus_distr_l. replace (/ INR (2 * S N + 1) * (INR (2 * S N + 1) * x ^ pred (2 * S N + 1))) with (x ^ (2 * S N)). 2:{ clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by lia. field ; apply Rgt_not_eq ; intuition. } unfold Rminus ; rewrite Rplus_comm. replace (((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1) + - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h + - x ^ (2 * S N)) with (- x ^ (2 * S N) + (((x + h) ^ (2 * S N + 1) / INR (2 * S N + 1) + - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h)) by intuition. apply Rplus_eq_compat_l. field. split ; [apply Rgt_not_eq|] ; intuition. } elim (Main (eps/3) eps_3_pos) ; intros delta2 Hdelta2. destruct delta1 as (delta1, delta1_pos) ; destruct delta2 as (delta2, delta2_pos). pose (mydelta := Rmin delta1 delta2). assert (mydelta_pos : mydelta > 0). { unfold mydelta ; rewrite Rmin_Rgt ; split ; assumption. } pose (delta := mkposreal mydelta mydelta_pos) ; exists delta ; intros h h_neq h_b. clear Main IHN. unfold Rminus at 1. apply Rle_lt_trans with (r2:=eps/3 + eps / 3). { assert (Temp : (sum_f_R0 (tg_alt (Ratan_seq (x + h))) (S N) - sum_f_R0 (tg_alt (Ratan_seq x)) (S N)) / h + - sum_f_R0 (tg_alt (Datan_seq x)) (S N) = ((sum_f_R0 (tg_alt (Ratan_seq (x + h))) N - sum_f_R0 (tg_alt (Ratan_seq x)) N) / h) + (- sum_f_R0 (tg_alt (Datan_seq x)) N) + ((tg_alt (Ratan_seq (x + h)) (S N) - tg_alt (Ratan_seq x) (S N)) / h - tg_alt (Datan_seq x) (S N))). { simpl ; field ; intuition. } apply Rle_trans with (r2:= Rabs ((sum_f_R0 (tg_alt (Ratan_seq (x + h))) N - sum_f_R0 (tg_alt (Ratan_seq x)) N) / h + - sum_f_R0 (tg_alt (Datan_seq x)) N) + Rabs ((tg_alt (Ratan_seq (x + h)) (S N) - tg_alt (Ratan_seq x) (S N)) / h - tg_alt (Datan_seq x) (S N))). { rewrite Temp ; clear Temp ; apply Rabs_triang. } apply Rplus_le_compat ; apply Rlt_le ; [apply Hdelta1 | apply Hdelta2] ; intuition ; apply Rlt_le_trans with (r2:=delta) ; intuition unfold delta, mydelta. { apply Rmin_l. } apply Rmin_r. } lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia