Linear_Combination_of_Convergent_Series
Provedproofwikiseries
Let and be sequences of real numbers. Let the two series and converge to and respectively. Let be real numbers. Then the series converges to .
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Algebra.InfiniteSum.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Algebra.InfiniteSum.Basic theorem Linear_Combination_of_Convergent_Series (a b : ℕ → ℝ) (ha : Summable a) (hb : Summable b) (c d : ℝ) : Summable (fun n => c * a n + d * b n) ∧ ∑' n, (c * a n + d * b n) = c * ∑' n, a n + d * ∑' n, b n := by sorry
Source