proposition: Lemma Cv_radius_weak_nth_derivable_compat (k : nat) : forall An r, Cv_radius_weak An r -> forall r', Rabs r' < Rabs r -> Cv_radius_weak (An_nth_deriv An k) r'.
proof: Proof. induction k ; intros An r rAn r' r'_bd. erewrite Cv_radius_weak_ext ; [| apply An_nth_deriv_0]. eapply Cv_radius_weak_le_compat ; [left |] ; eassumption. assert (Hrew : Rabs (middle (Rabs r') (Rabs r)) = middle (Rabs r') (Rabs r)). apply Rabs_pos_eq ; apply middle_le_le_pos ; apply Rabs_pos. erewrite Cv_radius_weak_ext ; [| apply An_nth_deriv_S] ; apply Cv_radius_weak_derivable_compat with (middle (Rabs r') (Rabs r)). apply IHk with r ; [| rewrite Hrew ; apply middle_is_in_the_middle] ; assumption. rewrite Hrew ; 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