Linearity of the L-series of f as a function of f

We show that the LSeries of f : ℕ → ℂ is a linear function of f (assuming convergence of both L-series when adding two functions).

Addition

theorem LSeries.term_add (f : ℕ → ℂ) (g : ℕ → ℂ) (s : ℂ) : LSeries.term (f + g) s = LSeries.term f s + LSeries.term g s

theorem LSeries.term_add_apply (f : ℕ → ℂ) (g : ℕ → ℂ) (s : ℂ) (n : ℕ) : LSeries.term (f + g) s n = LSeries.term f s n + LSeries.term g s n

theorem LSeriesHasSum.add {f : ℕ → ℂ} {g : ℕ → ℂ} {s : ℂ} {a : ℂ} {b : ℂ} (hf : LSeriesHasSum f s a) (hg : LSeriesHasSum g s b) : LSeriesHasSum (f + g) s (a + b)

theorem LSeriesSummable.add {f : ℕ → ℂ} {g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeriesSummable (f + g) s

@[simp]

theorem LSeries_add {f : ℕ → ℂ} {g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeries (f + g) s = LSeries f s + LSeries g s

Negation

theorem LSeries.term_neg (f : ℕ → ℂ) (s : ℂ) : LSeries.term (-f) s = -LSeries.term f s

theorem LSeries.term_neg_apply (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : LSeries.term (-f) s n = -LSeries.term f s n

theorem LSeriesHasSum.neg {f : ℕ → ℂ} {s : ℂ} {a : ℂ} (hf : LSeriesHasSum f s a) : LSeriesHasSum (-f) s (-a)

theorem LSeriesSummable.neg {f : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) : LSeriesSummable (-f) s

@[simp]

theorem LSeriesSummable.neg_iff {f : ℕ → ℂ} {s : ℂ} : LSeriesSummable (-f) s ↔ LSeriesSummable f s

@[simp]

theorem LSeries_neg (f : ℕ → ℂ) (s : ℂ) : LSeries (-f) s = -LSeries f s

Subtraction

theorem LSeries.term_sub (f : ℕ → ℂ) (g : ℕ → ℂ) (s : ℂ) : LSeries.term (f - g) s = LSeries.term f s - LSeries.term g s

theorem LSeries.term_sub_apply (f : ℕ → ℂ) (g : ℕ → ℂ) (s : ℂ) (n : ℕ) : LSeries.term (f - g) s n = LSeries.term f s n - LSeries.term g s n

theorem LSeriesHasSum.sub {f : ℕ → ℂ} {g : ℕ → ℂ} {s : ℂ} {a : ℂ} {b : ℂ} (hf : LSeriesHasSum f s a) (hg : LSeriesHasSum g s b) : LSeriesHasSum (f - g) s (a - b)

theorem LSeriesSummable.sub {f : ℕ → ℂ} {g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeriesSummable (f - g) s

@[simp]

theorem LSeries_sub {f : ℕ → ℂ} {g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) : LSeries (f - g) s = LSeries f s - LSeries g s

Scalar multiplication

theorem LSeries.term_smul (f : ℕ → ℂ) (c : ℂ) (s : ℂ) : LSeries.term (c • f) s = c • LSeries.term f s

theorem LSeries.term_smul_apply (f : ℕ → ℂ) (c : ℂ) (s : ℂ) (n : ℕ) : LSeries.term (c • f) s n = c * LSeries.term f s n

theorem LSeriesHasSum.smul {f : ℕ → ℂ} (c : ℂ) {s : ℂ} {a : ℂ} (hf : LSeriesHasSum f s a) : LSeriesHasSum (c • f) s (c * a)

theorem LSeriesSummable.smul {f : ℕ → ℂ} (c : ℂ) {s : ℂ} (hf : LSeriesSummable f s) : LSeriesSummable (c • f) s

theorem LSeriesSummable.of_smul {f : ℕ → ℂ} {c : ℂ} {s : ℂ} (hc : c ≠ 0) (hf : LSeriesSummable (c • f) s) : LSeriesSummable f s

theorem LSeriesSummable.smul_iff {f : ℕ → ℂ} {c : ℂ} {s : ℂ} (hc : c ≠ 0) : LSeriesSummable (c • f) s ↔ LSeriesSummable f s

@[simp]

theorem LSeries_smul (f : ℕ → ℂ) (c : ℂ) (s : ℂ) : LSeries (c • f) s = c * LSeries f s