proposition: Lemma pseries_snd_diffs (c : R^nat) K x : cvgn (pseries c K) -> cvgn (pseries (pseries_diffs c) K) -> cvgn (pseries (pseries_diffs (pseries_diffs c)) K) -> `|x| < `|K| -> is_derive x (1 : R) (fun x => limn (pseries c x)) (limn (pseries (pseries_diffs c) x)).
proof: Proof. move=> Ck CdK CddK xLK; rewrite /pseries. set s := (fun n : nat => _); set (f := fun x0 => _). suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> 0^'] --> limn (series s). have F : f^`() x = limn (series s) by apply: cvg_lim hfxs. have Df : derivable f x 1. move: hfxs; rewrite /derivable [X in X @ 0^'](_ : _ = (fun h => h^-1 *: (f (h%:A + x) - f x))) /=; last first. by apply/funext => i //=; rewrite [i%:A]mulr1. by move=> /(cvg_lim _) -> //. by constructor; [exact: Df|rewrite -derive1E]. pose sx := fun n : nat => c n * x ^+ n. have Csx : cvgn (pseries c x) by apply: is_cvg_pseries_inside Ck _. pose shx := fun h (n : nat) => c n * (h + x) ^+ n. suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s). apply: cvg_sub0 Cc. apply/cvgrPdist_lt => eps eps_gt0 /=. near=> h; rewrite sub0r normrN /=. rewrite (le_lt_trans _ eps_gt0)//. rewrite normr_le0 subr_eq0 -/sx -/(shx _); apply/eqP. have Cshx' : cvgn (series (shx h)). apply: is_cvg_pseries_inside Ck _. rewrite (le_lt_trans (ler_normD _ _))// -(subrK `|x| `|K|) ltrD2r. near: h. apply/nbhs_ballP => /=; exists ((`|K| - `|x|) /2%:R) => /=. by rewrite divr_gt0 // subr_gt0. move=> t; rewrite /ball /= sub0r normrN => H tNZ. rewrite (lt_le_trans H)// ler_pdivrMr // mulr2n mulrDr mulr1. by rewrite ler_wpDr // subr_ge0 ltW. rewrite limZr; last exact/is_cvg_seriesB/Csx. by rewrite lim_seriesB; last exact: Csx. apply: cvg_zero => /=. suff Cc : limn (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1))) @[h --> 0^'] --> (0 : R). apply: cvg_sub0 Cc. apply/cvgrPdist_lt => eps eps_gt0 /=. near=> h; rewrite sub0r normrN /=. rewrite (le_lt_trans _ eps_gt0)// normr_le0 subr_eq0; apply/eqP. have Cs : cvgn (series s) by apply: is_cvg_pseries_inside CdK _. have Cs1 := is_cvg_pseries_diffs_equiv Cs. have Fs1 := pseries_diffs_equiv Cs. set s1 := (fun i => _) in Cs1. have Cshx : cvgn (series (shx h)). apply: is_cvg_pseries_inside Ck _. rewrite (le_lt_trans (ler_normD _ _))// -(subrK `|x| `|K|) ltrD2r. near: h. apply/nbhs_ballP => /=; exists ((`|K| - `|x|) / 2%:R) => /=. by rewrite divr_gt0 // subr_gt0. move=> t; rewrite /ball /= sub0r normrN => H tNZ. rewrite (lt_le_trans H)// ler_pdivrMr // mulr2n mulrDr mulr1. by rewrite ler_wpDr // subr_ge0 ltW. have C1 := is_cvg_seriesB Cshx Csx. have Ckf := @is_cvg_seriesZ _ _ h^-1 C1. have Cu : (series (h^-1 *: (shx h - sx)) - series s1) x0 @[x0 --> \oo] --> limn (series (h^-1 *: (shx h - sx))) - limn (series s). exact: cvgB Ckf Fs1. set w := (fun n : nat => _ in RHS). have -> : w = h^-1 *: (shx h - sx) - s1. apply: funext => i; rewrite !fctE. rewrite /w /shx /sx /s1 /= mulrBr; congr (_ - _); last first. by rewrite mulrCA !mulrA. by rewrite -mulrBr [RHS]mulrCA [_^-1 * _]mulrC. rewrite [X in X h = _]/+%R /= [X in _ + X h = _]/-%R /=. have -> : series (h^-1 *: (shx h - sx) - s1) = series (h^-1 *: (shx h - sx)) - (series s1). by apply/funext => i; rewrite /series /= sumrB. have -> : h^-1 *: series (shx h - sx) = series (h^-1 *: (shx h - sx)). by apply/funext => i; rewrite /series /= -scaler_sumr. exact/esym/cvg_lim. pose r := (`|x| + `|K|) / 2. have xLr : `|x| < r by rewrite ltr_pdivlMr // mulrDr mulr1 ltrD2l. have rLx : r < `|K| by rewrite ltr_pdivrMr // mulrDr mulr1 ltrD2r. have r_gt0 : 0 < r by apply: le_lt_trans xLr. have rNZ : r != 0by case: ltrgt0P r_gt0. apply: (@lim_cvg_to_0_linear _ (fun n => `|c n| * n%:R * (n.-1)%:R * r ^+ n.-2) (fun h n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)) (r - `|x|)); first by rewrite subr_gt0. - have : cvgn ([series `|pseries_diffs (pseries_diffs c) n| * r ^+ n]_n). apply: is_cvg_pseries_inside_norm CddK _. by rewrite ger0_norm // ltW // (le_lt_trans _ xLr). have -> : (fun n => `|pseries_diffs (pseries_diffs c) n| * r ^+ n) = (fun n => pseries_diffs (pseries_diffs (fun m => `|c m|)) n * r ^+ n). apply/funext => i. by rewrite /pseries_diffs !normrM !mulrA ger0_norm // ger0_norm. move=> /is_cvg_pseries_diffs_equiv. rewrite /pseries_diffs. have -> : (fun n => n%:R * ((n.+1)%:R * `|c n.+1|) * r ^+ n.-1) = (fun n => pseries_diffs (fun m => (m.-1)%:R * `|c m| * r^-1) n * r ^+ n). apply/funext => n. rewrite /pseries_diffs /= mulrA. case: n => [|n /=]; first by rewrite !(mul0r, mulr0). rewrite [_%:R *_]mulrC !mulrA -[RHS]mulrA exprS. by rewrite [_^-1 * _]mulrA mulVf ?mul1r. move/is_cvg_pseries_diffs_equiv. have ->// : (fun n => n%:R * (n.-1%:R * `|c n| / r) * r ^+ n.-1) = (fun n => `|c n| * n%:R * n.-1%:R * r ^+ n.-2). apply/funext => [] [|[|i]]; rewrite ?(mul0r, mulr0) //=. rewrite mulrA -mulrA exprS [_^-1 * _]mulrA mulVf //. rewrite mul1r !mulrA; congr (_ * _). by rewrite mulrC mulrA. - move=> h /andP[h_gt0 hLrBx] n. rewrite normrM -!mulrA ler_wpM2l //. rewrite (le_trans (pseries_diffs_P3 _ _ (ltW xLr) _))// ?mulrA -?normr_gt0//. by rewrite (le_trans (ler_normD _ _))// -(subrK `|x| r) lerD2r ltW. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex