mathlib documentation

analysis.normed.field.infinite_sum

Multiplying two infinite sums in a normed ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we prove various results about (∑' x : ι, f x) * (∑' y : ι', g y) in a normed ring. There are similar results proven in topology/algebra/infinite_sum (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 (λ (x : ι × ι'), f x.fst * g x.snd)
theorem summable.mul_norm {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [normed_ring α] {f : ι α} {g : ι' α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
summable (λ (x : ι × ι'), f x.fst * g x.snd)
theorem summable_mul_of_summable_norm {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [normed_ring α] [complete_space α] {f : ι α} {g : ι' α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
summable (λ (x : ι × ι'), f x.fst * g x.snd)
theorem tsum_mul_tsum_of_summable_norm {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [normed_ring α] [complete_space α] {f : ι α} {g : ι' α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (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 {α : Type u_1} [normed_ring α] {f g : α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
summable (λ (n : ), (finset.nat.antidiagonal n).sum (λ (kl : × ), f kl.fst * g kl.snd))
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm {α : Type u_1} [normed_ring α] [complete_space α] {f g : α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), (finset.nat.antidiagonal n).sum (λ (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 {α : Type u_1} [normed_ring α] {f g : α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
summable (λ (n : ), (finset.range (n + 1)).sum (λ (k : ), f k * g (n - k)))
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm {α : Type u_1} [normed_ring α] [complete_space α] {f g : α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), (finset.range (n + 1)).sum (λ (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.