mathlib3 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 #

source
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)
source
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‖)
source
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)
source
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.

source
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)‖)
source
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.

source
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))‖)
source
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.