proposition: Lemma derivable_pt_lim_in_weaksum_r: forall An r (rho : Cv_radius_weak An r) (rho' : Cv_radius_weak (An_deriv An) r) x (x_in: Rball 0 r x), derivable_pt_lim_in (Rball 0 r) (weaksum_r An r rho) x (weaksum_r (An_deriv An) r rho' x).
proof: Proof. intros An r rho rho' x x_in. assert (x_bd : Rabs x < r). unfold Rball in x_in ; rewrite Rminus_0_r in x_in ; assumption. assert (x_bd' : Rabs x < Rabs r). apply Rlt_le_trans with r ; [assumption | right ; symmetry ; apply Rabs_right]. apply Rle_ge ; apply Rle_trans with (Rabs x) ; [apply Rabs_pos | left ; assumption]. assert (lb_lt_x : - middle (Rabs x) (Rabs r) < x). apply Rlt_le_trans with (- Rabs x). apply Ropp_gt_lt_contravar ; apply Rlt_gt ; apply middle_is_in_the_middle ; assumption. apply MyRIneq.Rabs_le. assert (x_lt_ub : x < middle (Rabs x) (Rabs r)). apply Rle_lt_trans with (Rabs x) ; [apply Rle_abs | apply middle_is_in_the_middle] ; assumption. pose (r' := middle (middle (Rabs x) (Rabs r)) (Rabs r)). assert (r'_bd1 := proj2 (middle_is_in_the_middle _ _ x_bd')). replace (middle (Rabs x) (Rabs r)) with (Rabs (middle (Rabs x) (Rabs r))) in r'_bd1 ; [| apply Rabs_right ; unfold r' ; apply Rle_ge ; unfold Rdiv ; apply Rle_mult_inv_pos ; [| lra] ; apply Rplus_le_le_0_compat ; apply Rabs_pos]. assert (r'_bd := proj2 (middle_is_in_the_middle _ _ r'_bd1)). assert (Temp : middle (Rabs (middle (Rabs x) (Rabs r))) (Rabs r) = r'). unfold r' ; unfold Rdiv ; apply Rmult_eq_compat_r ; apply Rplus_eq_compat_r ; apply Rabs_right ; apply Rle_ge ; apply Rle_mult_inv_pos ; [| lra] ; apply Rplus_le_le_0_compat ; apply Rabs_pos. rewrite Temp in r'_bd ; clear Temp ; fold r' in r'_bd ; replace r' with (Rabs r') in r'_bd ; [| apply Rabs_right ; unfold r' ; apply Rle_ge ; unfold Rdiv ; apply Rle_mult_inv_pos ; [| lra] ; apply Rplus_le_le_0_compat ; [| apply Rabs_pos] ; unfold Rdiv ; apply Rle_mult_inv_pos ; [| lra] ; apply Rplus_le_le_0_compat ; apply Rabs_pos]. pose (r'' := middle (Rabs x) (Rabs r)). assert (r''_pos : 0 < r''). unfold r''. apply Rlt_mult_inv_pos ; [| lra] ; apply Rplus_le_lt_0_compat ; [| apply Rle_lt_trans with (Rabs x) ; [| assumption]] ; apply Rabs_pos. assert (r''_bd : r'' < r'). unfold r'', r'. unfold Rdiv ; apply Rmult_lt_compat_r ; [lra |] ; apply Rplus_lt_compat_r. apply middle_is_in_the_middle ; assumption. pose (myR := mkposreal r'' r''_pos). assert (myR_ub : myR < r') by intuition. assert (Abel2' := Rpser_abel2 (An_deriv An) r' (Cv_radius_weak_derivable_compat An r rho r' r'_bd) myR myR_ub). assert (cv_interv : forall y : R, Boule 0 (mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x)(Rabs r)) lb_lt_x x_lt_ub) y -> {l : R | Un_cv (fun N : nat => SP (fun (n : nat) (x : R) => gt_pser (An_deriv An) x n) N y) l}). intros y y_bd. exists (weaksum_r (An_deriv An) r rho' y). assert (y_bd2 : Rabs y < r). unfold Boule, mkposreal_lb_ub in y_bd ; rewrite Rminus_0_r in y_bd. apply Rlt_trans with (middle (middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r))). rewrite (middle_unfold (middle _ _ )), <- Rminus_opp ; assumption. apply Rle_lt_trans with (middle (Rabs x) (Rabs r)). right ; unfold middle ; field. apply Rlt_le_trans with (Rabs r). apply middle_is_in_the_middle ; assumption. right ; apply Rabs_pos_eq ; left ; apply Rle_lt_trans with (Rabs x) ; [apply Rabs_pos |] ; assumption. intros alpha alpha_pos ; destruct (weaksum_r_sums (An_deriv An) r rho' y y_bd2 alpha alpha_pos) as (N, HN) ; exists N ; intros n n_lb ; apply HN ; assumption. assert (CVN : CVN_r (fun (n : nat) (x : R) => gt_pser (An_deriv An) x n) (mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub)). apply Rpser_abel2 with r'. apply Cv_radius_weak_derivable_compat with r ; assumption. unfold mkposreal_lb_ub. apply Rle_lt_trans with r'' ; [| assumption]. right ; unfold r'' ; intuition. assert (Temp : (middle (Rabs x) (Rabs r) - - middle (Rabs x) (Rabs r)) / 2 = middle (Rabs x) (Rabs r)) by field. intuition. assert (Main := CVN_CVU_interv (fun n x => gt_pser (An_deriv An) x n) (mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub) cv_interv CVN). assert (Main2 : RFseq_cvu (Rpser_partial_sum_derive An) (weaksum_r (An_deriv An) r rho') (middle (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r))) (mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub)). clear -Main x_bd x_bd'; intros eps eps_pos ; destruct (Main eps eps_pos) as (N, HN) ; exists (S N) ; intros n y n_lb y_bd. assert (y_bd2 : Boule 0 (mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub) y). unfold Boule in * ; rewrite middle_R0 in y_bd ; assumption. assert(n_lb2 : (N <= pred n)%nat) by intuition. assert (Temp := HN (pred n) y n_lb2 y_bd2). assert (T1 := SFL_interv_right (fun (n : nat) (x : R) => gt_pser (An_deriv An) x n) (mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub) cv_interv y y_bd2). assert (y_bd3 : Rabs y < r). unfold Boule, mkposreal_lb_ub in y_bd2 ; rewrite Rminus_0_r in y_bd2. apply Rlt_trans with ((middle (Rabs x) (Rabs r) - - middle (Rabs x) (Rabs r)) / 2). assumption. apply Rle_lt_trans with (middle (Rabs x) (Rabs r)). right ; field. apply Rlt_le_trans with (Rabs r). apply middle_is_in_the_middle ; assumption. right ; apply Rabs_pos_eq ; apply Rle_trans with (Rabs x) ; [apply Rabs_pos | left ; assumption]. assert (T2 := weaksum_r_sums (An_deriv An) r rho' y y_bd3) ; unfold Rpser, Rseq_pps in T2. rewrite Rseq_cv_eq_compat with (Vn := fun N => SP (fun (n : nat) (x : R) => gt_pser (An_deriv An) x n) N y) in T2 ; [| intro ; reflexivity]. assert (Lim_eq := UL_sequence _ _ _ T1 T2). rewrite <- Lim_eq. unfold SP in Temp ; unfold Rpser_partial_sum_derive. assert (Hrew : n = S (pred n)). symmetry. apply Nat.lt_succ_pred with N ; intuition. rewrite Hrew. unfold R_dist ; rewrite Rabs_minus_sym ; apply Temp. assert (Dfn_eq_fn' : forall (x0 : R) (n : nat), - middle (Rabs x) (Rabs r) < x0 -> x0 < middle (Rabs x) (Rabs r) -> derivable_pt_lim ((fun (n0 : nat) (x : R) => sum_f_R0 (gt_pser An x) n0) n) x0 (Rpser_partial_sum_derive An n x0)). intros y n y_lb y_ub. apply derivable_pt_lim_finite_sum. assert (fn_cv_f : RFseq_cv_interv (fun (n : nat) (x : R) => sum_f_R0 (gt_pser An x) n) (weaksum_r An r rho) (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r))). intros y lb_lt_y y_lt_ub eps eps_pos. assert(y_bd1 : - Rabs r < y). apply Rlt_trans with (- middle (Rabs x) (Rabs r)) ; [| assumption]. apply Ropp_lt_contravar ; apply middle_is_in_the_middle ; assumption. assert(y_bd2 : y < Rabs r). apply Rlt_trans with (middle (Rabs x) (Rabs r)) ; [assumption |] ; apply middle_is_in_the_middle ; assumption. assert (y_bd : Rabs y < Rabs r). apply Rabs_def1 ; assumption. replace (Rabs r) with r in y_bd ; [| symmetry ; apply Rabs_right ; apply Rle_ge ; apply Rle_trans with (Rabs x) ; [apply Rabs_pos | left ; assumption]]. destruct (weaksum_r_sums An r rho y y_bd eps eps_pos) as (N, HN) ; exists N ; intros n n_lb ; apply HN ; assumption. apply derivable_pt_lim_derivable_pt_lim_in. apply (RFseq_cvu_derivable (fun n x => sum_f_R0 (gt_pser An x) n) (Rpser_partial_sum_derive An) (weaksum_r An r rho) (weaksum_r (An_deriv An) r rho') x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub Dfn_eq_fn' fn_cv_f Main2). intros y y_lb y_ub. apply CVU_continuity with (fn:=Rpser_partial_sum_derive An) (x:=0) (r:=(mkposreal_lb_ub x (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r)) lb_lt_x x_lt_ub)). intros eps eps_pos ; destruct (Main2 eps eps_pos) as (N, HN) ; exists N ; intros n z n_lb z_bd. rewrite Rabs_minus_sym ; apply HN. assumption. replace (middle (- middle (Rabs x) (Rabs r)) (middle (Rabs x) (Rabs r))) with 0 by (symmetry ; apply middle_R0). assumption. intros. destruct n. unfold Rpser_partial_sum_derive. apply continuity_const ; unfold constant ; intuition. unfold Rpser_partial_sum_derive ; apply continuity_finite_sum. unfold Boule ; rewrite Rminus_0_r. unfold mkposreal_lb_ub. replace ((middle (Rabs x) (Rabs r) - - middle (Rabs x) (Rabs r)) / 2) with (middle (Rabs x) (Rabs r)) by field. apply Rabs_def1 ; intuition. Qed.
imports: Reals Rpow_facts Rfunction_def Rinterval Rextensionality Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Lra MyRIneq Rsequence_facts Rsequence_sums_facts RFsequence RFsequence_facts Rpser_def Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_sums_facts Tactics