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 : 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 : R} {g : R} (hf : Summable fun (x : ) => f x) (hg : Summable fun (x : ) => g x) :
Summable fun (n : ) => klFinset.antidiagonal n, f kl.1 * g kl.2
theorem summable_sum_mul_antidiagonal_of_summable_norm' {R : Type u_1} [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 (n : ) => klFinset.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 : R} {g : R} (hf : Summable fun (x : ) => f x) (hg : Summable fun (x : ) => g x) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), klFinset.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 : R} {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 : ), klFinset.antidiagonal n, f kl.1 * g kl.2
theorem summable_norm_sum_mul_range_of_summable_norm {R : Type u_1} [NormedRing R] {f : R} {g : R} (hf : Summable fun (x : ) => f x) (hg : Summable fun (x : ) => g x) :
Summable fun (n : ) => kFinset.range (n + 1), f k * g (n - k)
theorem summable_sum_mul_range_of_summable_norm' {R : Type u_1} [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 (n : ) => kFinset.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 : R} {g : R} (hf : Summable fun (x : ) => f x) (hg : Summable fun (x : ) => g x) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), kFinset.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 : R} {g : R} (hf : Summable fun (x : ) => f x) (hg : Summable fun (x : ) => g x) :
HasSum (fun (n : ) => kFinset.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 : R} {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 : ), kFinset.range (n + 1), f k * g (n - k)
theorem hasSum_sum_range_mul_of_summable_norm' {R : Type u_1} [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) :
HasSum (fun (n : ) => kFinset.range (n + 1), f k * g (n - k)) ((∑' (n : ), f n) * ∑' (n : ), g n)