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 : ℂ) : term (f + g) s = term f s + term g s

theorem LSeries.term_add_apply (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (f + g) s n = term f s n + 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 : ℂ) : term (-f) s = -term f s

theorem LSeries.term_neg_apply (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (-f) s n = -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 : ℂ) : term (f - g) s = term f s - term g s

theorem LSeries.term_sub_apply (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (f - g) s n = term f s n - 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 : ℂ) : term (c • f) s = c • term f s

theorem LSeries.term_smul_apply (f : ℕ → ℂ) (c s : ℂ) (n : ℕ) : term (c • f) s n = c * 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

Sums

@[simp]

theorem LSeries.term_sum_apply {ι : Type u_1} (f : ι → ℕ → ℂ) (S : Finset ι) (s : ℂ) (n : ℕ) : term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

theorem LSeries.term_sum {ι : Type u_1} (f : ι → ℕ → ℂ) (S : Finset ι) (s : ℂ) : term (∑ i ∈ S, f i) s = ∑ i ∈ S, term (f i) s

theorem LSeriesHasSum.sum {ι : Type u_1} {f : ι → ℕ → ℂ} {S : Finset ι} {s : ℂ} {a : ι → ℂ} (hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)) : LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

theorem LSeriesSummable.sum {ι : Type u_1} {f : ι → ℕ → ℂ} {S : Finset ι} {s : ℂ} (hf : ∀ i ∈ S, LSeriesSummable (f i) s) : LSeriesSummable (∑ i ∈ S, f i) s

@[simp]

theorem LSeries_sum {ι : Type u_1} {f : ι → ℕ → ℂ} {S : Finset ι} {s : ℂ} (hf : ∀ i ∈ S, LSeriesSummable (f i) s) : LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s