proposition: Lemma Cesaro_1 : forall (An:nat -> R) (l:R), Un_cv An l -> Un_cv (fun n:nat => sum_f_R0 An (pred n) / INR n) l.
proof: Proof. intros Bn l H; set (An := fun _:nat => 1). assert (H0 : forall n:nat, 0 < An n). { intro; unfold An; apply Rlt_0_1. } assert (H1 : forall n:nat, 0 < sum_f_R0 An n). { intro; apply tech1. trivial. } assert (H2 : cv_infty (fun n:nat => sum_f_R0 An n)). { unfold cv_infty; intro; destruct (Rle_dec M 0) as [Hle|Hnle]. - exists 0%nat; intros; apply Rle_lt_trans with 0; trivial. - assert (H2 : 0 < M) by auto with real. clear Hnle; set (m := up M); elim (archimed M); intros; assert (H5 : (0 <= m)%Z). + apply le_IZR; unfold m; simpl; left; apply Rlt_trans with M; trivial. + elim (IZN _ H5); intros; exists x; intros; unfold An; rewrite sum_cte; rewrite Rmult_1_l; apply Rlt_trans with (IZR (up M));trivial. apply Rle_lt_trans with (INR x). * rewrite INR_IZR_INZ; fold m; rewrite <- H6; right. trivial. * apply lt_INR; apply Nat.lt_succ_r. trivial. } assert (H3 := Cesaro _ _ _ H H0 H2). unfold Un_cv; unfold Un_cv in H3; intros; elim (H3 _ H4); intros; exists (S x); intros; unfold Rdist; unfold Rdist in H5; apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => An k * Bn k) (pred n) / sum_f_R0 An (pred n) - l)). - right; replace (sum_f_R0 Bn (pred n) / INR n - l) with (sum_f_R0 (fun k:nat => An k * Bn k) (pred n) / sum_f_R0 An (pred n) - l);trivial. unfold Rminus; do 2 rewrite <- (Rplus_comm (- l)); apply Rplus_eq_compat_l. unfold An; replace (sum_f_R0 (fun k:nat => 1 * Bn k) (pred n)) with (sum_f_R0 Bn (pred n)). + rewrite sum_cte; rewrite Rmult_1_l; replace (S (pred n)) with n;trivial. symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.lt_le_trans with (S x);trivial. apply Nat.lt_0_succ. + apply sum_eq; intros; ring. - apply H5; unfold ge; apply le_S_n; replace (S (pred n)) with n;trivial. symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.lt_le_trans with (S x);trivial. apply Nat.lt_0_succ. Qed.
imports: Rbase Rfunctions Rseries SeqProp Rcomplete PartSum AltSeries Binomial Rsigma Rprod Cauchy_prod Alembert Lra