proposition: Lemma Cesaro : forall (An Bn:nat -> R) (l:R), Un_cv Bn l -> (forall n:nat, 0 < An n) -> cv_infty (fun n:nat => sum_f_R0 An n) -> Un_cv (fun n:nat => sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n) l.
proof: Proof. unfold Un_cv; intros; assert (H3 : forall n:nat, 0 < sum_f_R0 An n). { intro; apply tech1; trivial. } assert (H4 : forall n:nat, sum_f_R0 An n <> 0). { intro; red; intro; assert (H5 := H3 n); rewrite H4 in H5; elim (Rlt_irrefl _ H5). } assert (H5 := cv_infty_cv_0 _ H1); assert (H6 : 0 < eps / 2). { unfold Rdiv; apply Rmult_lt_0_compat. - trivial. - apply Rinv_0_lt_compat; prove_sup. } elim (H _ H6); clear H; intros N1 H; set (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); assert (H7 : exists N : nat, (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2)). { case (Req_dec C 0); intro. - exists 0%nat; intros. rewrite H7; unfold Rdiv; rewrite Rmult_0_l; apply Rmult_lt_0_compat. + trivial. + apply Rinv_0_lt_compat; prove_sup. - assert (H8 : 0 < eps / (2 * Rabs C)). + unfold Rdiv; apply Rmult_lt_0_compat. * trivial. * apply Rinv_0_lt_compat; apply Rmult_lt_0_compat. -- prove_sup. -- apply Rabs_pos_lt;assumption. + elim (H5 _ H8); intros; exists x; intros; assert (H11 := H9 _ H10); unfold Rdist in H11; unfold Rminus in H11; rewrite Ropp_0 in H11; rewrite Rplus_0_r in H11. apply Rle_lt_trans with (Rabs (C / sum_f_R0 An n)). { apply RRle_abs. } unfold Rdiv; rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs C). { apply Rinv_0_lt_compat; apply Rabs_pos_lt;assumption. } rewrite <- Rmult_assoc; rewrite Rinv_l. * rewrite Rmult_1_l; replace (/ Rabs C * (eps * / 2)) with (eps / (2 * Rabs C)). { trivial. } field. apply Rabs_no_R0;assumption. * apply Rabs_no_R0;assumption. } elim H7; clear H7; intros N2 H7; set (N := max N1 N2); exists (S N); intros; unfold Rdist; replace (sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n - l) with (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n / sum_f_R0 An n). 2:{ replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with (sum_f_R0 (fun k:nat => An k * Bn k) n + sum_f_R0 (fun k:nat => An k * - l) n). - rewrite <- (scal_sum An n (- l)); field. trivial. - rewrite <- plus_sum; apply sum_eq; intros; ring. } assert (H9 : (N1 < n)%nat). { apply Nat.lt_le_trans with (S N). - apply Nat.lt_succ_r; unfold N; apply Nat.le_max_l. - trivial. } rewrite (tech2 (fun k:nat => An k * (Bn k - l)) _ _ H9); unfold Rdiv; rewrite Rmult_plus_distr_r; apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1 / sum_f_R0 An n) + Rabs (sum_f_R0 (fun i:nat => An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l)) (n - S N1) / sum_f_R0 An n)). { apply Rabs_triang. } rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. { unfold Rdiv; rewrite Rabs_mult; fold C; rewrite Rabs_right. - apply (H7 n); apply Nat.le_trans with (S N). + apply Nat.le_trans with N; [ unfold N; apply Nat.le_max_r | apply Nat.le_succ_diag_r ]. + trivial. - apply Rle_ge; left; apply Rinv_0_lt_compat;trivial. } unfold Rdist in H; unfold Rdiv; rewrite Rabs_mult; rewrite (Rabs_right (/ sum_f_R0 An n)). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat;trivial. } apply Rle_lt_trans with (sum_f_R0 (fun i:nat => Rabs (An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l))) (n - S N1) * / sum_f_R0 An n). { do 2 rewrite <- (Rmult_comm (/ sum_f_R0 An n)); apply Rmult_le_compat_l. - left; apply Rinv_0_lt_compat;trivial. - apply (Rsum_abs (fun i:nat => An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l)) (n - S N1)). } apply Rle_lt_trans with (sum_f_R0 (fun i:nat => An (S N1 + i)%nat * (eps / 2)) (n - S N1) * / sum_f_R0 An n). - do 2 rewrite <- (Rmult_comm (/ sum_f_R0 An n)); apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat. trivial. + apply sum_Rle; intros; rewrite Rabs_mult; pattern (An (S N1 + n0)%nat) at 2; rewrite <- (Rabs_right (An (S N1 + n0)%nat)). * apply Rmult_le_compat_l. -- apply Rabs_pos. -- left; apply H; unfold ge; apply Nat.le_trans with (S N1); [ apply Nat.le_succ_diag_r | apply Nat.le_add_r ]. * apply Rle_ge; left. trivial. - rewrite <- (scal_sum (fun i:nat => An (S N1 + i)%nat) (n - S N1) (eps / 2)); unfold Rdiv; repeat rewrite Rmult_assoc; apply Rmult_lt_compat_l. { trivial. } pattern (/ 2) at 2; rewrite <- Rmult_1_r; apply Rmult_lt_compat_l. + apply Rinv_0_lt_compat; prove_sup. + rewrite Rmult_comm; apply Rmult_lt_reg_l with (sum_f_R0 An n). { trivial. } rewrite <- Rmult_assoc; rewrite Rinv_r. 2:{ trivial. } rewrite Rmult_1_l; rewrite Rmult_1_r; rewrite (tech2 An N1 n). 2:{ trivial. } rewrite Rplus_comm; pattern (sum_f_R0 (fun i:nat => An (S N1 + i)%nat) (n - S N1)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. trivial. Qed.
imports: Rbase Rfunctions Rseries SeqProp Rcomplete PartSum AltSeries Binomial Rsigma Rprod Cauchy_prod Alembert Lra