proposition: Fact is_cvg_pseries_inside_norm f (x z : R) : cvgn (pseries f x) -> `|z| < `|x| -> cvgn (pseries (fun i => `|f i|) z).
proof: Proof. move=> Cx zLx; have [K [Kreal Kf]] := cvg_series_bounded Cx. have Kzxn n : 0 <= `|K + 1| * `|z ^+ n| / `|x ^+ n| by rewrite !mulr_ge0. apply: normed_cvg. apply: series_le_cvg Kzxn _ _ => [//=| /= n|]. rewrite (_ : `|_ * _| = `|f n * x ^+ n| * `|z ^+ n| / `|x ^+ n|); last first. rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC. by case: ltrgt0P zLx; rewrite //= normr_lt0. do! (apply: ler_pM || apply: mulr_ge0 || rewrite invr_ge0) => //. by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltrDl. have F : `|z / x| < 1. by rewrite normrM normfV ltr_pdivrMr ?mul1r // (le_lt_trans _ zLx). rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first. by apply/funext => i /=; rewrite normrM exprMn mulrA normfV !normrX exprVn. by apply: is_cvg_geometric_series; rewrite normr_id. 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