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
• tprod_one_add: expanding ∏' i : ι, (1 + f i) as infinite sum.

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

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

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

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

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

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

theorem Commute.tsum_right {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] (a : α) (h : ∀ (i : ι), Commute a (f i)) : Commute a (∑'[L] (i : ι), f i)

theorem Commute.tsum_left {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] (a : α) (h : ∀ (i : ι), Commute (f i) a) : Commute (∑'[L] (i : ι), f i) a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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_3} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {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_3} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {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 Summable.tsum_mul_tsum {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {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.

@[deprecated Summable.tsum_mul_tsum (since := "2025-04-12")]

theorem tsum_mul_tsum {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {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

Alias of Summable.tsum_mul_tsum.

---

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_3} {A : Type u_4} [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_3} {A : Type u_4} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [IsTopologicalSemiring α] (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 Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal {α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [IsTopologicalSemiring α] (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 infinite 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.

@[deprecated Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal (since := "2025-04-12")]

theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal {α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α] [IsTopologicalSemiring α] (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

Alias of Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal.

---

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_of_summable_norm if f and g are absolutely summable.

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

theorem Summable.tsum_mul_tsum_eq_tsum_sum_range {α : Type u_3} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α] [IsTopologicalSemiring α] (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.

@[deprecated Summable.tsum_mul_tsum_eq_tsum_sum_range (since := "2025-04-12")]

theorem tsum_mul_tsum_eq_tsum_sum_range {α : Type u_3} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α] [IsTopologicalSemiring α] (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)

Alias of Summable.tsum_mul_tsum_eq_tsum_sum_range.

---

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.

Infinite product of 1 + f i

This section extends Finset.prod_one_add to the infinite product ∏' i : ι, (1 + f i) = ∑' s : Finset ι, ∏ i ∈ s, f i.

theorem hasProd_one_add_of_hasSum_prod {ι : Type u_1} {α : Type u_3} [CommSemiring α] [TopologicalSpace α] {f : ι → α} {a : α} (h : HasSum (fun (x : Finset ι) => ∏ i ∈ x, f i) a) : HasProd (fun (x : ι) => 1 + f x) a

theorem multipliable_one_add_of_summable_prod {ι : Type u_1} {α : Type u_3} [CommSemiring α] [TopologicalSpace α] {f : ι → α} (h : Summable fun (x : Finset ι) => ∏ i ∈ x, f i) : Multipliable fun (x : ι) => 1 + f x

∏' i : ι, (1 + f i) is convergent if ∑' s : Finset ι, ∏ i ∈ s, f i is convergent.

For complete normed ring, see also multipliable_one_add_of_summable.

theorem tprod_one_add {ι : Type u_1} {α : Type u_3} [CommSemiring α] [TopologicalSpace α] {f : ι → α} [T2Space α] (h : Summable fun (x : Finset ι) => ∏ i ∈ x, f i) : ∏' (i : ι), (1 + f i) = ∑' (s : Finset ι), ∏ i ∈ s, f i