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/Ring.lean (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 : Summable f) (hg : Summable g) (hf' : 0 ≤ f) (hg' : 0 ≤ g) : Summable fun (x : ι × ι') => f x.1 * g x.2

theorem Summable.mul_norm {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [NormedRing R] {f : ι → R} {g : ι' → R} (hf : Summable fun (x : ι) => ‖f x‖) (hg : Summable fun (x : ι') => ‖g x‖) : Summable fun (x : ι × ι') => ‖f x.1 * g x.2‖

theorem summable_mul_of_summable_norm {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [NormedRing R] [CompleteSpace R] {f : ι → R} {g : ι' → R} (hf : Summable fun (x : ι) => ‖f x‖) (hg : Summable fun (x : ι') => ‖g x‖) : Summable fun (x : ι × ι') => f x.1 * g x.2

theorem summable_mul_of_summable_norm' {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [NormedRing R] {f : ι → R} {g : ι' → R} (hf : Summable fun (x : ι) => ‖f x‖) (h'f : Summable f) (hg : Summable fun (x : ι') => ‖g x‖) (h'g : Summable g) : Summable fun (x : ι × ι') => f x.1 * g x.2

theorem tsum_mul_tsum_of_summable_norm {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [NormedRing R] [CompleteSpace R] {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.1 * g z.2

Product of two infinite sums indexed by arbitrary types. See also tsum_mul_tsum if f and g are not absolutely summable, and tsum_mul_tsum_of_summable_norm' when the space is not complete.

theorem tsum_mul_tsum_of_summable_norm' {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [NormedRing R] {f : ι → R} {g : ι' → R} (hf : Summable fun (x : ι) => ‖f x‖) (h'f : Summable f) (hg : Summable fun (x : ι') => ‖g x‖) (h'g : Summable g) : (∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.1 * g z.2

ℕ-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.antidiagonal n.

theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (hg : Summable fun (x : ℕ) => ‖g x‖) : Summable fun (n : ℕ) => ‖∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2‖

theorem summable_sum_mul_antidiagonal_of_summable_norm' {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (h'f : Summable f) (hg : Summable fun (x : ℕ) => ‖g x‖) (h'g : Summable g) : Summable fun (n : ℕ) => ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2

theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm {R : Type u_1} [NormedRing R] [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (hg : Summable fun (x : ℕ) => ‖g x‖) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2

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

theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (h'f : Summable f) (hg : Summable fun (x : ℕ) => ‖g x‖) (h'g : Summable g) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2

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

theorem summable_sum_mul_range_of_summable_norm' {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (h'f : Summable f) (hg : Summable fun (x : ℕ) => ‖g x‖) (h'g : Summable g) : Summable fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)

theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm {R : Type u_1} [NormedRing R] [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (hg : Summable fun (x : ℕ) => ‖g x‖) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), 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, and tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' when the space is not complete.

theorem hasSum_sum_range_mul_of_summable_norm {R : Type u_1} [NormedRing R] [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (hg : Summable fun (x : ℕ) => ‖g x‖) : HasSum (fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

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

theorem hasSum_sum_range_mul_of_summable_norm' {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun (x : ℕ) => ‖f x‖) (h'f : Summable f) (hg : Summable fun (x : ℕ) => ‖g x‖) (h'g : Summable g) : HasSum (fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

theorem summable_of_absolute_convergence_real {f : ℕ → ℝ} : (∃ (r : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, |f i|) Filter.atTop (nhds r)) → Summable f