Theorem 8.3 — interchanging the order of summation

Proved

Rudin.ch08_double_series

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisseries

Given a double sequence $a_{ij}$ , suppose $\sum_j |a_{ij}| = b_i$ converges for each $i$ and $\sum_i b_i$ converges. Then the two iterated sums $\sum_i \sum_j a_{ij}$ and $\sum_j \sum_i a_{ij}$ both converge and are equal.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch03_series

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.3: given a double sequence `a i j`, if `∑_j |a i j| = b i` for each `i`
and `∑ b i` converges, then the two iterated sums of `a i j` converge and are equal. -/
theorem ch08_double_series (a : ℕ → ℕ → ℝ) (b : ℕ → ℝ)
    (hb : ∀ i, SeriesConvergesTo (fun j => |a i j|) (b i)) (hbsum : SeriesConverges b) :
    ∃ S : ℝ,
      SeriesConvergesTo (fun i => ∑' j, a i j) S ∧
      SeriesConvergesTo (fun j => ∑' i, a i j) S := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 175, Theorem 8.3

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $a : \mathbb{N}\times\mathbb{N} \to \mathbb{R}$ (written $a_{ij}$ ) and $b : \mathbb{N}\to\mathbb{R}$ . Assume:

for every $i$ , the partial sums of $\sum_j |a_{ij}|$ converge to $b_i$ ;
the partial sums of $\sum_i b_i$ converge to some real number.

Then there exists a real number $S$ such that both iterated series converge to it:

\sum_i \Bigl(\textstyle\sum'_j a_{ij}\Bigr) = S \qquad\text{and}\qquad \sum_j \Bigl(\textstyle\sum'_i a_{ij}\Bigr) = S,

where the inner sums $\sum'$ denote unconditional sums of the families (equal to the ordinary sum when the family is summable, and $0$ otherwise), and the outer convergence is convergence of the partial sums.

The conclusion asserts the common value of the two iterated sums but gives no formula for $S$ in terms of $b$ .

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph