Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

Fubini for double series: if ∑i∑j∣aij∣ converges then both iterated sums and the sum along every bijection N→N×N converge to one and the same value

Statement

Let a:N×N→R be a doubly indexed array of reals, written aij. Assume:

(H) for every i the series ∑j∣aij∣ converges, with sum Ai; and the series ∑iAi converges, with sum L.

Then, with J:N→N×N any bijection (N×N≈N, Injection, surjection, bijection):

  1. ∑naJ(n) converges absolutely (Absolutely convergent and conditionally convergent series, and the general starting index), and its sum S is the same for every such bijection (Dirichlet's rearrangement theorem: an absolutely convergent series converges unconditionally, and every rearrangement of it has the same sum);
  2. for every i the series ∑jaij converges, say to Ri; the series ∑iRi converges absolutely; and ∑i=0∞Ri=S;
  3. for every j the series ∑i∣aij∣ converges and ∑iaij converges, say to Cj; the series ∑jCj converges absolutely; and ∑j=0∞Cj=S.

In particular the two iterated sums exist and agree:

∑i=0∞(∑j=0∞aij)  =  ∑j=0∞(∑i=0∞aij)  =  ∑n=0∞aJ(n).

The hypothesis is on the absolute values, and it is stated as an iterated condition, not as an unqualified "double sum". Each row must be absolutely summable, and the row totals must themselves be summable. Without it the two iterated sums may both exist and differ, which is FALSE: whenever both iterated sums of a double array exist, they are equal.

Facts & Assumptions

Given: An array a:N×N→R satisfying (H), with row totals Ai and L=∑i=0∞Ai, and a bijection J:N→N×N.

[L1]

Finite sums: the empty sum is 0, ∑k<n+1xk=∑k<nxk+xn, finite sums are additive, monotone in their terms, and may be split at any intermediate index (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L2]

For a series of nonnegative terms, convergence is equivalent to the range of the partial sums being bounded above; then the sum is the supremum of that range, every partial sum is at most the sum, and the partial sums converge to it (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L4]

∣∑k<nxk∣≤∑k<n∣xk∣ (Triangle inequality for finite sums).

[L5]

Absolute value: ∣x∣≥0, −∣x∣≤x≤∣x∣, and ∣x∣=0 exactly when x=0 (Basic properties of the absolute value).

[L6]

The principle of induction on N (The principle of mathematical induction).

[L7]

A bijection is an injective surjection; N×N admits a bijection with N (Injection, surjection, bijection, N×N≈N).

[L10]

Proof

technique · direct
1.1

Rectangles are bounded by L. For all P,Q∈N one has ∑i<P∑j<Q∣aij∣≤∑i<PAi≤L, since each inner sum is a partial sum of the convergent nonnegative series ∑j∣aij∣ and so is at most Ai, and finite sums are monotone.

givenL1L2
1.2

Single points. Let d:N×N→R vanish except at one pair (p,q), let N∈N and let ρ be injective on {n:n<N} with values in N×N. If (p,q)=ρ(n0) for some (necessarily unique) n0<N, then ∑n<Ndρ(n)=dpq; otherwise ∑n<Ndρ(n)=0. Both follow by splitting the sum at n0 and at n0+1, all remaining terms being 0.

L1L7
1.3

List dominated by a rectangle. For every N∈N, every array (cij) of nonnegative reals, all P,Q∈N and every injective ρ on {n:n<N} with values in {(i,j):i<P, j<Q}, one has ∑n<Ncρ(n)≤∑i<P∑j<Qcij. Induction on N, everything else universally quantified: at N=0 the left side is 0 and the right side is nonnegative; and passing from N to N+1, put (p,q):=ρ(N) and let c′′ agree with c except that cpq′′:=0, so that the induction hypothesis applied to c′′ and ρ restricted gives ∑n<Ncρ(n)≤∑i<P∑j<Qcij−cpq, the subtraction coming from splitting the outer sum at p and the inner one at q; adding cpq closes the induction.

L1L6
1.4

Bounding indices. For every N there are P,Q with J(n)∈{(i,j):i<P, j<Q} for all n<N; and for all P,Q there is N with {(i,j):i<P, j<Q}⊆{J(n):n<N}. Both are inductions using that the order on N is total, so that finitely many naturals have a strict upper bound; the second uses surjectivity of J to name, for each pair, the index mapping onto it.

L6L7
1.5

For every i the series ∑jaij converges, since ∑j∣aij∣ does; write Ri for its sum, so ∣Ri∣≤Ai by [L4] and [L10]. Hence ∑i∣Ri∣ converges by comparison with ∑iAi, and ∑iRi converges absolutely.

givenL2L3L4L8L10
1.6

Let ε>0 be real. Choose P0≥1 with L−∑i<P0Ai<ε, possible because the partial sums of ∑iAi converge to L; then choose, for each i<P0, an index Qi with Ai−∑j<Qi∣aij∣<ε/P0, and let Q0 be an upper bound of the finitely many Qi, so that Ai−∑j<Q0∣aij∣<ε/P0 for every i<P0.

givenL2L6choose
2.1

Rectangle to list. Let c be an array, let P,Q,N∈N and let ρ be injective on {n:n<N} with {(i,j):i<P, j<Q}⊆{ρ(n):n<N}. Let c′ agree with c on that rectangle and vanish off it. Then ∑i<P∑j<Qcij=∑n<Ncρ(n)′. This is proved by induction on P, with an inner induction on Q: enlarging the rectangle by one column adds the single term cPQ to the left side, and changes c′ by an array vanishing except at (P,Q), which by step 1.2 adds exactly cPQ to the right side; at P=0 or Q=0 both sides are 0.

step 1.2L1L6
2.2

By step 1.3 and step 1.4, every partial sum ∑n<N∣aJ(n)∣ is at most ∑i<P∑j<Q∣aij∣≤L; hence ∑n∣aJ(n)∣ converges, with sum Λ≤L, and ∑naJ(n) converges, say to S. Any two bijections N→N×N differ by a bijection of N, so by [L9] the value S does not depend on J; this is claim 1.

step 1.1step 1.3step 1.4L2L8L9
2.3

Write D:=∑i<P0∑j<Q0aij and E:=∑i<P0∑j<Q0∣aij∣. By step 1.6 and monotonicity, E>∑i<P0(Ai−ε/P0)=∑i<P0Ai−ε>L−2ε, so L−E<2ε.

step 1.6L1
2.4

By step 1.4 fix N with {(i,j):i<P0, j<Q0}⊆{J(n):n<N}, and by step 1.4 again fix P≥P0, Q≥Q0 with J(n) in the rectangle {(i,j):i<P, j<Q} for all n<N.

step 1.4choose
2.5

The transposed array aijT:=aji satisfies (H): its i-th row total is ∑j∣aji∣, which converges because its partial sums ∑j<Q∣aji∣ are bounded by L by step 1.1; and the partial sums ∑i<P∑j∣aji∣ are limits of the rectangle sums ∑i<P∑j<Q∣aji∣, again bounded by L by step 1.1, so the series of row totals converges.

step 1.1L1L2L10
3.1

For every N, ∣S−∑n<NaJ(n)∣≤Λ−∑n<N∣aJ(n)∣: for M>N the triangle inequality gives ∣∑n<MaJ(n)−∑n<NaJ(n)∣≤∑n<M∣aJ(n)∣−∑n<N∣aJ(n)∣≤Λ−∑n<N∣aJ(n)∣, and letting M grow, the limit preserves the two non-strict inequalities bounding the left side.

step 2.2L1L4L10
3.2

Let a′ agree with a on the rectangle {(i,j):i<P0, j<Q0} and vanish off it. By step 2.1, D=∑n<NaJ(n)′ and E=∑n<N∣aJ(n)′∣; since ∣aJ(n)′∣≤∣aJ(n)∣ termwise, monotonicity gives E≤∑n<N∣aJ(n)∣≤Λ≤L.

step 2.1step 2.2step 2.4L1L2
4.1

By step 3.1 and step 3.2, ∣S−∑n<NaJ(n)∣≤Λ−∑n<N∣aJ(n)∣≤L−E<2ε.

step 3.1step 2.3step 3.2
4.2

Also ∣∑n<NaJ(n)−D∣=∣∑n<N(a−a′)J(n)∣≤∑n<N∣(a−a′)J(n)∣≤∑i<P∑j<Q∣(a−a′)ij∣=∑i<P∑j<Q∣aij∣−E≤L−E<2ε, the middle inequality by step 1.3 and the following equality by splitting the iterated sum at P0 and at Q0, the array a−a′ agreeing with a off the small rectangle and vanishing on it.

step 1.1step 2.1step 1.3step 2.3step 2.4step 3.2L1L4
4.3

For each i<P0, ∣Ri−∑j<Q0aij∣≤Ai−∑j<Q0∣aij∣<ε/P0, by the argument of step 3.1 applied to the row i; summing over i<P0 gives ∣∑i<P0Ri−D∣<ε.

step 3.1step 1.6L1L4
4.4

Writing ΣR for the sum of ∑iRi, the same argument applied to the series ∑iRi and the comparison ∣Ri∣≤Ai gives ∣ΣR−∑i<P0Ri∣≤∑i=0∞∣Ri∣−∑i<P0∣Ri∣≤L−∑i<P0Ai<ε.

step 3.1step 1.5step 1.6L1L2
5.1

Combining step 4.1, step 4.2, step 4.3 and step 4.4, ∣ΣR−S∣<ε+ε+2ε+2ε=6ε. As ε>0 was arbitrary and ∣ΣR−S∣≥0, this forces ΣR=S, which with step 1.5 is claim 2.

step 1.5step 4.1step 4.2step 4.3step 4.4L5
6.1

Applying claims 1 and 2 to aT and to the bijection JT obtained by exchanging the coordinates of J gives claim 3, since aJT(n)T=aJ(n) for every n, so the two linear series are the same series and have the same sum S.

step 2.2step 5.1step 2.5L7∎

Remarks

  • What the finite bookkeeping of steps 1.2 to 1.5 does, and why it is proved. Three facts are needed and none of them is among the laws of Laws of finite sums and finite products, all of which compare sums term by term over the same index range: that a sum along an injective list picks up an isolated term exactly once; that an iterated sum over a rectangle equals the sum along any injective list containing that rectangle, of the array cut down to it; and that a sum of nonnegative terms along an injective list into a rectangle is at most the iterated sum over the rectangle. Each is proved by zeroing out one entry at a time, which keeps the argument inside those laws.

  • Where the hypothesis is used. Only through step 1.1, which bounds every rectangle by L, and through step 1.6, which makes a single rectangle capture all but 2ε of the total mass. Everything else is bookkeeping. This is why the hypothesis has to be an absolute one: for a signed array no rectangle captures the mass, and the two iterated sums can disagree.

  • The independence of the enumeration is Dirichlet's rearrangement theorem: an absolutely convergent series converges unconditionally, and every rearrangement of it has the same sum and nothing more. Two bijections N→N×N differ by a bijection of N, and an absolutely convergent series is unconditionally convergent. So the "sum of the array" is a well-defined real number attached to the array itself, and the theorem says the two iterated sums compute it.

Depends on

Used by

Dependency tree · two levels

79 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