Infinite sum in a ring

This file provides lemmas about the interaction between infinite sums and multiplication.

Main results

• tsum_mul_tsum_eq_tsum_sum_antidiagonal: Cauchy product formula

theorem HasSum.mul_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a₁ : α} (a₂ : α) (h : HasSum f a₁) : HasSum (fun (i : ι) => a₂ * f i) (a₂ * a₁)

theorem HasSum.mul_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a₁ : α} (a₂ : α) (hf : HasSum f a₁) : HasSum (fun (i : ι) => f i * a₂) (a₁ * a₂)

theorem Summable.mul_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} (a : α) (hf : Summable f) : Summable fun (i : ι) => a * f i

theorem Summable.mul_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} (a : α) (hf : Summable f) : Summable fun (i : ι) => f i * a

theorem Summable.tsum_mul_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} [T2Space α] (a : α) (hf : Summable f) : ∑' (i : ι), a * f i = a * ∑' (i : ι), f i

theorem Summable.tsum_mul_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} [T2Space α] (a : α) (hf : Summable f) : ∑' (i : ι), f i * a = (∑' (i : ι), f i) * a

theorem Commute.tsum_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} [T2Space α] (a : α) (h : ∀ (i : ι), Commute a (f i)) : Commute a (∑' (i : ι), f i)

theorem Commute.tsum_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} [T2Space α] (a : α) (h : ∀ (i : ι), Commute (f i) a) : Commute (∑' (i : ι), f i) a

theorem HasSum.div_const {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} (h : HasSum f a) (b : α) : HasSum (fun (i : ι) => f i / b) (a / b)

theorem Summable.div_const {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} (h : Summable f) (b : α) : Summable fun (i : ι) => f i / b

theorem hasSum_mul_left_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) : HasSum (fun (i : ι) => a₂ * f i) (a₂ * a₁) ↔ HasSum f a₁

theorem hasSum_mul_right_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) : HasSum (fun (i : ι) => f i * a₂) (a₁ * a₂) ↔ HasSum f a₁

theorem hasSum_div_const_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) : HasSum (fun (i : ι) => f i / a₂) (a₁ / a₂) ↔ HasSum f a₁

theorem summable_mul_left_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} (h : a ≠ 0) : (Summable fun (i : ι) => a * f i) ↔ Summable f

theorem summable_mul_right_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} (h : a ≠ 0) : (Summable fun (i : ι) => f i * a) ↔ Summable f

theorem summable_div_const_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} (h : a ≠ 0) : (Summable fun (i : ι) => f i / a) ↔ Summable f

theorem tsum_mul_left {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} [T2Space α] : ∑' (x : ι), a * f x = a * ∑' (x : ι), f x

theorem tsum_mul_right {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} [T2Space α] : ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a

theorem tsum_div_const {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} [T2Space α] : ∑' (x : ι), f x / a = (∑' (x : ι), f x) / a

theorem HasSum.const_div {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} (h : HasSum (fun (x : ι) => 1 / f x) a) (b : α) : HasSum (fun (i : ι) => b / f i) (b * a)

theorem Summable.const_div {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} (h : Summable fun (x : ι) => 1 / f x) (b : α) : Summable fun (i : ι) => b / f i

theorem hasSum_const_div_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) : HasSum (fun (i : ι) => a₂ / f i) (a₂ * a₁) ↔ HasSum (1 / f) a₁

theorem summable_const_div_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ι → α} {a : α} (h : a ≠ 0) : (Summable fun (i : ι) => a / f i) ↔ Summable (1 / f)

Multiplying two infinite sums

In this section, we prove various results about (∑' x : ι, f x) * (∑' y : κ, g y). Note that we always assume that the family fun x : ι × κ ↦ f x.1 * g x.2 is summable, since there is no way to deduce this from the summabilities of f and g in general, but if you are working in a normed space, you may want to use the analogous lemmas in Analysis.Normed.Module.Basic (e.g tsum_mul_tsum_of_summable_norm).

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

Arbitrary index types

theorem HasSum.mul_eq {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [TopologicalSemiring α] {f : ι → α} {g : κ → α} {s t u : α} (hf : HasSum f s) (hg : HasSum g t) (hfg : HasSum (fun (x : ι × κ) => f x.1 * g x.2) u) : s * t = u

theorem HasSum.mul {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [TopologicalSemiring α] {f : ι → α} {g : κ → α} {s t : α} (hf : HasSum f s) (hg : HasSum g t) (hfg : Summable fun (x : ι × κ) => f x.1 * g x.2) : HasSum (fun (x : ι × κ) => f x.1 * g x.2) (s * t)

theorem tsum_mul_tsum {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [TopologicalSemiring α] {f : ι → α} {g : κ → α} (hf : Summable f) (hg : Summable g) (hfg : Summable fun (x : ι × κ) => f x.1 * g x.2) : (∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 * g z.2

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum_of_summable_norm if f and g are 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, 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, 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. This in fact allows us to generalize to any type satisfying [Finset.HasAntidiagonal A]

theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal {α : Type u_4} {A : Type u_5} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} : (Summable fun (x : A × A) => f x.1 * g x.2) ↔ Summable fun (x : (n : A) × { x : A × A // x ∈ Finset.antidiagonal n }) => f (↑x.snd).1 * g (↑x.snd).2

The family (k, l) : ℕ × ℕ ↦ f k * g l is summable if and only if the family (n, k, l) : Σ (n : ℕ), antidiagonal n ↦ f k * g l is summable.

theorem summable_sum_mul_antidiagonal_of_summable_mul {α : Type u_4} {A : Type u_5} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [TopologicalSemiring α] (h : Summable fun (x : A × A) => f x.1 * g x.2) : Summable fun (n : A) => ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2

theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal {α : Type u_4} {A : Type u_5} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [TopologicalSemiring α] (hf : Summable f) (hg : Summable g) (hfg : Summable fun (x : A × A) => f x.1 * g x.2) : (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ Finset.antidiagonal n, f kl.1 * g kl.2

The Cauchy product formula for the product of two infinites sums indexed by ℕ, expressed by summing on Finset.antidiagonal.

See also tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm if f and g are absolutely summable.

theorem summable_sum_mul_range_of_summable_mul {α : Type u_4} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α] [TopologicalSemiring α] (h : Summable fun (x : ℕ × ℕ) => f x.1 * g x.2) : Summable fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)

theorem tsum_mul_tsum_eq_tsum_sum_range {α : Type u_4} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α] [TopologicalSemiring α] (hf : Summable f) (hg : Summable g) (hfg : Summable fun (x : ℕ × ℕ) => f x.1 * g x.2) : (∑' (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 infinites sums indexed by ℕ, expressed by summing on Finset.range.

See also tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm if f and g are absolutely summable.