# Documentation

Mathlib.Analysis.Normed.Field.InfiniteSum

# Multiplying two infinite sums in a normed ring #

In this file, we prove various results about (∑' x : ι, f x) * (∑' y : ι', g y) in a normed ring. There are similar results proven in Mathlib.Topology.Algebra.InfiniteSum (e.g tsum_mul_tsum), but in a normed ring we get summability results which aren't true in general.

We first establish results about arbitrary index types, ι and ι', and then we specialize to ι = ι' = ℕ to prove the Cauchy product formula (see tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm).

### Arbitrary index types #

theorem Summable.mul_of_nonneg {ι : Type u_2} {ι' : Type u_3} {f : ι} {g : ι'} (hf : ) (hg : ) (hf' : 0 f) (hg' : 0 g) :
Summable fun x => f x.fst * g x.snd
theorem Summable.mul_norm {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [] {f : ιR} {g : ι'R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
Summable fun x => f x.fst * g x.snd
theorem summable_mul_of_summable_norm {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [] [] {f : ιR} {g : ι'R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
Summable fun x => f x.fst * g x.snd
theorem tsum_mul_tsum_of_summable_norm {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [] [] {f : ιR} {g : ι'R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
(∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.fst * g z.snd

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum if f and g are not absolutely summable.

### ℕ-indexed families (Cauchy product) #

We prove two versions of the Cauchy product formula. The first one is tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm, where the n-th term is a sum over Finset.range (n+1) involving Nat subtraction. In order to avoid Nat subtraction, we also provide tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm, where the n-th term is a sum over all pairs (k, l) such that k+l=n, which corresponds to the Finset Finset.Nat.antidiagonal n.

theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {R : Type u_1} [] {f : R} {g : R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
Summable fun n => Finset.sum () fun kl => f kl.fst * g kl.snd
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm {R : Type u_1} [] [] {f : R} {g : R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), Finset.sum () fun kl => f kl.fst * g kl.snd

The Cauchy product formula for the product of two infinite sums indexed by ℕ, expressed by summing on Finset.Nat.antidiagonal. See also tsum_mul_tsum_eq_tsum_sum_antidiagonal if f and g are not absolutely summable.

theorem summable_norm_sum_mul_range_of_summable_norm {R : Type u_1} [] {f : R} {g : R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
Summable fun n => Finset.sum (Finset.range (n + 1)) fun k => f k * g (n - k)
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm {R : Type u_1} [] [] {f : R} {g : R} (hf : Summable fun x => f x) (hg : Summable fun x => g x) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), Finset.sum (Finset.range (n + 1)) fun k => f k * g (n - k)

The Cauchy product formula for the product of two infinite sums indexed by ℕ, expressed by summing on Finset.range. See also tsum_mul_tsum_eq_tsum_sum_range if f and g are not absolutely summable.