Mathlib.Topology.Algebra.InfiniteSum.Ring

Module docstring

{"# 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 ","### 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

","#### ℕ-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] "}

HasSum.mul_left theorem

(a₂) (h : HasSum f a₁) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁)

Full source

theorem HasSum.mul_left (a₂) (h : HasSum f a₁) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) := by
  simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)

Left Multiplication Preserves Summability

Informal description

Let $f$ be a function from an index set to a topological ring, and suppose $f$ has sum $a_1$. Then for any element $a_2$ in the ring, the function $i \mapsto a_2 \cdot f(i)$ has sum $a_2 \cdot a_1$.

HasSum.mul_right theorem

(a₂) (hf : HasSum f a₁) : HasSum (fun i ↦ f i * a₂) (a₁ * a₂)

Full source

theorem HasSum.mul_right (a₂) (hf : HasSum f a₁) : HasSum (fun i ↦ f i * a₂) (a₁ * a₂) := by
  simpa only using hf.map (AddMonoidHom.mulRight a₂) (continuous_id.mul continuous_const)

Right Multiplication Preserves Infinite Sums

Informal description

Let $f$ be a function such that its infinite sum converges to $a₁$. Then for any element $a₂$, the function $i \mapsto f(i) \cdot a₂$ has an infinite sum that converges to $a₁ \cdot a₂$.

Summable.mul_left theorem

(a) (hf : Summable f) : Summable fun i ↦ a * f i

Full source

theorem Summable.mul_left (a) (hf : Summable f) : Summable fun i ↦ a * f i :=
  (hf.hasSum.mul_left _).summable

Left Multiplication Preserves Summability

Informal description

Let $f$ be a summable function from an index set to a topological ring. Then for any element $a$ in the ring, the function $i \mapsto a \cdot f(i)$ is also summable.

Summable.mul_right theorem

(a) (hf : Summable f) : Summable fun i ↦ f i * a

Full source

theorem Summable.mul_right (a) (hf : Summable f) : Summable fun i ↦ f i * a :=
  (hf.hasSum.mul_right _).summable

Summability under right multiplication by a constant

Informal description

Let $f$ be a summable function and let $a$ be a constant. Then the function $i \mapsto f(i) \cdot a$ is also summable.

Summable.tsum_mul_left theorem

(a) (hf : Summable f) : ∑' i, a * f i = a * ∑' i, f i

Full source

protected theorem Summable.tsum_mul_left (a) (hf : Summable f) : ∑' i, a * f i = a * ∑' i, f i :=
  (hf.hasSum.mul_left _).tsum_eq

Left Multiplication Commutes with Infinite Summation

Informal description

Let $f$ be a summable function from an index set to a topological ring. Then for any element $a$ in the ring, the infinite sum $\sum_{i} (a \cdot f(i))$ equals $a$ multiplied by the infinite sum $\sum_{i} f(i)$.

Summable.tsum_mul_right theorem

(a) (hf : Summable f) : ∑' i, f i * a = (∑' i, f i) * a

Full source

protected theorem Summable.tsum_mul_right (a) (hf : Summable f) : ∑' i, f i * a = (∑' i, f i) * a :=
  (hf.hasSum.mul_right _).tsum_eq

Right Multiplication of Summable Series by a Constant

Informal description

Let $f$ be a summable function and let $a$ be a constant. Then the infinite sum $\sum_{i} (f(i) \cdot a)$ is equal to $(\sum_{i} f(i)) \cdot a$.

Commute.tsum_right theorem

(a) (h : ∀ i, Commute a (f i)) : Commute a (∑' i, f i)

Full source

theorem Commute.tsum_right (a) (h : ∀ i, Commute a (f i)) : Commute a (∑' i, f i) := by
  classical
  by_cases hf : Summable f
  · exact (hf.tsum_mul_left a).symm.trans ((congr_arg _ <| funext h).trans (hf.tsum_mul_right a))
  · exact (tsum_eq_zero_of_not_summable hf).symm ▸ Commute.zero_right _

Commutation of Element with Infinite Sum

Informal description

Let $a$ be an element in a topological ring and $f$ be a summable function from an index set to the same ring. If $a$ commutes with $f(i)$ for every index $i$ (i.e., $a \cdot f(i) = f(i) \cdot a$), then $a$ also commutes with the infinite sum $\sum_{i} f(i)$ (i.e., $a \cdot \sum_{i} f(i) = \sum_{i} f(i) \cdot a$).

Commute.tsum_left theorem

(a) (h : ∀ i, Commute (f i) a) : Commute (∑' i, f i) a

Full source

theorem Commute.tsum_left (a) (h : ∀ i, Commute (f i) a) : Commute (∑' i, f i) a :=
  (Commute.tsum_right _ fun i ↦ (h i).symm).symm

Commutation of Infinite Sum with Element

Informal description

Let $a$ be an element in a topological ring and $f$ be a summable function from an index set to the same ring. If $f(i)$ commutes with $a$ for every index $i$ (i.e., $f(i) \cdot a = a \cdot f(i)$), then the infinite sum $\sum_{i} f(i)$ also commutes with $a$ (i.e., $\left(\sum_{i} f(i)\right) \cdot a = a \cdot \left(\sum_{i} f(i)\right)$).

HasSum.div_const theorem

(h : HasSum f a) (b : α) : HasSum (fun i ↦ f i / b) (a / b)

Full source

theorem HasSum.div_const (h : HasSum f a) (b : α) : HasSum (fun i ↦ f i / b) (a / b) := by
  simp only [div_eq_mul_inv, h.mul_right b⁻¹]

Division by Constant Preserves Infinite Sums

Informal description

Let $f$ be a function such that its infinite sum converges to $a$. Then for any nonzero element $b$, the function $i \mapsto f(i) / b$ has an infinite sum that converges to $a / b$.

Summable.div_const theorem

(h : Summable f) (b : α) : Summable fun i ↦ f i / b

Full source

theorem Summable.div_const (h : Summable f) (b : α) : Summable fun i ↦ f i / b :=
  (h.hasSum.div_const _).summable

Summability under division by a constant

Informal description

Let $f$ be a summable function from an index set to a topological division monoid $\alpha$. Then for any nonzero element $b \in \alpha$, the function $i \mapsto f(i) / b$ is summable.

hasSum_mul_left_iff theorem

(h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁) ↔ HasSum f a₁

Full source

theorem hasSum_mul_left_iff (h : a₂ ≠ 0) : HasSumHasSum (fun i ↦ a₂ * f i) (a₂ * a₁) ↔ HasSum f a₁ :=
  ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹, HasSum.mul_left _⟩

Equivalence of Summability Under Left Multiplication by Nonzero Element

Informal description

Let $f$ be a function from an index set to a topological ring, and let $a_1, a_2$ be elements of the ring with $a_2 \neq 0$. Then the function $i \mapsto a_2 \cdot f(i)$ has sum $a_2 \cdot a_1$ if and only if $f$ has sum $a_1$.

hasSum_mul_right_iff theorem

(h : a₂ ≠ 0) : HasSum (fun i ↦ f i * a₂) (a₁ * a₂) ↔ HasSum f a₁

Full source

theorem hasSum_mul_right_iff (h : a₂ ≠ 0) : HasSumHasSum (fun i ↦ f i * a₂) (a₁ * a₂) ↔ HasSum f a₁ :=
  ⟨fun H ↦ by simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹, HasSum.mul_right _⟩

Right Multiplication Preserves Infinite Sums (Iff Version)

Informal description

For a nonzero element $a_2$ in a topological division monoid $\alpha$, the function $i \mapsto f(i) \cdot a_2$ has an infinite sum converging to $a_1 \cdot a_2$ if and only if the function $f$ itself has an infinite sum converging to $a_1$.

hasSum_div_const_iff theorem

(h : a₂ ≠ 0) : HasSum (fun i ↦ f i / a₂) (a₁ / a₂) ↔ HasSum f a₁

Full source

theorem hasSum_div_const_iff (h : a₂ ≠ 0) : HasSumHasSum (fun i ↦ f i / a₂) (a₁ / a₂) ↔ HasSum f a₁ := by
  simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)

Division by Constant Preserves Summability (Iff Version)

Informal description

For a nonzero element $a_2$ in a topological division monoid $\alpha$, the function $i \mapsto f(i) / a_2$ has an infinite sum converging to $a_1 / a_2$ if and only if the function $f$ itself has an infinite sum converging to $a_1$.

summable_mul_left_iff theorem

(h : a ≠ 0) : (Summable fun i ↦ a * f i) ↔ Summable f

Full source

theorem summable_mul_left_iff (h : a ≠ 0) : (Summable fun i ↦ a * f i) ↔ Summable f :=
  ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹, fun H ↦ H.mul_left _⟩

Summability under Left Multiplication by Nonzero Element

Informal description

Let $f$ be a function from an index set to a topological division monoid $\alpha$, and let $a \in \alpha$ be a nonzero element. Then the function $i \mapsto a \cdot f(i)$ is summable if and only if $f$ itself is summable.

summable_mul_right_iff theorem

(h : a ≠ 0) : (Summable fun i ↦ f i * a) ↔ Summable f

Full source

theorem summable_mul_right_iff (h : a ≠ 0) : (Summable fun i ↦ f i * a) ↔ Summable f :=
  ⟨fun H ↦ by simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹, fun H ↦ H.mul_right _⟩

Summability under Right Multiplication by Nonzero Constant (Iff Version)

Informal description

For a nonzero element $a$ in a topological division monoid $\alpha$, the function $i \mapsto f(i) \cdot a$ is summable if and only if the function $f$ is summable.

summable_div_const_iff theorem

(h : a ≠ 0) : (Summable fun i ↦ f i / a) ↔ Summable f

Full source

theorem summable_div_const_iff (h : a ≠ 0) : (Summable fun i ↦ f i / a) ↔ Summable f := by
  simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)

Summability under Division by Nonzero Constant (Iff Version)

Informal description

For a nonzero element $a$ in a topological division monoid $\alpha$, the function $i \mapsto f(i) / a$ is summable if and only if the function $f$ is summable.

tsum_mul_left theorem

[T2Space α] : ∑' x, a * f x = a * ∑' x, f x

Full source

theorem tsum_mul_left [T2Space α] : ∑' x, a * f x = a * ∑' x, f x := by
  classical
  exact if hf : Summable f then hf.tsum_mul_left a
  else if ha : a = 0 then by simp [ha]
  else by rw [tsum_eq_zero_of_not_summable hf,
              tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]

Left Scalar Multiplication Commutes with Infinite Summation

Informal description

Let $\alpha$ be a Hausdorff topological space and $f$ be a function from an index set to $\alpha$. Then the infinite sum $\sum_{x} (a \cdot f(x))$ is equal to $a$ multiplied by the infinite sum $\sum_{x} f(x)$, i.e., \[ \sum_{x} (a \cdot f(x)) = a \cdot \left( \sum_{x} f(x) \right). \]

tsum_mul_right theorem

[T2Space α] : ∑' x, f x * a = (∑' x, f x) * a

Full source

theorem tsum_mul_right [T2Space α] : ∑' x, f x * a = (∑' x, f x) * a := by
  classical
  exact if hf : Summable f then hf.tsum_mul_right a
  else if ha : a = 0 then by simp [ha]
  else by rw [tsum_eq_zero_of_not_summable hf,
              tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).mp hf), zero_mul]

Right Multiplication of Infinite Sum by a Constant in Hausdorff Spaces

Informal description

In a Hausdorff topological space $\alpha$, the infinite sum $\sum_{x} (f(x) \cdot a)$ is equal to $(\sum_{x} f(x)) \cdot a$ for any function $f$ and constant $a$.

tsum_div_const theorem

[T2Space α] : ∑' x, f x / a = (∑' x, f x) / a

Full source

theorem tsum_div_const [T2Space α] : ∑' x, f x / a = (∑' x, f x) / a := by
  simpa only [div_eq_mul_inv] using tsum_mul_right

Division of Infinite Sum by a Constant in Hausdorff Spaces

Informal description

In a Hausdorff topological space $\alpha$, the infinite sum $\sum_{x} \frac{f(x)}{a}$ is equal to $\frac{\sum_{x} f(x)}{a}$ for any function $f$ and nonzero constant $a$.

HasSum.const_div theorem

(h : HasSum (fun x ↦ 1 / f x) a) (b : α) : HasSum (fun i ↦ b / f i) (b * a)

Full source

theorem HasSum.const_div (h : HasSum (fun x ↦ 1 / f x) a) (b : α) :
    HasSum (fun i ↦ b / f i) (b * a) := by
  have := h.mul_left b
  simpa only [div_eq_mul_inv, one_mul] using this

Scaling of Reciprocal Series in Topological Rings

Informal description

Let $f$ be a function from an index set to a topological ring, and suppose the series $\sum_{x} \frac{1}{f(x)}$ converges to $a$. Then for any element $b$ in the ring, the series $\sum_{i} \frac{b}{f(i)}$ converges to $b \cdot a$.

Summable.const_div theorem

(h : Summable (fun x ↦ 1 / f x)) (b : α) : Summable fun i ↦ b / f i

Full source

theorem Summable.const_div (h : Summable (fun x ↦ 1 / f x)) (b : α) :
    Summable fun i ↦ b / f i :=
  (h.hasSum.const_div b).summable

Summability of Scaled Reciprocal Series

Informal description

Let $f$ be a function from an index set to a topological ring $\alpha$. If the series $\sum_x \frac{1}{f(x)}$ is summable, then for any element $b \in \alpha$, the series $\sum_i \frac{b}{f(i)}$ is also summable.

hasSum_const_div_iff theorem

(h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ / f i) (a₂ * a₁) ↔ HasSum (1 / f) a₁

Full source

theorem hasSum_const_div_iff (h : a₂ ≠ 0) :
    HasSumHasSum (fun i ↦ a₂ / f i) (a₂ * a₁) ↔ HasSum (1/ f) a₁ := by
  simpa only [div_eq_mul_inv, one_mul] using hasSum_mul_left_iff h

Equivalence of Summability Under Constant Division by Nonzero Element

Informal description

Let $f$ be a function from an index set to a topological ring, and let $a_1, a_2$ be elements of the ring with $a_2 \neq 0$. Then the function $i \mapsto a_2 / f(i)$ has sum $a_2 \cdot a_1$ if and only if the function $i \mapsto 1 / f(i)$ has sum $a_1$.

summable_const_div_iff theorem

(h : a ≠ 0) : (Summable fun i ↦ a / f i) ↔ Summable (1 / f)

Full source

theorem summable_const_div_iff (h : a ≠ 0) : (Summable fun i ↦ a / f i) ↔ Summable (1 / f) := by
  simpa only [div_eq_mul_inv, one_mul] using summable_mul_left_iff h

Summability of Constant Divided Series Equivalence

Informal description

Let $f$ be a function from an index set to a topological ring $\alpha$, and let $a \in \alpha$ be a nonzero element. Then the function $i \mapsto a / f(i)$ is summable if and only if the function $i \mapsto 1 / f(i)$ is summable.

HasSum.mul_eq theorem

(hf : HasSum f s) (hg : HasSum g t) (hfg : HasSum (fun x : ι × κ ↦ f x.1 * g x.2) u) : s * t = u

Full source

theorem HasSum.mul_eq (hf : HasSum f s) (hg : HasSum g t)
    (hfg : HasSum (fun x : ι × κ ↦ f x.1 * g x.2) u) : s * t = u :=
  have key₁ : HasSum (fun i ↦ f i * t) (s * t) := hf.mul_right t
  have this : ∀ i : ι, HasSum (fun c : κ ↦ f i * g c) (f i * t) := fun i ↦ hg.mul_left (f i)
  have key₂ : HasSum (fun i ↦ f i * t) u := HasSum.prod_fiberwise hfg this
  key₁.unique key₂

Product of Sums Equals Sum of Products in Infinite Series

Informal description

Let $f : \iota \to R$ and $g : \kappa \to R$ be functions with infinite sums $s$ and $t$ respectively, and suppose the function $(x,y) \mapsto f(x) \cdot g(y)$ has infinite sum $u$. Then the product of the sums equals the sum of the products, i.e., $s \cdot t = u$.

HasSum.mul theorem

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

Full source

theorem HasSum.mul (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) :=
  let ⟨_u, hu⟩ := hfg
  (hf.mul_eq hg hu).symm ▸ hu

Product of Sums is Sum of Products in Infinite Series

Informal description

Let $f : \iota \to R$ and $g : \kappa \to R$ be functions with infinite sums $s$ and $t$ respectively, and suppose the function $(x,y) \mapsto f(x) \cdot g(y)$ is summable. Then the function $(x,y) \mapsto f(x) \cdot g(y)$ has sum $s \cdot t$.

Summable.tsum_mul_tsum theorem

 (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

Full source

/-- Product of two infinites sums indexed by arbitrary types.
    See also `tsum_mul_tsum_of_summable_norm` if `f` and `g` are absolutely summable. -/
protected theorem Summable.tsum_mul_tsum (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 :=
  hf.hasSum.mul_eq hg.hasSum hfg.hasSum

Product of Sums Equals Sum of Products for Summable Functions

Informal description

Let $f : \iota \to R$ and $g : \kappa \to R$ be summable functions, and suppose the function $(x,y) \mapsto f(x) \cdot g(y)$ is also summable. Then the product of the infinite sums equals the infinite sum of the products, i.e., \[ \left(\sum_{x \in \iota} f(x)\right) \cdot \left(\sum_{y \in \kappa} g(y)\right) = \sum_{z \in \iota \times \kappa} f(z.1) \cdot g(z.2). \]

summable_mul_prod_iff_summable_mul_sigma_antidiagonal theorem

 :
  (Summable fun x : A × A ↦ f x.1 * g x.2) ↔
    Summable fun x : Σ n : A, antidiagonal n ↦ f (x.2 : A × A).1 * g (x.2 : A × A).2

Full source

/-- 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_mul_prod_iff_summable_mul_sigma_antidiagonal :
    (Summable fun x : A × A ↦ f x.1 * g x.2) ↔
      Summable fun x : Σn : A, antidiagonal n ↦ f (x.2 : A × A).1 * g (x.2 : A × A).2 :=
  Finset.sigmaAntidiagonalEquivProd.summable_iff.symm

Summability Equivalence for Product vs. Antidiagonal Decomposition

Informal description

For functions $f, g : A \to \mathbb{R}$ (or any topological ring), the following are equivalent: 1. The function $(k, l) \mapsto f(k) \cdot g(l)$ is summable over $A \times A$. 2. The function $(n, (k, l)) \mapsto f(k) \cdot g(l)$ is summable over the disjoint union $\Sigma (n : A), \text{antidiagonal}(n)$, where $\text{antidiagonal}(n)$ is the set of pairs $(k, l)$ such that $k + l = n$.

summable_sum_mul_antidiagonal_of_summable_mul theorem

(h : Summable fun x : A × A ↦ f x.1 * g x.2) : Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Full source

theorem summable_sum_mul_antidiagonal_of_summable_mul
    (h : Summable fun x : A × A ↦ f x.1 * g x.2) :
    Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 := by
  rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
  conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
  exact h.sigma' fun n ↦ (hasSum_fintype _).summable

Summability of Antidiagonal Sums from Summability of Product Function

Informal description

Let $A$ be a type with an antidiagonal structure, and let $f, g : A \to R$ be functions such that the function $(k, l) \mapsto f(k) \cdot g(l)$ is summable over $A \times A$. Then the function $n \mapsto \sum_{(k,l) \in \text{antidiagonal}(n)} f(k) \cdot g(l)$ is summable over $A$.

Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal theorem

 (hf : Summable f) (hg : Summable g) (hfg : Summable fun x : A × A ↦ f x.1 * g x.2) :
  ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Full source

/-- 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. -/
protected theorem Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal (hf : Summable f)
    (hg : Summable g) (hfg : Summable fun x : A × A ↦ f x.1 * g x.2) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 := by
  conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
  rw [hf.tsum_mul_tsum hg hfg, ← sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]
  exact (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg).tsum_sigma'
    (fun n ↦ (hasSum_fintype _).summable)

Cauchy Product Formula: $\left(\sum f_n\right) \cdot \left(\sum g_n\right) = \sum_n \sum_{k+l=n} f_k g_l$

Informal description

Let $A$ be a type with a notion of antidiagonal (e.g., $\mathbb{N}$), and let $f, g : A \to R$ be summable functions to a topological ring $R$. Suppose the function $(k, l) \mapsto f(k) \cdot g(l)$ is summable over $A \times A$. Then the product of the infinite sums can be expressed as a double sum over antidiagonals: \[ \left(\sum_{n \in A} f(n)\right) \cdot \left(\sum_{n \in A} g(n)\right) = \sum_{n \in A} \sum_{(k, l) \in \text{antidiagonal}(n)} f(k) \cdot g(l). \]

summable_sum_mul_range_of_summable_mul theorem

(h : Summable fun x : ℕ × ℕ ↦ f x.1 * g x.2) : Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Full source

theorem summable_sum_mul_range_of_summable_mul (h : Summable fun x : ℕℕ × ℕ ↦ f x.1 * g x.2) :
    Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k) := by
  simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
  exact summable_sum_mul_antidiagonal_of_summable_mul h

Summability of Range-Convolved Product from Summability of Product Function

Informal description

Let $f, g : \mathbb{N} \to R$ be functions such that the function $(k, l) \mapsto f(k) \cdot g(l)$ is summable over $\mathbb{N} \times \mathbb{N}$. Then the function $n \mapsto \sum_{k=0}^n f(k) \cdot g(n - k)$ is summable over $\mathbb{N}$.

Summable.tsum_mul_tsum_eq_tsum_sum_range theorem

 (hf : Summable f) (hg : Summable g) (hfg : Summable fun x : ℕ × ℕ ↦ f x.1 * g x.2) :
  ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k)

Full source

/-- 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.
-/
protected theorem Summable.tsum_mul_tsum_eq_tsum_sum_range (hf : Summable f) (hg : Summable g)
    (hfg : Summable fun x : ℕℕ × ℕ ↦ f x.1 * g x.2) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k) := by
  simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
  exact hf.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg hfg

Cauchy Product Formula: $\left(\sum f_n\right) \cdot \left(\sum g_n\right) = \sum_{n=0}^\infty \sum_{k=0}^n f_k g_{n-k}$

Informal description

Let $f, g : \mathbb{N} \to R$ be summable sequences in a topological ring $R$, and suppose the function $(k, l) \mapsto f(k) \cdot g(l)$ is summable over $\mathbb{N} \times \mathbb{N}$. Then the product of the infinite sums can be expressed as: \[ \left(\sum_{n=0}^\infty f(n)\right) \cdot \left(\sum_{n=0}^\infty g(n)\right) = \sum_{n=0}^\infty \sum_{k=0}^n f(k) \cdot g(n - k). \]