proposition: Lemma Rpser_alembert_weak_reciprocal : forall (An : nat -> R) (lambda : R), lambda <> 0 -> (forall n : nat, An n <> 0) -> Rseq_cv (fun n => Rabs (An (S n) / An n)) lambda -> forall r, / lambda < Rabs r -> ~ Cv_radius_weak An r.
proof: Proof. intros An lam lam_neq An_neq An_frac_ub r r_ld Hf ; pose (l' := middle 1 (Rabs r * lam)). assert (lam_pos : 0 < lam). apply Rle_neq_lt ; [| symmetry ; exact lam_neq]. eapply Rseq_positive_limit ; [| eassumption] ; intro n ; compute ; apply Rabs_pos. assert (rlam_lb : 1 < Rabs r * lam). apply Rle_lt_trans with (/ lam * lam). right ; field ; apply Rgt_not_eq ; assumption. apply Rmult_lt_compat_r ; assumption. assert (lam_l'_pos : 0 <= lam / l'). apply Rle_mult_inv_pos ; [| apply Rlt_trans with 1; [| apply middle_is_in_the_middle]] ; lra. destruct (Rseq_cv_bounded _ _ lam_neq An_frac_ub l') as [N H]. apply middle_is_in_the_middle ; assumption. assert (HN : forall n, Rabs (An N) * (lam / l') ^ n <= Rabs (An (N + n)%nat)). clear -H lam_pos lam_l'_pos An_neq ; intro n ; induction n. simpl ; rewrite Nat.add_0_r, Rmult_1_r ; reflexivity. apply Rle_trans with (Rabs (An N) * (lam / l') ^ n * (lam / l')). right ; simpl ; ring. apply Rle_trans with (Rabs (An (N + n)%nat) * (lam / l')). apply Rmult_le_compat_r ; assumption. apply Rle_trans with (Rabs (An (N + n)%nat) * Rabs (An (N + S n)%nat) * / Rabs (An (N + n)%nat)). rewrite Rmult_assoc ; apply Rmult_le_compat_l ; [apply Rabs_pos |]. rewrite <- Rabs_inv, <- Rabs_mult. rewrite <- (Rabs_pos_eq lam), <- (Rabs_Rabsolu ((An (N + S n)%nat) * / An (N + n)%nat)), <-plus_n_Sm ; left ; [apply H | assumption]. right ; field ; apply Rabs_no_R0 ; apply An_neq. clear H. assert (r_gt_1: 1 < (lam / l') * Rabs r). apply Rlt_le_trans with (Rabs r * lam * / l') ; [| right ; unfold Rdiv ; ring]. apply Rlt_1_mult_inv ; [apply Rlt_trans with 1 ; [lra |]|] ; apply middle_is_in_the_middle ; assumption. assert (Hinfty : Rseq_cv_pos_infty (gt_abs_pser An r)). apply Rseq_cv_pos_infty_shifts_compat with N. apply Rseq_cv_pos_infty_le_compat with (Rseq_mult (Rseq_constant (Rabs (An N) * Rabs r ^ N)) (Rseq_pow (lam / l' * Rabs r))). intro n ; unfold Rseq_pow, Rseq_shifts, Rseq_mult, Rseq_constant, gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult. apply Rle_trans with ((Rabs (An N) * (lam / l') ^ n) * Rabs r ^ (n + N)). right; repeat rewrite Rmult_assoc ; apply Rmult_eq_compat_l. rewrite Rpow_mult_distr, pow_add ; ring. rewrite Rabs_mult, RPow_abs ; rewrite Nat.add_comm ; apply Rmult_le_compat_r ; [apply Rabs_pos |] ; apply HN. apply Rseq_cv_finite_pos_mult_pos_infty_r with (Rabs (An N) * Rabs r ^ N). rewrite RPow_abs, <- Rabs_mult ; apply Rabs_pos_lt ; apply Rmult_integral_contrapositive_currified ; [apply An_neq | apply pow_nonzero]. intro r_eq ; rewrite r_eq, Rabs_R0, Rmult_0_l in rlam_lb ; clear -rlam_lb ; lra. apply Rseq_constant_cv. apply Rseq_pow_gt_1_cv ; assumption. destruct Hf as [B HB]. destruct (Hinfty B) as [M HM]. apply (Rlt_irrefl (gt_abs_pser An r M)). apply Rle_lt_trans with B ; [apply HB ; exists M | apply HM] ; auto. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts Rpow_facts Lra PeanoNat MyRIneq MyNeq Rinterval RFsequence RFsequence_facts Tactics