proposition: Lemma lim_cvg_to_0_linear (R : realType) (f : nat -> R) (g : R -> nat -> R) k : 0 < k -> cvgn (series f) -> (forall r, 0 < `|r| < k -> forall n, `|g r n| <= f n * `| r |) -> limn (series (g x)) @[x --> 0^'] --> 0.
proof: Proof. move=> k_gt0 Cf Hg. apply: (@cvg_to_0_linear _ _ (limn (series f)) k) => // h hLk; rewrite mulrC. have Ckf : cvgn (series (`|h| *: f)) := @is_cvg_seriesZ _ _ `|h| Cf. have Cng : cvgn [normed series (g h)]. apply: series_le_cvg (Hg _ hLk) _ => [//|?|]. exact: le_trans (Hg _ hLk _). by under eq_fun do rewrite mulrC. apply: (le_trans (lim_series_norm Cng)). rewrite -[_ * _](lim_seriesZ _ Cf) (lim_series_le Cng Ckf) // => n. by rewrite [leRHS]mulrC; apply: Hg. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau