doc-next-gen

Mathlib.Analysis.Normed.Ring.InfiniteSum

Module docstring

{"# Multiplying two infinite sums in a normed ring

In this file, we prove various results about (∑' x : ι, f x) * (∑' y : ι', g y) in a normed ring. There are similar results proven in Mathlib.Topology.Algebra.InfiniteSum (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 ","### ℕ-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.antidiagonal n. "}

Summable.mul_of_nonneg theorem
{f : ι → ℝ} {g : ι' → ℝ} (hf : Summable f) (hg : Summable g) (hf' : 0 ≤ f) (hg' : 0 ≤ g) : Summable fun x : ι × ι' => f x.1 * g x.2
Full source 
theorem Summable.mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ} (hf : Summable f) (hg : Summable g)
    (hf' : 0 ≤ f) (hg' : 0 ≤ g) : Summable fun x : ι × ι' => f x.1 * g x.2 :=
  (summable_prod_of_nonneg fun _ ↦ mul_nonneg (hf' _) (hg' _)).2 ⟨fun x ↦ hg.mul_left (f x),
    by simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)⟩
Summability of Product of Non-Negative Summable Functions
Informal description
Let $f : \iota \to \mathbb{R}$ and $g : \iota' \to \mathbb{R}$ be non-negative summable functions. Then the function $(x,y) \mapsto f(x) \cdot g(y)$ is summable over $\iota \times \iota'$.
Summable.mul_norm theorem
{f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : Summable fun x : ι × ι' => ‖f x.1 * g x.2‖
Full source 
theorem Summable.mul_norm {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖)
    (hg : Summable fun x => ‖g x‖) : Summable fun x : ι × ι' => ‖f x.1 * g x.2‖ :=
  .of_nonneg_of_le (fun _ ↦ norm_nonneg _)
    (fun x => norm_mul_le (f x.1) (g x.2))
    (hf.mul_of_nonneg hg (fun x => norm_nonneg <| f x) fun x => norm_nonneg <| g x :)
Summability of the Norm of the Product of Summable Functions in a Normed Ring
Informal description
Let $R$ be a normed ring, and let $f \colon \iota \to R$ and $g \colon \iota' \to R$ be functions such that $\sum_{x} \|f(x)\|$ and $\sum_{y} \|g(y)\|$ are summable. Then the function $(x,y) \mapsto \|f(x) \cdot g(y)\|$ is summable over $\iota \times \iota'$.
summable_mul_of_summable_norm theorem
[CompleteSpace R] {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : Summable fun x : ι × ι' => f x.1 * g x.2
Full source 
theorem summable_mul_of_summable_norm [CompleteSpace R] {f : ι → R} {g : ι' → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    Summable fun x : ι × ι' => f x.1 * g x.2 :=
  (hf.mul_norm hg).of_norm
Summability of Product in Complete Normed Ring under Norm Summability Conditions
Informal description
Let $R$ be a complete normed ring, and let $f \colon \iota \to R$ and $g \colon \iota' \to R$ be functions such that $\sum_{x} \|f(x)\|$ and $\sum_{y} \|g(y)\|$ are summable. Then the function $(x,y) \mapsto f(x) \cdot g(y)$ is summable over $\iota \times \iota'$.
summable_mul_of_summable_norm' theorem
{f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : Summable fun x : ι × ι' => f x.1 * g x.2
Full source 
theorem summable_mul_of_summable_norm' {f : ι → R} {g : ι' → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    Summable fun x : ι × ι' => f x.1 * g x.2 := by
  classical
  suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
  let s : FinsetFinset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
  apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finset_prod_atTop
  rw [← prod_atTop_atTop_eq]
  have := Tendsto.prodMap h'f.hasSum h'g.hasSum
  rw [← nhds_prod_eq] at this
  convert ((continuous_mul (M := R)).continuousAt
      (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp this with p
  simp [s, sum_product, ← mul_sum, ← sum_mul]
Summability of Product of Absolutely Summable Functions in Normed Ring
Informal description
Let $R$ be a normed ring, and let $f \colon \iota \to R$ and $g \colon \iota' \to R$ be functions such that: 1. $\sum_{x} \|f(x)\|$ and $\sum_{x} f(x)$ are summable 2. $\sum_{y} \|g(y)\|$ and $\sum_{y} g(y)$ are summable Then the function $(x,y) \mapsto f(x) \cdot g(y)$ is summable over $\iota \times \iota'$.
tsum_mul_tsum_of_summable_norm theorem
[CompleteSpace R] {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2
Full source 
/-- Product of two infinite sums indexed by arbitrary types.
    See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable, and
    `tsum_mul_tsum_of_summable_norm'` when the space is not complete. -/
theorem tsum_mul_tsum_of_summable_norm [CompleteSpace R] {f : ι → R} {g : ι' → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2 :=
  hf.of_norm.tsum_mul_tsum hg.of_norm (summable_mul_of_summable_norm hf hg)
Product of Infinite Sums in Complete Normed Ring under Absolute Summability
Informal description
Let $R$ be a complete normed ring, and let $f \colon \iota \to R$ and $g \colon \iota' \to R$ be functions such that $\sum_{x} \|f(x)\|$ and $\sum_{y} \|g(y)\|$ are summable. Then the product of their infinite sums equals the sum of their pointwise products: \[ \left(\sum_{x \in \iota} f(x)\right) \cdot \left(\sum_{y \in \iota'} g(y)\right) = \sum_{(x,y) \in \iota \times \iota'} f(x) \cdot g(y). \]
tsum_mul_tsum_of_summable_norm' theorem
{f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2
Full source 
theorem tsum_mul_tsum_of_summable_norm' {f : ι → R} {g : ι' → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2 :=
  h'f.tsum_mul_tsum h'g (summable_mul_of_summable_norm' hf h'f hg h'g)
Product of Sums Equals Sum of Products in Normed Ring
Informal description
Let $R$ be a normed ring, and let $f \colon \iota \to R$ and $g \colon \iota' \to R$ be functions such that: 1. $\sum_{x} \|f(x)\|$ and $\sum_{x} f(x)$ are summable, 2. $\sum_{y} \|g(y)\|$ and $\sum_{y} g(y)$ are summable. Then the product of the sums $(\sum_{x} f(x)) \cdot (\sum_{y} g(y))$ equals the sum $\sum_{(x,y) \in \iota \times \iota'} f(x) \cdot g(y)$.
summable_norm_sum_mul_antidiagonal_of_summable_norm theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖
Full source 
theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ := by
  have :=
    summable_sum_mul_antidiagonal_of_summable_mul
      (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
  refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)
  calc
    ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ :=
      norm_sum_le _ _
    _ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le
Summability of Norms of Cauchy Product Terms for Absolutely Summable Sequences
Informal description
Let $R$ be a normed ring, and let $f, g \colon \mathbb{N} \to R$ be sequences such that $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty \|g(n)\|$ are summable. Then the sequence $n \mapsto \left\|\sum_{(k,l) \in \text{antidiagonal}(n)} f(k) g(l)\right\|$ is summable, where $\text{antidiagonal}(n) = \{(k,l) \in \mathbb{N} \times \mathbb{N} \mid k + l = n\}$.
summable_sum_mul_antidiagonal_of_summable_norm' theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2
Full source 
theorem summable_sum_mul_antidiagonal_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    Summable fun n => ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
  summable_sum_mul_antidiagonal_of_summable_mul (summable_mul_of_summable_norm' hf h'f hg h'g)
Summability of Cauchy Product of Absolutely Summable Sequences in Normed Ring
Informal description
Let $R$ be a normed ring, and let $f, g \colon \mathbb{N} \to R$ be sequences such that: 1. $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty f(n)$ are summable 2. $\sum_{n=0}^\infty \|g(n)\|$ and $\sum_{n=0}^\infty g(n)$ are summable Then the sequence $n \mapsto \sum_{(k,l) \in \text{antidiagonal}(n)} f(k) \cdot g(l)$ is summable, where $\text{antidiagonal}(n) = \{(k,l) \in \mathbb{N} \times \mathbb{N} \mid k + l = n\}$.
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm theorem
[CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : ((∑' 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 infinite sums indexed by `ℕ`,
    expressed by summing on `Finset.antidiagonal`.
    See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
    *not* absolutely summable, and `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'`
    when the space is not complete. -/
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
  hf.of_norm.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg.of_norm (summable_mul_of_summable_norm hf hg)
Cauchy Product Formula for Absolutely Summable Series in Complete Normed Rings
Informal description
Let $R$ be a complete normed ring, and let $f, g \colon \mathbb{N} \to R$ be sequences such that $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty \|g(n)\|$ are summable. Then the product of their infinite sums can be expressed as: \[ \left(\sum_{n=0}^\infty f(n)\right) \left(\sum_{n=0}^\infty g(n)\right) = \sum_{n=0}^\infty \sum_{(k,l) \in \text{antidiagonal}(n)} f(k) g(l), \] where $\text{antidiagonal}(n) = \{(k,l) \in \mathbb{N} \times \mathbb{N} \mid k + l = n\}$.
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2
Full source 
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2 :=
  h'f.tsum_mul_tsum_eq_tsum_sum_antidiagonal  h'g (summable_mul_of_summable_norm' hf h'f hg h'g)
Cauchy Product Formula for Absolutely Summable Sequences in Normed Rings
Informal description
Let $R$ be a normed ring and let $f, g \colon \mathbb{N} \to R$ be sequences such that: 1. $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty f(n)$ are summable 2. $\sum_{n=0}^\infty \|g(n)\|$ and $\sum_{n=0}^\infty g(n)$ are summable Then the product of the infinite sums can be expressed as: $$\left(\sum_{n=0}^\infty f(n)\right) \left(\sum_{n=0}^\infty g(n)\right) = \sum_{n=0}^\infty \sum_{(k,l) \in \text{antidiagonal}(n)} f(k) g(l)$$ where $\text{antidiagonal}(n) = \{(k,l) \in \mathbb{N} \times \mathbb{N} \mid k+l = n\}$.
summable_norm_sum_mul_range_of_summable_norm theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : Summable fun n => ‖∑ k ∈ range (n + 1), f k * g (n - k)‖
Full source 
theorem summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)
    (hg : Summable fun x => ‖g x‖) : Summable fun n => ‖∑ k ∈ range (n + 1), f k * g (n - k)‖ := by
  simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
  exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
Summability of Norms in Cauchy Product for Absolutely Summable Sequences
Informal description
Let $R$ be a normed ring and let $f, g \colon \mathbb{N} \to R$ be sequences such that $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty \|g(n)\|$ are summable. Then the sequence defined by $$n \mapsto \left\|\sum_{k=0}^n f(k) g(n - k)\right\|$$ is summable.
summable_sum_mul_range_of_summable_norm' theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : Summable fun n => ∑ k ∈ range (n + 1), f k * g (n - k)
Full source 
theorem summable_sum_mul_range_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    Summable fun n => ∑ k ∈ range (n + 1), f k * g (n - k) := by
  simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
  exact summable_sum_mul_antidiagonal_of_summable_norm' hf h'f hg h'g
Summability of Cauchy Product via Range Summation for Absolutely Summable Sequences in Normed Rings
Informal description
Let $R$ be a normed ring and let $f, g \colon \mathbb{N} \to R$ be sequences such that: 1. $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty f(n)$ are summable 2. $\sum_{n=0}^\infty \|g(n)\|$ and $\sum_{n=0}^\infty g(n)$ are summable Then the sequence defined by $$n \mapsto \sum_{k=0}^n f(k) \cdot g(n-k)$$ is summable in $R$.
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm theorem
[CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : ((∑' 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 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, and `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'` when the
    space is not complete. -/
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k) := by
  simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg
Cauchy Product Formula for Absolutely Summable Series in Complete Normed Rings (Range Version)
Informal description
Let $R$ be a complete normed ring, and let $f, g \colon \mathbb{N} \to R$ be sequences such that $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty \|g(n)\|$ are summable. Then the product of their infinite sums can be expressed as: \[ \left(\sum_{n=0}^\infty f(n)\right) \left(\sum_{n=0}^\infty g(n)\right) = \sum_{n=0}^\infty \sum_{k=0}^n f(k) g(n - k). \]
hasSum_sum_range_mul_of_summable_norm theorem
[CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n)
Full source 
theorem hasSum_sum_range_mul_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n) := by
  convert (summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum
  exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm hf hg
Cauchy Product Formula for Absolutely Summable Series in Complete Normed Rings (Range Version)
Informal description
Let $R$ be a complete normed ring and let $f, g \colon \mathbb{N} \to R$ be sequences such that $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty \|g(n)\|$ are summable. Then the sequence defined by $$n \mapsto \sum_{k=0}^n f(k) g(n - k)$$ has sum equal to the product of the infinite sums: $$\left(\sum_{n=0}^\infty f(n)\right) \left(\sum_{n=0}^\infty g(n)\right).$$
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k)
Full source 
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ k ∈ range (n + 1), f k * g (n - k) := by
  simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm' hf h'f hg h'g
Cauchy Product Formula for Absolutely Summable Sequences in Normed Rings (Range Version)
Informal description
Let $R$ be a normed ring and let $f, g \colon \mathbb{N} \to R$ be sequences such that: 1. $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty f(n)$ are summable 2. $\sum_{n=0}^\infty \|g(n)\|$ and $\sum_{n=0}^\infty g(n)$ are summable Then the product of the infinite sums can be expressed as: $$\left(\sum_{n=0}^\infty f(n)\right) \left(\sum_{n=0}^\infty g(n)\right) = \sum_{n=0}^\infty \sum_{k=0}^n f(k) g(n-k)$$
hasSum_sum_range_mul_of_summable_norm' theorem
{f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n)
Full source 
theorem hasSum_sum_range_mul_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n) := by
  convert (summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum
  exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' hf h'f hg h'g
Cauchy Product Formula for Absolutely Summable Sequences in Normed Rings (Range Version)
Informal description
Let $R$ be a normed ring and let $f, g \colon \mathbb{N} \to R$ be sequences such that: 1. $\sum_{n=0}^\infty \|f(n)\|$ and $\sum_{n=0}^\infty f(n)$ are summable 2. $\sum_{n=0}^\infty \|g(n)\|$ and $\sum_{n=0}^\infty g(n)$ are summable Then the sequence defined by $$n \mapsto \sum_{k=0}^n f(k) \cdot g(n-k)$$ has sum equal to the product of the infinite sums: $$\sum_{n=0}^\infty \left( \sum_{k=0}^n f(k) g(n-k) \right) = \left( \sum_{n=0}^\infty f(n) \right) \left( \sum_{n=0}^\infty g(n) \right)$$
summable_of_absolute_convergence_real theorem
{f : ℕ → ℝ} : (∃ r, Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)) → Summable f
Full source 
lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
    (∃ r, Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)) → Summable f
  | ⟨r, hr⟩ => by
    refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
    · exact fun i ↦ norm_nonneg _
    · simpa only using hr
Absolute Convergence Implies Summability for Real Sequences
Informal description
For a sequence $(f_n)_{n \in \mathbb{N}}$ of real numbers, if there exists a real number $r \in \mathbb{R}$ such that the sequence of partial sums of absolute values $S_n = \sum_{i=0}^{n-1} |f_i|$ converges to $r$, then the series $\sum_{n=0}^\infty f_n$ is summable.