TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Tonelli's theorem for double series of nonnegative extended real numbers

Statement

For every double sequence $(a_{i j})_{i, j \in N}$ in $[0, + \infty]$ ,

$\sum_{i = 0}^{\infty} (\sum_{j = 0}^{\infty} a_{i j}) = \sup_{m, n \in N} \sum_{i < m} \sum_{j < n} a_{i j} = \sum_{j = 0}^{\infty} (\sum_{i = 0}^{\infty} a_{i j}),$

where every sum is the nonnegative extended sum of Series in the nonnegative extended real line. Thus the order of summation may be interchanged, even when the common value is $+ \infty$ .

Facts & Assumptions

Given: A double sequence $(a_{i j})_{i, j \in N}$ with $0 \leq a_{i j} \leq + \infty$ .

[L1]

For a nonnegative extended sequence, the partial sums start at the empty sum $0$ , increase, and the series is their supremum in $[0, + \infty]$ (Series in the nonnegative extended real line).

[L2]

Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound there, with $\sup \emptyset = - \infty$ and $\inf \emptyset = + \infty$ (Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ ).

[L3]

A natural-number-indexed finite family of nonempty sets has a choice function in ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Proof

technique · direct

1.1givenL1

Put $r_{i, n} : = \sum_{j < n} a_{i j}$ and $R_{m, n} : = \sum_{i < m} r_{i, n}$ . These finite sums exist for $m, n \in N$ , $R_{0, n} = R_{m, 0} = 0$ , and $R_{m, n}$ is nondecreasing in each index.

1.2L2

The set ${R_{m, n} : m, n \in N}$ is nonempty and bounded above by $+ \infty$ , so let $S : = \sup_{m, n} R_{m, n} \in [0, + \infty]$ .

2.1step 1.1L1L2L3choose

For fixed $m$ , $\sup_{n} R_{m, n} = \sum_{i < m} \sup_{n} r_{i, n}$ : the inequality $\leq$ follows from $r_{i, n} \leq \sup_{q} r_{i, q}$ ; for the reverse inequality, if one of the finitely many row suprema is $+ \infty$ then its partial sums make $R_{m, n}$ unbounded, while if they are all finite, for every $ε > 0$ finite choice selects for each $i < m$ an index $n_{i}$ with $r_{i, n_{i}} > \sup_{n} r_{i, n} - ε / m$ when $m > 0$ ; take the largest $n_{i}$ and use monotonicity. The case $m = 0$ is the empty equality $0 = 0$ .

3.1step 1.1step 1.2step 2.1L1L2

Repeating steps 1.1 and 2.1 with the two indices interchanged gives $\sum_{j} (\sum_{i} a_{i j}) = \sup_{n} \sup_{m} R_{m, n} = S$ .

3.2step 1.2step 2.1L1

By [L1] and step 2.1, $\sum_{i} (\sum_{j} a_{i j}) = \sup_{m} \sum_{i < m} \sup_{n} r_{i, n} = \sup_{m} \sup_{n} R_{m, n} = S$ .

4.1step 3.2step 3.1∎

Both iterated sums equal the supremum of the finite rectangular sums, so they equal one another; the argument includes zero rows, zero columns, infinite entries, and unbounded finite rectangles without subtraction or an undefined product.

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

T. Tao, An Introduction to Measure Theory, Theorem 0.0.2 (standard reference, not scraped)