proposition: Lemma ps_atanSeq_continuity_pt_1 : forall (N : nat) (x : R), 0 <= x -> x <= 1 -> continuity_pt (fun x => sum_f_R0 (tg_alt (Ratan_seq x)) N) x.
proof: Proof. assert (Sublemma : forall (x:R) (N:nat), sum_f_R0 (tg_alt (Ratan_seq x)) N = x * (comp (fun x => sum_f_R0 (fun n => (fun i : nat => (-1) ^ i / INR (2 * i + 1)) n * x ^ n) N) (fun x => x ^ 2) x)). { intros x N. induction N. { unfold tg_alt, Ratan_seq, comp ; simpl ; field. } simpl sum_f_R0 at 1. rewrite IHN. replace (comp (fun x => sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x ^ n) (S N)) (fun x => x ^ 2)) with (comp (fun x => sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x ^ n) N + (-1) ^ (S N) / INR (2 * (S N) + 1) * x ^ (S N)) (fun x => x ^ 2)) by intuition. unfold comp. rewrite Rmult_plus_distr_l. apply Rplus_eq_compat_l. unfold tg_alt, Ratan_seq. rewrite <- Rmult_assoc. case (Req_dec x 0) ; intro Hyp. { rewrite Hyp ; rewrite pow_i. { rewrite Rmult_0_l ; rewrite Rmult_0_l. unfold Rdiv ; rewrite Rmult_0_l ; rewrite Rmult_0_r ; reflexivity. } intuition. } replace (x * ((-1) ^ S N / INR (2 * S N + 1)) * (x ^ 2) ^ S N) with (x ^ (2 * S N + 1) * ((-1) ^ S N / INR (2 * S N + 1))). { lra. } rewrite Rmult_assoc. replace (x * ((-1) ^ S N / INR (2 * S N + 1) * (x ^ 2) ^ S N)) with (((-1) ^ S N / INR (2 * S N + 1) * (x ^ 2) ^ S N) * x) by ring. rewrite Rmult_assoc. replace ((x ^ 2) ^ S N * x) with (x ^ (2 * S N + 1)). { rewrite Rmult_comm at 1 ; reflexivity. } rewrite <- pow_mult. assert (Temp : forall x n, x ^ n * x = x ^ (n+1)). { intros a n ; induction n. { rewrite pow_O. simpl ; intuition. } simpl ; rewrite Rmult_assoc ; rewrite IHn ; intuition. } rewrite Temp ; reflexivity. } intros N x x_lb x_ub. intros eps eps_pos. assert (continuity_id : continuity id). { apply derivable_continuous ; exact derivable_id. } assert (Temp := continuity_mult id (comp (fun x1 : R => sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x1 ^ n) N) (fun x1 : R => x1 ^ 2)) continuity_id). assert (Temp2 : continuity (comp (fun x1 : R => sum_f_R0 (fun n : nat => (-1) ^ n / INR (2 * n + 1) * x1 ^ n) N) (fun x1 : R => x1 ^ 2))). { apply continuity_comp. { reg. } apply continuity_finite_sum. } elim (Temp Temp2 x eps eps_pos) ; clear Temp Temp2 ; intros alpha T ; destruct T as (alpha_pos, T). exists alpha ; split. { intuition. } intros x0 x0_cond. rewrite Sublemma ; rewrite Sublemma. apply T. intuition. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia