proposition: Lemma Alembert_C4 : forall (An:nat -> R) (k:R), 0 <= k < 1 -> (forall n:nat, 0 < An n) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.
proof: Proof. intros An k Hyp H H0. assert (X:{ l:R | is_lub (EUn (fun N:nat => sum_f_R0 An N)) l } -> { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). { intros (x,H1). exists x; apply Un_cv_crit_lub; [ unfold Un_growing; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H | apply H1]. } apply X. apply completeness. 2:{ exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. } assert (H1 := tech13 _ _ Hyp H0). elim H1; intros. elim H2; intros. elim H4; intros. unfold bound; exists (sum_f_R0 An x0 + / (1 - x) * An (S x0)). unfold is_upper_bound; intros; unfold EUn in H6. elim H6; intros. rewrite H7. destruct (lt_eq_lt_dec x2 x0) as [[| -> ]|]. - replace (sum_f_R0 An x0) with (sum_f_R0 An x2 + sum_f_R0 (fun i:nat => An (S x2 + i)%nat) (x0 - S x2)). 2:{ symmetry ; apply tech2; assumption. } pattern (sum_f_R0 An x2) at 1; rewrite <- Rplus_0_r. rewrite Rplus_assoc; apply Rplus_le_compat_l. left; apply Rplus_lt_0_compat. + apply tech1. intros; apply H. + apply Rmult_lt_0_compat. * apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; replace (x + (1 - x)) with 1 by ring; elim H3; intros; assumption. * apply H. - pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply Rmult_lt_0_compat. + apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; replace (x + (1 - x)) with 1 by ring; elim H3; intros; assumption. + apply H. - replace (sum_f_R0 An x2) with (sum_f_R0 An x0 + sum_f_R0 (fun i:nat => An (S x0 + i)%nat) (x2 - S x0)). 2:{ symmetry ; apply tech2; assumption. } apply Rplus_le_compat_l. cut (sum_f_R0 (fun i:nat => An (S x0 + i)%nat) (x2 - S x0) <= An (S x0) * sum_f_R0 (fun i:nat => x ^ i) (x2 - S x0)). { intro; apply Rle_trans with (An (S x0) * sum_f_R0 (fun i:nat => x ^ i) (x2 - S x0)). { assumption. } rewrite <- (Rmult_comm (An (S x0))); apply Rmult_le_compat_l. { left; apply H. } rewrite tech3. 2:{ lra. } unfold Rdiv; apply Rmult_le_reg_l with (1 - x). { lra. } do 2 rewrite (Rmult_comm (1 - x)). rewrite Rmult_assoc; rewrite Rinv_l. 2:{ lra. } rewrite Rmult_1_r; apply Rplus_le_reg_l with (x ^ S (x2 - S x0)). replace (x ^ S (x2 - S x0) + (1 - x ^ S (x2 - S x0))) with 1 by ring. rewrite <- (Rplus_comm 1); pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply pow_lt. lra. } replace (An (S x0)) with (An (S x0 + 0)%nat) by (f_equal;ring). apply (tech6 (fun i:nat => An (S x0 + i)%nat) x). { lra. } intro. cut (forall n:nat, (n >= x0)%nat -> An (S n) < x * An n). { intro H9. replace (S x0 + S i)%nat with (S (S x0 + i)) by ring. apply H9. unfold ge. apply tech8. } intros. apply Rmult_lt_reg_l with (/ An n). { apply Rinv_0_lt_compat; apply H. } do 2 rewrite (Rmult_comm (/ An n)). rewrite Rmult_assoc. rewrite Rinv_r. 2:{ assert (H11 := H n). lra. } rewrite Rmult_1_r. replace (An (S n) * / An n) with (Rabs (An (S n) / An n)). { apply H5; assumption. } rewrite Rabs_right. { unfold Rdiv; reflexivity. } left; unfold Rdiv; change (0 < An (S n) * / An n); apply Rmult_lt_0_compat. + apply H. + apply Rinv_0_lt_compat; apply H. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra