proposition: Lemma finite_cv_radius_derivable_compat : forall An r, finite_cv_radius An r <-> finite_cv_radius (An_deriv An) r.
proof: Proof. intros An r ; split. intros [H_ub H_lub] ; split. intros r' (r'_lb, r'_ub) ; apply Cv_radius_weak_derivable_compat with (r := middle (Rabs r) (Rabs r')). apply H_ub ; split. left ; apply middle_lt_le_pos_lt. apply Rabs_pos_lt ; apply Rgt_not_eq ; apply Rlt_gt ; apply Rle_lt_trans with r' ; assumption. apply Rabs_pos. rewrite middle_comm ; apply Rlt_le_trans with (Rabs r). eapply middle_is_in_the_middle. apply Rle_lt_trans with r' ; [right ; apply Rabs_right ; intuition |]. apply Rlt_le_trans with r ; [assumption | right ; symmetry ; apply Rabs_right ; left ; apply Rle_lt_trans with r' ; assumption]. right ; apply Rabs_right ; left ; apply Rle_lt_trans with r' ; assumption. apply Rle_lt_trans with r'. right ; apply Rabs_right ; intuition. rewrite Rabs_right. apply Rle_lt_trans with (Rabs r') ; [right ; symmetry ;apply Rabs_right ; intuition | rewrite middle_comm]. eapply middle_is_in_the_middle. apply Rle_lt_trans with r' ; [right ; apply Rabs_right ; intuition |]. apply Rlt_le_trans with r ; [assumption | right ; symmetry ; apply Rabs_right ; left ; apply Rle_lt_trans with r' ; assumption]. left ; apply middle_lt_le_pos_lt ; [apply Rabs_pos_lt ; apply Rgt_not_eq ; apply Rlt_gt ; apply Rle_lt_trans with r' ; assumption | apply Rabs_pos]. intros r' rltr' Hf ; apply (H_lub _ rltr') ; apply Cv_radius_weak_derivable_compat_rev ; assumption. intros [H_ub H_lub] ; split. intros r' r'_bd ; apply Cv_radius_weak_derivable_compat_rev ; apply H_ub ; assumption. intros r' rltr' Hf. assert (r0_bd : r < middle r r') by (apply middle_is_in_the_middle ; assumption). apply (H_lub _ r0_bd) ; eapply Cv_radius_weak_derivable_compat. eassumption. assert (r_pos : 0 <= r). eapply finite_cv_radius_pos ; split ; [apply H_ub | apply H_lub]. assert (r'_pos : 0 <= r') by (left ; apply Rle_lt_trans with r ; assumption). assert (middle_pos : 0 <= middle r r') by (apply middle_le_le_pos ; assumption). do 2 (rewrite Rabs_pos_eq ; [| assumption]) ; apply middle_is_in_the_middle ; assumption. 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