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 with (Rabs r * / Rabs 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 (Rabs (An 1%nat)) ; intros x Hx ; destruct Hx as (i, Hi) ; rewrite Hi ; unfold gt_abs_pser, gt_pser, An_deriv, Rseq_shift, Rseq_mult, Rseq_abs. destruct i. simpl ; rewrite Rmult_1_l ; rewrite Rmult_1_r ; apply Rle_refl. rewrite r'_lb ; rewrite pow_i ; [| intuition] ; repeat (rewrite Rmult_0_r) ; rewrite Rabs_R0 ; apply Rabs_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_abs_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_abs_pser, gt_pser, Rseq_abs, Rseq_mult in * ; case (le_lt_dec i N) ; intro H. rewrite <- Rabs_Rabsolu ; apply Rle_trans with B2 ; [apply HB2 | apply RmaxLess2] ; assumption. apply Rle_trans with (Rabs (/r' * (INR (S i) * (r' / r) ^ S i) * An (S i) * r ^ S i)). right ; apply Rabs_eq_compat ; unfold An_deriv, Rseq_shift, Rseq_mult ; field_simplify. unfold Rdiv ; repeat (rewrite Rmult_assoc) ; repeat (apply Rmult_eq_compat_l). rewrite Rpow_mult_distr. try (rewrite Rinv_1 ; rewrite Rmult_1_r). rewrite Rmult_assoc. replace ((/ r) ^ S i * (r ^ S i * / r')) with (/ r'). simpl ; field ; assumption. field_simplify. unfold Rdiv ; repeat (rewrite <- Rmult_assoc) ; apply Rmult_eq_compat_r. rewrite <- Rinv_pow. field. apply pow_nonzero. intro Hf ; rewrite Hf, Rabs_R0 in r'_bd. assert (H0 : 0 < 0). apply Rlt_trans with (Rabs r') ; assumption. apply (Rlt_irrefl _ H0). intro Hf ; rewrite Hf, Rabs_R0 in r'_bd. assert (H0 : 0 < 0). apply Rlt_trans with (Rabs r') ; assumption. apply (Rlt_irrefl _ H0). assumption. assumption. assumption. rewrite Rmult_assoc ; rewrite Rabs_mult. apply Rle_trans with (Rabs (/ r' * (INR (S i) * (r' / r) ^ S i)) * B). apply Rmult_le_compat_l ; [apply Rabs_pos |] ; apply HB ; exists (S i) ; reflexivity. apply Rle_trans with (1*B) ; [| rewrite Rmult_1_l ; apply RmaxLess1]. apply Rmult_le_compat_r. apply Rle_trans with (Rabs (An 0%nat * r ^ 0)) ; [apply Rabs_pos |] ; apply HB ; exists 0%nat ; reflexivity. rewrite Rabs_mult ; apply Rle_trans with (Rabs (/r') * Rabs r'). apply Rmult_le_compat_l. apply Rabs_pos. apply Rle_trans with (R_dist (INR (S i) * (r' / r) ^ S i) 0) ; [right ; unfold R_dist ; rewrite Rminus_0_r ; reflexivity |] ; left ; apply HN ; intuition. rewrite <- Rabs_mult ; rewrite Rinv_l ; [| assumption] ; rewrite Rabs_R1 ; right ; trivial. Qed.
imports: Reals Fourier Lra Rpow_facts Rinterval Rextensionality Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_sums MyINR