Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

The complex continuous dual of ell-one is ell-infinity

Statement

For complex sequence spaces, with indices starting at zero, (C)1(C),bhb,hb(a)=n=0bnan is a complex-linear isometric bijection. There is no conjugation in this pairing.

Facts & Assumptions

Given: The spaces, maps, scalar field, and hypotheses in the statement above. All duals consist of linear functionals over the ambient field; evaluation has no conjugation.

[F1]

From The dual space X^* of a normed space and its dual norm, with its stated hypotheses: Let X be a normed space over the scalar field K, where K=R in the literal definition and K=C by the convention of rem-real-and-complex-normed-space-convention. The dual space of X is X:=B(X,K), the space of bounded linear functionals on X (def-space-of-bounded-linear-operators). Each fX is in particular a linear functional in the algebraic sense, so X is a subspace of the algebraic dual from def-algebraic-dual-and-linear-functional. The dual norm on X is the operator norm: fX:=f=sup{f(x):x1}.

[F2]

From The sequence spaces c_0 and ell-infinity, with its stated hypotheses: Let K=R or C, with absolute value in the real case and modulus a+ib=a2+b2 in the complex case. A scalar sequence here is a function x:NK, including index zero. Let ={x=(xn)nN:supnNxn<},c0={x:xn0}, both equipped with x=supnNxn. Thus c0 is a specified linear subspace of the bounded-sequence space . Here xn0 means that for every real ε>0 there is NN such that xn<ε for all nN. Addition and scalar multiplication are coordinatewise. The scalar triangle inequality makes bounded sequences and null sequences linear spaces and gives the triangle inequality for the displayed supremum norm. Absolute homogeneity follows coordinatewise, and a zero supremum forces every coordinate to vanish.

[F3]

From Finite truncations approximate null and summable sequences, with its stated hypotheses: Let K=R or C. Use coordinates indexed by N={0,1,}. Define 1(K)={a:n=0an<}, with coordinatewise operations and norm a1=nan. Let PN retain coordinates 0,,N and set all others to zero. Then xPNx0(xc0(K)),aPNa10(a1(K)).

Proof

1.1

For bounded b and a1(C), bnanba1. The series therefore defines a complex-linear functional with hbb, and depends complex-linearly on b.

F1F2F3
2.1

Since en1=1, hbhb(en)=bn for every n. Taking the supremum gives equality of norms; no maximizing coordinate is required. For b=0 this reads 0=0.

step 1.1
3.1

Given h1(C), let bn=h(en). Then bnh, so b. Truncation density gives h(a)=limNh(PNa)=nbnan. Hence the map is onto, and evaluation at en makes the coefficient sequence unique.

F1F2F3step 1.1

Depends on

Used by

Dependency tree · two levels

10 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