proposition: Lemma CV_radius_derive (a : nat -> R) : CV_radius (PS_derive a) = CV_radius a.
proof: Proof. have H := (CV_radius_bounded a). have H0 := (CV_radius_bounded (PS_derive a)). apply Rbar_le_antisym. apply is_lub_Rbar_subset with (2 := H) (3 := H0) => x [M Ha]. exists (Rmax (Rabs (a O)) (Rabs x * M)) ; case => /= [ | n]. rewrite Rmult_1_r ; by apply Rmax_l. apply Rle_trans with (2 := Rmax_r _ _). replace (a (S n) * (x * x ^ n)) with (x * ((PS_derive a n * x ^ n) / INR (S n))) by (rewrite /PS_derive ; field ; apply not_0_INR, sym_not_eq, O_S). rewrite Rabs_mult ; apply Rmult_le_compat_l. by apply Rabs_pos. rewrite Rabs_div ; [ | by apply not_0_INR, sym_not_eq, O_S]. apply Rle_div_l. by apply Rabs_pos_lt, not_0_INR, sym_not_eq, O_S. apply Rle_trans with (1 := Ha n). rewrite -{1}(Rmult_1_r M). apply Rmult_le_compat_l. by apply Rle_trans with (2 := Ha O), Rabs_pos. by apply Rle_trans with (2 := Rle_abs _), (le_INR 1), le_n_S, Nat.le_0_l. apply H => x [M Hx]. have H1 : Rbar_le (Finite 0) (CV_radius (PS_derive a)). apply H0 ; exists (Rabs (PS_derive a O)) ; case => /= [ | n]. rewrite Rmult_1_r ; by apply Rle_refl. rewrite Rmult_0_l Rmult_0_r Rabs_R0 ; by apply Rabs_pos. wlog: x Hx / (0 < x) => [Hw | Hx0]. case: (Rle_lt_dec x 0) => Hx0. apply Rbar_le_trans with (Finite 0). exact Hx0. by apply H1. by apply Hw. suff : forall y, 0 < y < x -> Rbar_le (Finite y) (CV_radius (PS_derive a)). case: (CV_radius (PS_derive a)) H1 => [l | | ] //= H1 H2. apply Rnot_lt_le => /= H3. have H4 : (0 < (x+l)/2 < x). split. apply Rdiv_lt_0_compat. by apply Rplus_lt_le_0_compat. by apply Rlt_R0_R2. apply Rminus_lt, Ropp_lt_cancel ; field_simplify. rewrite ?Rdiv_1 ; apply Rdiv_lt_0_compat. by apply -> Rminus_lt_0. by apply Rlt_R0_R2. move: (H2 _ H4). apply Rlt_not_le. apply Rminus_lt, Ropp_lt_cancel ; field_simplify. rewrite ?Rdiv_1 ; apply Rdiv_lt_0_compat. rewrite Rplus_comm ; by apply -> Rminus_lt_0. by apply Rlt_R0_R2. move => y Hy. apply H0 ; rewrite /PS_derive. have H2 : is_lim_seq (fun n => INR (S n) / x * (y/x) ^ n) 0. apply ex_series_lim_0. apply ex_series_Rabs. apply CV_disk_DAlembert with 1. move => n. apply Rgt_not_eq, Rdiv_lt_0_compat. by apply lt_0_INR, Nat.lt_0_succ. apply Rlt_trans with y ; by apply Hy. apply is_lim_seq_spec. move => eps. case: (nfloor_ex (/eps)) => [ | N HN]. by apply Rlt_le, Rinv_0_lt_compat, eps. exists (S N) => n Hn. apply Rabs_lt_between'. replace (INR (S (S n)) / x / (INR (S n) / x)) with (INR (S (S n)) / (INR (S n))) by (field ; split ; [apply Rgt_not_eq, Rlt_trans with y ; by apply Hy | by apply Rgt_not_eq, lt_0_INR, Nat.lt_0_succ]). rewrite Rabs_pos_eq. split. apply Rlt_div_r. by apply lt_0_INR, Nat.lt_0_succ. rewrite ?S_INR Rminus_lt_0 ; ring_simplify. rewrite Rplus_assoc. apply Rplus_le_lt_0_compat. apply Rmult_le_pos. by apply (le_INR O), Nat.le_0_l. by apply Rlt_le, eps. by apply Rle_lt_0_plus_1, Rlt_le, eps. apply Rlt_div_l. by apply lt_0_INR, Nat.lt_0_succ. rewrite ?S_INR Rminus_lt_0 ; ring_simplify. rewrite /Rminus Rplus_assoc -/(Rminus eps 1). rewrite -(Ropp_involutive (eps-1)) -Rminus_lt_0 Ropp_minus_distr'. apply Rlt_trans with 1. apply Rminus_lt_0 ; ring_simplify ; by apply eps. replace 1 with (eps*/eps) by (field ; apply Rgt_not_eq, eps). apply Rmult_lt_compat_l. by apply eps. apply Rlt_le_trans with (1 := proj2 HN). rewrite -S_INR ; by apply le_INR. apply Rlt_le, Rdiv_lt_0_compat ; by apply lt_0_INR, Nat.lt_0_succ. right ; split. by apply Rgt_not_eq, Rlt_0_1. rewrite Rinv_1 Rabs_pos_eq. apply -> Rdiv_lt_1. by apply Hy. apply Rlt_trans with y ; by apply Hy. apply Rlt_le, Rdiv_lt_0_compat. by apply Hy. apply Rlt_trans with y ; by apply Hy. apply is_lim_seq_spec in H2. case: (H2 (mkposreal _ (Rlt_0_1))) ; simpl pos => {H2} N HN. set My := fix f n := match n with | O => 1 | S n => Rmax (Rabs (INR (S n) / x * (y / x) ^ n)) (f n) end. exists (M * My N) => n. replace (INR (S n) * a (S n) * y ^ n) with ((a (S n) * x ^ (S n)) * (INR (S n) /x * (y / x) ^ n)) by (rewrite /pow -/pow ; apply Rminus_diag_uniq ; field_simplify ; [rewrite ?Rdiv_1 | apply Rgt_not_eq, Rlt_trans with y ; by apply Hy ] ; rewrite ?Rmult_assoc -(Rmult_minus_distr_l (a (S n))) ; apply Rmult_eq_0_compat_l ; rewrite Rmult_comm Rmult_assoc -(Rmult_minus_distr_l (INR (S n))) ; apply Rmult_eq_0_compat_l, Rminus_diag_eq ; elim: n => /= [ | n IH] ; [ring | rewrite -IH ; field ; apply Rgt_not_eq, Rlt_trans with y ; by apply Hy]). rewrite Rabs_mult ; apply Rmult_le_compat. by apply Rabs_pos. by apply Rabs_pos. by apply Hx. case: (le_lt_dec N n) => Hn. apply Rle_trans with 1. move: (HN n Hn) ; rewrite Rminus_0_r ; by apply Rlt_le. move: (HN n Hn) => {HN Hn} ; elim: N => [ | N IH] H2. simpl ; by apply Rle_refl. apply Rle_trans with (1 := IH H2) ; rewrite /My -/My ; by apply Rmax_r. elim: N n Hn {HN} => [ | N IH] n Hn. by apply Nat.nlt_0_r in Hn. apply le_S_n in Hn ; case: (le_lt_eq_dec _ _ Hn) => {} Hn. apply Rle_trans with (2 := Rmax_r _ (My N)) ; by apply IH. rewrite Hn ; by apply (Rmax_l _ (My N)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series