proposition: Lemma tech13 : forall (An:nat -> R) (k:R), 0 <= k < 1 -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> exists k0 : R, k < k0 < 1 /\ (exists N : nat, (forall n:nat, (N <= n)%nat -> Rabs (An (S n) / An n) < k0)).
proof: Proof. intros; exists (k + (1 - k) / 2). split. 1:split. - pattern k at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. unfold Rdiv; apply Rmult_lt_0_compat. + apply Rplus_lt_reg_l with k; rewrite Rplus_0_r; replace (k + (1 - k)) with 1; [ elim H; intros; assumption | ring ]. + apply Rinv_0_lt_compat; prove_sup0. - apply Rmult_lt_reg_l with 2. + prove_sup0. + unfold Rdiv; rewrite Rmult_1_r; rewrite Rmult_plus_distr_l; pattern 2 at 1; rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l; [ idtac | discrR ]; rewrite Rmult_1_r; replace (2 * k + (1 - k)) with (1 + k); [ idtac | ring ]. elim H; intros. apply Rplus_lt_compat_l; assumption. - unfold Un_cv in H0; cut (0 < (1 - k) / 2). + intro; elim (H0 ((1 - k) / 2) H1); intros. exists x; intros. assert (H4 := H2 n H3). unfold Rdist in H4; rewrite <- Rabs_Rabsolu; replace (Rabs (An (S n) / An n)) with (Rabs (An (S n) / An n) - k + k); [ idtac | ring ]; apply Rle_lt_trans with (Rabs (Rabs (An (S n) / An n) - k) + Rabs k). * apply Rabs_triang. * rewrite (Rabs_right k). -- apply Rplus_lt_reg_l with (- k); rewrite <- (Rplus_comm k); repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; repeat rewrite Rplus_0_l; apply H4. -- apply Rle_ge; elim H; intros; assumption. + unfold Rdiv; apply Rmult_lt_0_compat. * apply Rplus_lt_reg_l with k; rewrite Rplus_0_r; elim H; intros; replace (k + (1 - k)) with 1; [ assumption | ring ]. * apply Rinv_0_lt_compat; prove_sup0. Qed.
imports: Rbase Rfunctions Rseries Lia