Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Dvoretzky--Rogers theorem

Statement

Assume Countable Choice. Every infinite-dimensional real or complex Banach space contains an unconditionally convergent series that is not absolutely convergent.

Facts & Assumptions

[A1]
[L1]

Each sufficiently high-dimensional finite block admits vectors with prescribed squared norms and the uniform subset-sum estimate (The Dvoretzky--Rogers finite-block estimate).

[L2]

Uniform smallness of all finite tails is equivalent to unconditional convergence in a Banach space (Equivalent forms of unconditional convergence).

Proof

technique · construction

Given: The objects and hypotheses in the Statement.

1.1given

Put cn=(8n2)−1 for n≥1. Since ∑n≥1n−2<2, we have ∑ncn<1/4, while ∑ncn=8−1/2∑n1/n=∞. Put N1=1 and, for m≥2, recursively take Nm to be the least integer greater than Nm−1 such that ∑n≥Nmcn<4−m. Thus

∑m(∑Nm≤n<Nm+1cn)1/2<∞.

[explicit least-index recursion, scalar series]

2.1givenA1L1step 1.1

Let rm=Nm+1−Nm. Infinite-dimensionality supplies a subspace of dimension at least rm(rm−1) (the cases rm≤1 are chosen directly). Use [A1] exactly here to select, for all m, one family (xn)Nm≤n<Nm+1 given by [L1] with dn=cn. Then ∥xn∥=1/(8n) and every subset F of the mth block satisfies

∥∑n∈Fxn∥≤3(∑n∈Fcn)1/2.

[A1, L1, step 1.1]

3.1givenL2step 2.1step 1.1

For any finite set F contained in the tail beginning at NM, split it by blocks and use the triangle inequality and step 2.1:

∥∑n∈Fxn∥≤3∑m≥M(∑Nm≤n<Nm+1cn)1/2.

The right side tends to zero by step 1.1. Condition (3) of [L2] therefore holds, so ∑nxn converges unconditionally. [L2, steps 1.1, 2.1]

4.1step 2.1algebra∎

On the other hand, [given, step 2.1, step 3.1] ∑n∥xn∥=8−1/2∑n1/n=∞, so the same series is not absolutely convergent.

Depends on

Used by

Dependency tree · two levels

11 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