proposition: Theorem cesaro_transform : forall (l : IR) (x : nat -> IR) (y : nat -> IR) (H1 : Cauchy_Lim_prop2 x l) (H2 : seq_pos y) (H3 : seq_inf_sum y), Cauchy_Lim_prop2 (fun n : nat => seq_part_sum (fun k : nat => x k [*] y k) (S n) [/](seq_part_sum y (S n)) [//] (seq_pos_imp_ap_zero y H2 n)) l.
proof: Proof. unfold Cauchy_Lim_prop2. intros. assert (H4 : [0] [<] eps[/]TwoNZ). apply pos_div_two. auto. assert ({N : nat | forall m, N <= m -> AbsSmall (eps[/]TwoNZ) ((x m) [-] l) }). apply (H1 (eps[/]TwoNZ) H4). destruct X0 as [N1 H5]. set (C := seq_part_sum (fun k : nat => y k [*] (x k [-] l)) (S N1)); assert (H7 : { N : nat | forall m : nat, N <= m -> AbsSmall (eps[/]TwoNZ) (C [/](seq_part_sum y (S m)) [//] (seq_pos_imp_ap_zero y H2 m))}). apply (seq_inf_sum_imp_div_small y H3 H2 C (eps[/]TwoNZ) H4). destruct H7 as [N2 H7]. exists (S (Nat.max (S N1) N2)). intros. astepr (seq_part_sum (fun k : nat => y k [*] (x k [-] l)) (S m)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m). 2: apply (algebraic_transform1 l x y H2 m). astepr ((seq_part_sum (fun k : nat => y k [*] (x k [-] l)) (S N1)[+] Sum (S N1) m (fun k : nat => y k [*] (x k [-] l)) )[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m). 2: apply (algebraic_transform2 l x y H2 m). astepr (((seq_part_sum (fun k : nat => y k [*] (x k [-] l)) (S N1)) [/]seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m) [+] ((Sum (S N1) m (fun k : nat => y k [*] (x k [-] l)))[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m)). apply AbsSmall_eps_div_two. apply H7. eauto with arith. apply AbsSmall_leEq_trans with ((Sum (S N1) m (fun k : nat => y k [*] eps [/]TwoNZ))[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m). astepl (eps[/]TwoNZ [*] (Sum (S N1) m (fun k: nat => y k)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m)). 2: apply algebraic_transform3. astepr (eps[/]TwoNZ[*][1]). apply mult_resp_leEq_lft. cut (AbsSmall [1] (Sum (G:=IR) (S N1) m (fun k : nat => y k)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m)). unfold AbsSmall. tauto. apply seq_inf_sum_ratio_bound. eauto with arith. apply less_leEq; auto. apply algebraic_estimate1; auto. eauto with arith. intros. apply H5. auto with arith. Qed.
imports: CoRN.reals.Series CoRN.reals.PosSeq