proposition: Lemma derivable_pt_lim_exp_0 : derivable_pt_lim exp 0 1.
proof: Proof. unfold derivable_pt_lim; intros. set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). cut (CVN_R fn). - intro; assert (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) by apply (CVN_R_CVS _ X). assert (forall n:nat, continuity (fn n)). { intro; unfold fn. replace (fun x:R => x ^ n / INR (fact (S n))) with (pow_fct n / fct_cte (INR (fact (S n))))%F; [ idtac | reflexivity ]. apply continuity_div. - apply derivable_continuous; apply (derivable_pow n). - apply derivable_continuous; apply derivable_const. - intro; unfold fct_cte; apply INR_fact_neq_0. } assert (continuity (SFL fn cv)) by (apply SFL_continuity; assumption). unfold continuity in H1. assert (H2 := H1 0). unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2; unfold limit_in in H2; simpl in H2; unfold Rdist in H2. elim (H2 _ H); intros alp H3. elim H3; intros. exists (mkposreal _ H4); intros. rewrite Rplus_0_l; rewrite exp_0. replace ((exp h - 1) / h) with (SFL fn cv h). + replace 1 with (SFL fn cv 0). { apply H5. split. - unfold D_x, no_cond; split. + trivial. + apply (not_eq_sym H6). - rewrite Rminus_0_r; apply H7. } unfold SFL. case (cv 0) as (x,Hu). eapply UL_sequence. { apply Hu. } unfold Un_cv, SP in |- *. intros; exists 1%nat; intros. unfold Rdist; rewrite decomp_sum. 2:lia. rewrite Rplus_comm. replace (fn 0%nat 0) with 1. 2:{ unfold fn; simpl. unfold Rdiv; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. } unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r. replace (sum_f_R0 (fun i:nat => fn (S i) 0) (pred n)) with 0. { rewrite Rabs_R0; apply H8. } symmetry ; apply sum_eq_R0; intros. unfold fn. simpl. unfold Rdiv; do 2 rewrite Rmult_0_l; reflexivity. + unfold SFL, exp. case (cv h) as (x0,Hu); case (exist_exp h) as (x,Hexp); simpl. eapply UL_sequence. { apply Hu. } unfold Un_cv; intros. unfold exp_in, infinite_sum in Hexp. assert (0 < eps0 * Rabs h). { apply Rmult_lt_0_compat. - apply H8. - apply Rabs_pos_lt; assumption. } elim (Hexp _ H9); intros N0 H10. exists N0; intros. unfold Rdist. apply Rmult_lt_reg_l with (Rabs h). { apply Rabs_pos_lt; assumption. } rewrite <- Rabs_mult. rewrite Rmult_minus_distr_l. replace (h * ((x - 1) / h)) with (x - 1). 2:{ field. assumption. } unfold Rdist in H10. replace (h * SP fn n h - (x - 1)) with (sum_f_R0 (fun i:nat => / INR (fact i) * h ^ i) (S n) - x). { rewrite (Rmult_comm (Rabs h)). apply H10. unfold ge. apply Nat.le_trans with (S N0). - apply Nat.le_succ_diag_r. - apply -> Nat.succ_le_mono; apply H11. } rewrite decomp_sum. 2:apply Nat.lt_0_succ. replace (/ INR (fact 0) * h ^ 0) with 1. 2:simpl; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. unfold Rminus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. rewrite <- (Rplus_comm (- x)). rewrite <- (Rplus_comm (- x + 1)). rewrite Rplus_assoc; repeat apply Rplus_eq_compat_l. replace (pred (S n)) with n; [ idtac | reflexivity ]. unfold SP. rewrite scal_sum. apply sum_eq; intros. unfold fn. replace (h ^ S i) with (h * h ^ i) by (simpl;ring). unfold Rdiv; ring. - assert (H0 := Alembert_exp). unfold CVN_R. intro; unfold CVN_r. exists (fun N:nat => r ^ N / INR (fact (S N))). cut { l:R | Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l }. { intros (x,p). exists x; intros. split. { assumption. } unfold Boule; intros. rewrite Rminus_0_r in H1. unfold fn. unfold Rdiv; rewrite Rabs_mult. assert (0 < INR (fact (S n))). { apply INR_fact_lt_0. } rewrite (Rabs_right (/ INR (fact (S n)))). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat; apply H2. } do 2 rewrite <- (Rmult_comm (/ INR (fact (S n)))). apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply H2. } rewrite <- RPow_abs. apply pow_maj_Rabs. rewrite Rabs_Rabsolu; left; apply H1. } assert ((r:R) <> 0). { assert (H1 := cond_pos r); red; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1). } apply Alembert_C2. { intro; apply Rabs_no_R0. unfold Rdiv; apply prod_neq_R0. { apply pow_nonzero; assumption. } apply Rinv_neq_0_compat; apply INR_fact_neq_0. } unfold Un_cv in H0. unfold Un_cv; intros. cut (0 < eps0 / r); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply (cond_pos r) ] ]. elim (H0 _ H3); intros N0 H4. exists N0; intros. assert (hyp_sn:(S n >= N0)%nat) by lia. assert (H6 := H4 _ hyp_sn). unfold Rdist in H6; rewrite Rminus_0_r in H6. rewrite Rabs_Rabsolu in H6. unfold Rdist; rewrite Rminus_0_r. rewrite Rabs_Rabsolu. replace (Rabs (r ^ S n / INR (fact (S (S n)))) / Rabs (r ^ n / INR (fact (S n)))) with (r * / INR (fact (S (S n))) * / / INR (fact (S n))). { rewrite Rmult_assoc; rewrite Rabs_mult. rewrite (Rabs_right r). 2:{ apply Rle_ge; left; apply (cond_pos r). } apply Rmult_lt_reg_l with (/ r). { apply Rinv_0_lt_compat; apply (cond_pos r). } rewrite <- Rmult_assoc; rewrite Rinv_l. 2:assumption. rewrite Rmult_1_l; rewrite <- (Rmult_comm eps0). apply H6. } unfold Rdiv. repeat rewrite Rabs_mult. repeat rewrite Rabs_inv. rewrite Rinv_mult. repeat rewrite Rabs_right. 2,4:match goal with |- context[fact ?x] => pose proof (INR_fact_lt_0 x) end;lra. 2,3:apply Rle_ge; left; apply pow_lt; apply (cond_pos r). rewrite Rinv_inv. rewrite (Rmult_comm r). rewrite (Rmult_comm (r ^ S n)). repeat rewrite Rmult_assoc. apply Rmult_eq_compat_l. rewrite (Rmult_comm r). rewrite <- Rmult_assoc; rewrite <- (Rmult_comm (INR (fact (S n)))). apply Rmult_eq_compat_l. simpl. rewrite Rmult_assoc; rewrite Rinv_r. 2:{ apply pow_nonzero; assumption. } ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra