proposition: Lemma derivable_pt_lim_sum_r : forall (An:nat->C) (r:R) (Pr : finite_cv_radius An r) z, Cnorm z < r -> derivable_pt_lim (sum_r An r Pr) z (sum_r_derive An r Pr z).
proof: Proof. intros An r Pr z z_bd eps eps_pos. assert (H : 0 <= middle (Cnorm z) r < r). split. left ; apply middle_le_lt_pos_lt ; [| apply Rle_lt_trans with (Cnorm z) ; [| assumption]] ; apply Cnorm_pos. apply (middle_is_in_the_middle _ _ z_bd). destruct (derivable_pt_lim_weaksum_r _ _ (proj1 Pr (middle (Cnorm z) r) H) _ (proj1 (middle_is_in_the_middle _ _ z_bd)) _ eps_pos) as [delta Hdelta]. pose (delta' := Rmin delta (((middle (Cnorm z) r) - Cnorm z) / 2)%R) ; assert (delta'_pos : 0 < delta'). apply Rmin_pos. apply delta. apply ub_lt_2_pos with (middle (Cnorm z) (middle (Cnorm z) r)) ; apply (middle_is_in_the_middle _ _ (proj1 (middle_is_in_the_middle _ _ z_bd))). exists (mkposreal delta' delta'_pos) ; intros h h_neq h_bd. replace (sum_r An r Pr (z + h)) with (weaksum_r An (middle (Cnorm z) r) (proj1 Pr (middle (Cnorm z) r) H) (z + h)). replace (sum_r An r Pr z) with (weaksum_r An (middle (Cnorm z) r) (proj1 Pr (middle (Cnorm z) r) H) z). replace (sum_r_derive An r Pr z) with (weaksum_r_derive An (middle (Cnorm z) r) (proj1 Pr (middle (Cnorm z) r) H) z). apply Hdelta ; [assumption | apply Rlt_le_trans with delta'] ; [assumption | apply Rmin_l]. unfold sum_r_derive ; destruct (Rlt_le_dec (Cnorm z) r) as [z_bd2 | Hf]. apply weaksum_r_derive_unique ; apply (middle_is_in_the_middle _ _ z_bd). assert (F : r < r) by (apply Rle_lt_trans with (Cnorm z) ; assumption) ; destruct (Rlt_irrefl _ F). unfold sum_r ; destruct (Rlt_le_dec (Cnorm z) r) as [z_bd2 | Hf]. apply weaksum_r_unique ; apply (middle_is_in_the_middle _ _ z_bd). assert (F : r < r) by (apply Rle_lt_trans with (Cnorm z) ; assumption) ; destruct (Rlt_irrefl _ F). unfold sum_r ; destruct (Rlt_le_dec (Cnorm (z + h)) r) as [z_bd2 | Hf]. apply weaksum_r_unique_strong. apply Rle_lt_trans with (Cnorm z + Cnorm h)%R. apply Cnorm_triang. apply Rlt_le_trans with (Cnorm z + ((middle (Cnorm z) r - Cnorm z) / 2))%R. apply Rplus_lt_compat_l ; apply Rlt_le_trans with delta' ; [assumption | apply Rmin_r]. unfold Rminus ; field_simplify ; unfold Rdiv ; try (rewrite Rinv_1, Rmult_1_r). left ; do 2 eapply middle_is_in_the_middle ; assumption. eapply middle_is_in_the_middle ; assumption. assert (F : r < r). apply Rlt_trans with (middle (Cnorm z) r). apply Rle_lt_trans with (Cnorm (z + h)). assumption. apply Rle_lt_trans with (Cnorm z + Cnorm h)%R. apply Cnorm_triang. apply Rlt_trans with (Cnorm z + ((middle (Cnorm z) r - Cnorm z) / 2))%R. apply Rplus_lt_compat_l ; apply Rlt_le_trans with delta' ; [intuition | apply Rmin_r]. unfold middle ; field_simplify. apply Rlt_le_trans with ((2 * Cnorm z + r + r) / 4)%R. unfold Rdiv ; apply Rmult_lt_compat_r ; [lra |]. apply Rplus_lt_compat_r. apply Rle_lt_trans with (2 * Cnorm z + Cnorm z)%R. right ; ring. apply Rplus_lt_compat_l ; assumption. right ; field. eapply middle_is_in_the_middle ; assumption. destruct (Rlt_irrefl _ F). 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