Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Real and complex ell one have the Schur property

Statement

Both ℓ1(R) and ℓ1(C) have the Schur property: every weakly convergent sequence in either space converges in the ℓ1 norm.

Facts & Assumptions

Given: K∈{R,C} and a sequence a(n)⇀a in ℓ1(K), with coordinates indexed by N={0,1,…}.

[F1]

The Schur property is the implication from weak convergence to norm convergence, equivalently the same implication for weakly null sequences (Schur property). Weak convergence is convergence under every bounded scalar-linear functional (Weak convergence of nets and sequences).

[F2]

By the definitions of ℓ∞ and ℓ1 (The sequence spaces c_0 and ell-infinity, Finite truncations approximate null and summable sequences), for either scalar field, if b∈ℓ∞(K) and c∈ℓ1(K), then

∑k∣ckbk∣≤∥b∥∞∥c∥1.

Thus the absolutely convergent series hb(c)=∑kckbk defines a bounded scalar-linear functional, with no conjugation in the complex pairing. Coordinate evaluation is the special case b=ek (The sequence spaces c_0 and ell-infinity, Finite truncations approximate null and summable sequences).

[F3]

If c∈ℓ1(K) and PNc retains coordinates 0,…,N, then ∑k>N∣ck∣=∥c−PNc∥1→0 (Finite truncations approximate null and summable sequences).

[F4]

Every nonempty subset of N has a least element (The well-ordering principle), and a deterministic successor rule can be iterated along N (The recursion theorem).

[F5]

A strictly increasing index map satisfies nj≥j (A strictly increasing index map satisfies nk≥k).

Proof

1.1F3F6algebra

First verify the Banach-space condition. Let (c(m)) be Cauchy in ℓ1(K). Each coordinate sequence is Cauchy because ∣ck(m)−ck(r)∣≤∥c(m)−c(r)∥1; let ck be its scalar limit by [F6]. Given η>0, take M such that ∥c(m)−c(r)∥1<η/2 for m,r≥M. For fixed m≥M and N, passage to the limit in the finite sum gives ∑k=0N∣ck−ck(m)∣≤η/2. Hence [F6] gives ∑k∣ck−ck(m)∣≤η/2, so c−c(m)∈ℓ1 and ∥c−c(m)∥1<η. In particular c=(c−c(M))+c(M)∈ℓ1. Thus both scalar versions of ℓ1 are complete and hence Banach.

2.1givenF1step 1.1

Put u(n)=a(n)−a. For every f∈(ℓ1(K))∗, f(u(n))=f(a(n))−f(a)→0, so (u(n)) is weakly null. By [F1] and step 1.1 it is enough to prove ∥u(n)∥1→0.

3.1step 2.1assume-contra

Suppose otherwise. Negating the definition of convergence supplies an ε>0 such that S:={n∈N:∥u(n)∥1≥ε} is cofinal in N: for every N it contains an n≥N. In particular S is nonempty.

4.1F2F3F4step 3.1

We recursively define strictly increasing indices n0<n1<⋯ and strictly increasing finite cutoffs N0<N1<⋯. Let n0 be the least element of S, and let N0 be the least N for which ∑k>N∣uk(n0)∣<ε/8; the latter set is nonempty by [F3]. Given (nj,Nj), coordinate evaluation is a bounded functional by [F2], so uk(n)→0 for each k≤Nj. Because this head is finite, eventually ∑k=0Nj∣uk(n)∣<ε/8. The cofinal set S therefore contains an n>nj satisfying this inequality. Take the least such n as nj+1, then take the least N>Nj with ∑k>N∣uk(nj+1)∣<ε/8, again using [F3]. Each least value is unique by [F4]. On the set of pairs (n,N) with n∈S and ∑k>N∣uk(n)∣<ε/8, these rules therefore define a total deterministic successor function; [F4] iterates it from (n0,N0) and assembles the entire sequence without a choice axiom.

5.1step 3.1step 4.1algebra

Define disjoint finite blocks I0={0,…,N0} and Ij={Nj−1+1,…,Nj} for j≥1. For j≥1, the construction and nj∈S give ∑k∈Ij∣uk(nj)∣≥∥u(nj)∥1−∑k=0Nj−1∣uk(nj)∣−∑k>Nj∣uk(nj)∣>3ε/4. For j=0 there is no old head, so the same block sum is greater than 7ε/8.

6.1F2F5step 5.1construct

Define one scalar sequence b=(bk) blockwise. If k∈Ij and uk(nj)≠0, put bk=sgn⁡(uk(nj)) when K=R, and put bk=uk(nj)‾/∣uk(nj)∣ when K=C; put bk=0 when that coordinate is zero. Because (Nj) is strictly increasing, [F5] gives Nj≥j; hence every natural k lies in exactly one of the disjoint blocks. Thus ∣bk∣≤1, so b∈ℓ∞(K), and the no-conjugation pairing from [F2] satisfies uk(nj)bk=∣uk(nj)∣ on Ij in both scalar fields.

7.1F2step 4.1step 5.1step 6.1

Let hb be the bounded functional supplied by [F2]. For j≥1, the triangle inequality, step 5.1, and the head and tail estimates in step 4.1 give ∣hb(u(nj))∣≥∑k∈Ij∣uk(nj)∣−∑k=0Nj−1∣uk(nj)∣−∑k>Nj∣uk(nj)∣>ε/2. For j=0, the block exceeds 7ε/8 and the only complementary tail is below ε/8, so the stronger bound ∣hb(u(n0))∣>3ε/4 holds.

8.1F1F5step 1.1step 2.1step 7.1discharge-contradiction: step 3.1∎

On the other hand, weak nullity in step 2.1 gives hb(u(n))→0. The indices (nj) are strictly increasing, and [F5] gives nj≥j, so the scalar subsequence hb(u(nj)) also tends to zero. This contradicts its uniform lower bound in step 7.1. Therefore ∥u(n)∥1→0, hence ∥a(n)−a∥1→0; [F1] and the completeness proved in step 1.1 establish the Schur property over both R and C. The construction used only least natural numbers, scalar completeness and recursion, not Countable Choice or any stronger choice principle.

Depends on

Used by

Dependency tree · two levels

53 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