proposition: Lemma is_pseries_odd_even (a : nat -> R) (x l1 l2 : R) : is_pseries (fun n => a (2*n)%nat) (x^2) l1 -> is_pseries (fun n => a (2*n+1)%nat) (x^2) l2 -> is_pseries a x (l1 + x * l2).
proof: Proof. rewrite 3!is_pseries_R. move => H1 H2. apply filterlim_ext with (fun n => (sum_n (fun k : nat => a (2 * k)%nat * (x ^ 2) ^ k) (Nat.div2 n)) + x * match n with | O => 0 | S n => (sum_n (fun k : nat => a (2 * k + 1)%nat * (x ^ 2) ^ k) (Nat.div2 n)) end). case => [ | n]. rewrite /= !sum_O /= ; ring. case: (Nat.Even_or_Odd n) => Hn. rewrite 3!sum_n_Reals. rewrite -(MyNat.Even_div2 _ Hn) {3}(MyNat.Even_double _ Hn) Nat.double_twice. elim: (Nat.div2 n) => {n Hn} [ | n] ; rewrite ?double_S /sum_f_R0 -/sum_f_R0. rewrite /double /= ; ring. rewrite -pow_mult. replace (2 * S n)%nat with (S (S (Nat.double n))) by (now rewrite -MyNat.double_S Nat.double_twice). replace (S (S (Nat.double n)) + 1)%nat with (S (S (S (Nat.double n)))) by (now rewrite Nat.add_1_r). rewrite !Nat.double_twice; simpl; move => <-; ring. rewrite 3!sum_n_Reals. rewrite -(MyNat.Odd_div2 _ Hn) {3}(MyNat.Odd_double _ Hn) !Nat.double_twice. elim: (Nat.div2 n) => {n Hn} [ | n] ; rewrite ?double_S /sum_f_R0 -/sum_f_R0. rewrite /double /= ; ring. rewrite -?pow_mult. replace (2 * S n)%nat with (S (S (Nat.double n))) by (rewrite -MyNat.double_S Nat.double_twice ; ring). replace (2 * S (S n))%nat with (S (S (S (S (Nat.double n))))) by (rewrite -MyNat.double_S Nat.double_twice ; ring). replace (S (S (Nat.double n)) + 1)%nat with (S (S (S (Nat.double n)))) by ring. rewrite !Nat.double_twice; simpl; move => <-; ring. apply (is_lim_seq_plus' _ _ l1 (x*l2)). apply filterlim_comp with (2:=H1). intros P [N HN]. exists (2*N+1)%nat. intros n Hn; apply HN. apply le_double. apply Nat.add_le_mono_l with 1%nat. rewrite Nat.add_comm. apply Nat.le_trans with (1:=Hn). apply Nat.le_trans with (1+Nat.double (Nat.div2 n))%nat. case (Nat.Even_or_Odd n); intros J. rewrite <- MyNat.Even_double; try exact J. now apply le_S. rewrite <- MyNat.Odd_double; easy. simpl; now rewrite Nat.add_0_r. apply (is_lim_seq_scal_l _ x l2) => //. apply filterlim_ext_loc with (fun n => sum_n (fun k : nat => a (2 * k + 1)%nat * (x ^ 2) ^ k) (Nat.div2 (pred n))). exists 1%nat; intros y; case y. easy. intros n _; reflexivity. apply filterlim_comp with (2:=H2). intros P [N HN]. exists (2*N+2)%nat. intros n Hn; apply HN. apply le_double. apply Nat.add_le_mono_l with 2%nat. rewrite Nat.add_comm. apply Nat.le_trans with (1:=Hn). apply Nat.le_trans with (1+(1+Nat.double (Nat.div2 (pred n))))%nat. case (Nat.Even_or_Odd (pred n)); intros J. rewrite <- MyNat.Even_double; try exact J. case n. simpl; now apply le_S, le_S. intros m; simpl; now apply le_S. rewrite <- MyNat.Odd_double; try exact J. case n; simpl; try easy. now apply le_S. simpl; now rewrite Nat.add_0_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series