proposition: Lemma cv_speed_pow_fact : forall x:R, Un_cv (fun n:nat => x ^ n / INR (fact n)) 0.
proof: Proof. intro; cut (Un_cv (fun n:nat => Rabs x ^ n / INR (fact n)) 0 -> Un_cv (fun n:nat => x ^ n / INR (fact n)) 0). { intro; apply H. unfold Un_cv; unfold Rdist; intros; case (Req_dec x 0); intro. - exists 1%nat; intros. rewrite H1; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_R0; rewrite pow_ne_zero; [ unfold Rdiv; rewrite Rmult_0_l; rewrite Rabs_R0; assumption | red; intro; rewrite H3 in H2; elim (Nat.nle_succ_diag_l _ H2) ]. - assert (H2 := Rabs_pos_lt x H1); set (M := up (Rabs x)); cut (0 <= M)%Z. + intro; elim (IZN M H3); intros M_nat H4. set (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))). cut (Un_cv Un 0); unfold Un_cv; unfold Rdist; intros. * elim (H5 eps H0); intros N H6. exists (M_nat + N)%nat; intros; cut (exists p : nat, (p >= N)%nat /\ n = (M_nat + p)%nat). { intro; elim H8; intros p H9. elim H9; intros; rewrite H11; unfold Un in H6; apply H6; assumption. } exists (n - M_nat)%nat. split. -- unfold ge; apply (fun p n m:nat => Nat.add_le_mono_l n m p) with M_nat; rewrite (Nat.add_comm _ (n - M_nat)), Nat.sub_add. { assumption. } apply Nat.le_trans with (M_nat + N)%nat. ++ apply Nat.le_add_r. ++ assumption. -- rewrite Nat.add_comm, Nat.sub_add; [reflexivity | ]; apply Nat.le_trans with (M_nat + N)%nat; [ apply Nat.le_add_r | assumption ]. * set (Vn := fun n:nat => Rabs x * (Un 0%nat / INR (S n))). cut (1 <= M_nat)%nat. 1:intro; cut (forall n:nat, 0 < Un n). 1:intro; cut (Un_decreasing Un). 1:intro; cut (forall n:nat, Un (S n) <= Vn n). 1:intro; cut (Un_cv Vn 0). -- unfold Un_cv; unfold Rdist; intros. elim (H10 eps0 H5); intros N1 H11. exists (S N1); intros. cut (forall n:nat, 0 < Vn n). { intro; apply Rle_lt_trans with (Rabs (Vn (pred n) - 0)). 1:repeat rewrite Rabs_right. - unfold Rminus; rewrite Ropp_0; do 2 rewrite Rplus_0_r; replace n with (S (pred n)). + apply H9. + inversion H12; simpl; reflexivity. - apply Rle_ge; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; left; apply H13. - apply Rle_ge; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; left; apply H7. - apply H11; unfold ge; apply le_S_n; replace (S (pred n)) with n; [ unfold ge in H12; exact H12 | inversion H12; simpl; reflexivity ]. } intro; apply Rlt_le_trans with (Un (S n0)); [ apply H7 | apply H9 ]. -- cut (cv_infty (fun n:nat => INR (S n))). 1:intro; cut (Un_cv (fun n:nat => / INR (S n)) 0). 1:unfold Un_cv, Rdist; intros; unfold Vn. 1:cut (0 < eps1 / (Rabs x * Un 0%nat)). ++ intro; elim (H11 _ H13); intros N H14. exists N; intros; replace (Rabs x * (Un 0%nat / INR (S n)) - 0) with (Rabs x * Un 0%nat * (/ INR (S n) - 0)); [ idtac | unfold Rdiv; ring ]. rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs (Rabs x * Un 0%nat)). ** apply Rinv_0_lt_compat; apply Rabs_pos_lt. apply prod_neq_R0. { apply Rabs_no_R0; assumption. } assert (H16 := H7 0%nat); red; intro; rewrite H17 in H16; elim (Rlt_irrefl _ H16). ** rewrite <- Rmult_assoc; rewrite Rinv_l. { rewrite Rmult_1_l. replace (/ Rabs (Rabs x * Un 0%nat) * eps1) with (eps1 / (Rabs x * Un 0%nat)). - apply H14; assumption. - unfold Rdiv; rewrite (Rabs_right (Rabs x * Un 0%nat)). + apply Rmult_comm. + apply Rle_ge; apply Rmult_le_pos. * apply Rabs_pos. * left; apply H7. } apply Rabs_no_R0. apply prod_neq_R0; [ apply Rabs_no_R0; assumption | assert (H16 := H7 0%nat); red; intro; rewrite H17 in H16; elim (Rlt_irrefl _ H16) ]. ++ unfold Rdiv; apply Rmult_lt_0_compat. { assumption. } apply Rinv_0_lt_compat; apply Rmult_lt_0_compat. { apply Rabs_pos_lt; assumption. } apply H7. ++ now apply (cv_infty_cv_0 (fun n:nat => INR (S n))). ++ unfold cv_infty; intro; destruct (total_order_T M0 0) as [[Hlt|Heq]|Hgt]. ** exists 0%nat; intros. apply Rlt_trans with 0; [ assumption | apply lt_INR_0; apply Nat.lt_0_succ ]. ** exists 0%nat; intros; rewrite Heq; apply lt_INR_0; apply Nat.lt_0_succ. ** set (M0_z := up M0). assert (H10 := archimed M0). cut (0 <= M0_z)%Z. { intro; elim (IZN _ H11); intros M0_nat H12. exists M0_nat; intros. apply Rlt_le_trans with (IZR M0_z). - elim H10; intros; assumption. - rewrite H12; rewrite <- INR_IZR_INZ; apply le_INR. apply Nat.le_trans with n; [ assumption | apply Nat.le_succ_diag_r ]. } apply le_IZR; left; simpl; unfold M0_z; apply Rlt_trans with M0; [ assumption | elim H10; intros; assumption ]. -- intro; apply Rle_trans with (Rabs x * Un n * / INR (S n)). ++ unfold Un; replace (M_nat + S n)%nat with (M_nat + n + 1)%nat. ** { rewrite pow_add; replace (Rabs x ^ 1) with (Rabs x); [ idtac | simpl; ring ]. unfold Rdiv; rewrite <- (Rmult_comm (Rabs x)); repeat rewrite Rmult_assoc; repeat apply Rmult_le_compat_l. - apply Rabs_pos. - left; apply pow_lt; assumption. - replace (M_nat + n + 1)%nat with (S (M_nat + n)). + rewrite fact_simpl; rewrite Nat.mul_comm; rewrite mult_INR; rewrite Rinv_mult. apply Rmult_le_compat_l. * left; apply Rinv_0_lt_compat; apply lt_INR_0; apply -> Nat.neq_0_lt_0; red; intro; elim (fact_neq_0 _ H9). * left; apply Rinv_lt_contravar. -- apply Rmult_lt_0_compat; apply lt_INR_0; apply Nat.lt_0_succ. -- apply lt_INR; apply -> Nat.succ_lt_mono. pattern n at 1; replace n with (0 + n)%nat; [ idtac | reflexivity ]. apply Nat.add_lt_mono_r. apply Nat.lt_le_trans with 1%nat; [ apply Nat.lt_0_succ | assumption ]. + ring. } ** ring. ++ unfold Vn; rewrite Rmult_assoc; unfold Rdiv; rewrite (Rmult_comm (Un 0%nat)); rewrite (Rmult_comm (Un n)). repeat apply Rmult_le_compat_l. ** apply Rabs_pos. ** left; apply Rinv_0_lt_compat; apply lt_INR_0; apply Nat.lt_0_succ. ** apply decreasing_prop; [ assumption | apply Nat.le_0_l ]. -- unfold Un_decreasing; intro; unfold Un. replace (M_nat + S n)%nat with (M_nat + n + 1)%nat by ring. rewrite pow_add; unfold Rdiv; rewrite Rmult_assoc; apply Rmult_le_compat_l. { left; apply pow_lt; assumption. } replace (Rabs x ^ 1) with (Rabs x); [ idtac | simpl; ring ]. replace (M_nat + n + 1)%nat with (S (M_nat + n)) by ring. apply Rmult_le_reg_l with (INR (fact (S (M_nat + n)))). ++ apply lt_INR_0; apply Nat.neq_0_lt_0; red; intro; elim (fact_neq_0 _ H8). ++ rewrite (Rmult_comm (Rabs x)); rewrite <- Rmult_assoc; rewrite Rinv_r. ** rewrite Rmult_1_l. rewrite fact_simpl; rewrite mult_INR; rewrite Rmult_assoc; rewrite Rinv_r. { rewrite Rmult_1_r; apply Rle_trans with (INR M_nat). - left; rewrite INR_IZR_INZ. rewrite <- H4; assert (H8 := archimed (Rabs x)); elim H8; intros; assumption. - apply le_INR; lia. } apply INR_fact_neq_0. ** apply INR_fact_neq_0. -- intro; unfold Un; unfold Rdiv; apply Rmult_lt_0_compat. { apply pow_lt; assumption. } apply Rinv_0_lt_compat; apply lt_INR_0; apply Nat.neq_0_lt_0; red; intro; elim (fact_neq_0 _ H7). -- clear Un Vn; apply INR_le; simpl. induction M_nat as [| M_nat HrecM_nat]. ++ assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). ++ apply (le_INR 1); apply le_n_S; apply Nat.le_0_l. + apply le_IZR; simpl; left; apply Rlt_trans with (Rabs x). { assumption. } elim (archimed (Rabs x)); intros; assumption. } unfold Un_cv; unfold Rdist; intros; elim (H eps H0); intros. exists x0; intros; apply Rle_lt_trans with (Rabs (Rabs x ^ n / INR (fact n) - 0)). - unfold Rminus; rewrite Ropp_0; do 2 rewrite Rplus_0_r; rewrite (Rabs_right (Rabs x ^ n / INR (fact n))). + unfold Rdiv; rewrite Rabs_mult; rewrite (Rabs_right (/ INR (fact n))). * rewrite RPow_abs; right; reflexivity. * apply Rle_ge; left; apply Rinv_0_lt_compat; apply lt_INR_0; apply Nat.neq_0_lt_0; red; intro; elim (fact_neq_0 _ H3). + apply Rle_ge; unfold Rdiv; apply Rmult_le_pos. * case (Req_dec x 0); intro. -- rewrite H3; rewrite Rabs_R0. induction n as [| n Hrecn]; [ simpl; left; apply Rlt_0_1 | simpl; rewrite Rmult_0_l; right; reflexivity ]. -- left; apply pow_lt; apply Rabs_pos_lt; assumption. * left; apply Rinv_0_lt_compat; apply lt_INR_0; apply Nat.neq_0_lt_0; red; intro; elim (fact_neq_0 _ H3). - apply H1; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia