proposition: Lemma Cv_radius_weak_derivable_compat : forall An r, Cv_radius_weak An r -> forall r', Rabs r' < Rabs r -> Cv_radius_weak (An_deriv An) r'.
proof: Proof. intros An r rho r' r'_bd. assert (Rabsr_pos : 0 < Rabs r). apply Rle_lt_trans with (Rabs r') ; [apply Rabs_pos | assumption]. assert (x_lt_1 : Rabs (r'/ r) < 1). unfold Rdiv ; rewrite Rabs_mult ; rewrite Rabs_Rinv. replace 1%R with (Rabs r * / Rabs r)%R. apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption. apply Rinv_r ; apply Rgt_not_eq ; assumption. intro Hf ; rewrite Hf, Rabs_R0 in Rabsr_pos ; apply (Rlt_irrefl _ Rabsr_pos). destruct rho as (B,HB). case (Req_or_neq r') ; intro r'_lb. exists (Cnorm (An 1%nat)) ; intros x Hx ; destruct Hx as (i, Hi) ; rewrite Hi ; unfold An_deriv, Cseq_shift ; unfold_gt. destruct i. simpl ; rewrite Cmult_1_l, Cmult_1_r ; apply Rle_refl. rewrite r'_lb ; rewrite IRC_pow_compat, pow_i ; [| intuition] ; repeat rewrite Cmult_0_r, Cnorm_C0 ; apply Cnorm_pos. assert (Rabsr'_pos : 0 < Rabs r') by (apply Rabs_pos_lt ; assumption). destruct (Rpser_cv_speed_pow_id (r' / r) x_lt_1 (Rabs r') Rabsr'_pos) as (N, HN). destruct (Rseq_partial_bound (gt_norm_pser (An_deriv An) r') N) as (B2, HB2). exists (Rmax B B2) ; intros x Hx ; destruct Hx as (i, Hi) ; rewrite Hi ; unfold gt_norm_pser, gt_pser, Cseq_norm, Cseq_mult in * ; case (le_lt_dec i N) ; intro H. apply Rle_trans with B2 ; [rewrite <- Rabs_Cnorm ; apply HB2 | apply RmaxLess2] ; assumption. apply Rle_trans with (Cnorm (/r' * (INC (S i) * (r' / r) ^ S i) * An (S i) * r ^ S i)). right ; apply Cnorm_eq_compat ; unfold An_deriv, Cseq_shift, Cseq_mult ; field_simplify. unfold Cdiv ; repeat (rewrite Cmult_assoc) ; repeat (apply Cmult_eq_compat_l). rewrite Cpow_mul_distr_l. try (rewrite Cinv_1 ; rewrite Cmult_1_r). rewrite Cmult_assoc. replace ((/ r) ^ S i * (r ^ S i * / r')) with (/ r'). simpl ; field ; auto with complex. assert (r_neq : r <> 0%R). intro Hf ; rewrite Hf, Rabs_R0 in Rabsr_pos ; elim (Rlt_irrefl _ Rabsr_pos). rewrite <- Cpow_inv. rewrite <- Cmult_assoc. field ; split. auto with complex. apply Cpow_neq_compat ; auto with complex. auto with complex. auto with complex. apply Rle_trans with (Cnorm (/ r' * (INC (S i) * (r' / r) ^ S i)) * B)%R. rewrite Cmult_assoc, Cnorm_Cmult ; apply Rmult_le_compat_l ; [apply Cnorm_pos |] ; apply HB ; exists (S i) ; reflexivity. apply Rle_trans with (1*B)%R ; [| rewrite Rmult_1_l ; apply RmaxLess1]. apply Rmult_le_compat_r. apply Rle_trans with (Cnorm (An 0%nat * r ^ 0)) ; [apply Cnorm_pos |] ; apply HB ; exists 0%nat ; reflexivity. rewrite Cnorm_Cmult ; apply Rle_trans with (Cnorm (/r') * Cnorm r')%R. apply Rmult_le_compat_l. apply Cnorm_pos. apply Rle_trans with (Cnorm ((INC (S i) * (r' / r) ^ S i) - 0)). right ; rewrite Cminus_0_r ; reflexivity. apply Rle_trans with (R_dist (INR (S i) * (r' / r) ^ S i) 0)%R. right ; unfold R_dist ; rewrite <- Cnorm_IRC_Rabs ; apply Cnorm_eq_compat. rewrite Cminus_IRC_Rminus ; unfold Rminus ; apply Cadd_eq_compat_r. rewrite Cmult_IRC_Rmult, IRC_INR_INC ; apply Cmult_eq_compat_l. rewrite <- IRC_pow_compat, Cdiv_IRC_Rdiv. reflexivity. intro Hf ; rewrite Hf, Rabs_R0 in Rabsr_pos ; elim (Rlt_irrefl _ Rabsr_pos). rewrite Cnorm_IRC_Rabs ; left ; apply HN ; intuition. rewrite <- Cnorm_Cmult ; rewrite Cinv_l ; [| auto with complex] ; rewrite Cnorm_C1 ; right ; trivial. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts