Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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.

Square-summable families on an arbitrary index set and the space 2(I)

Definition

Throughout, F is R or C and families are indexed by an arbitrary set I, with no enumeration or countability assumed. Finite real lists use Finite sums and finite products, by recursion, and sums over finite subsets use A finite sum in a commutative monoid indexed by an arbitrary finite set in the additive monoid of the scalar field. Disjoint splitting is Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule, and scalar modulus estimates use Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive; all suprema and infima of real sets below are taken in the complete ordered field R (Complete ordered field (least-upper-bound property)) or in [0,+]R (The extended real line R=R{,+}, its order, and the arithmetic that is left undefined, Every subset of R has a least upper bound and a greatest lower bound in R, agreeing with the real supremum and infimum on nonempty sets bounded in R).

Sums of nonnegative families. Let (ci)iI be a family of nonnegative reals and let Fin(I) be the set of finite subsets of I, ordered by inclusion. Define

iIci:=sup{iFci  :  FFin(I)}[0,+].

The set of finite subsums is nonempty, since contributes the empty sum 0, so the supremum exists in [0,+]; it is a real number exactly when the finite subsums are bounded above in R, and + otherwise. For finite I the finite subsum at I is the largest of all finite subsums, because all terms are nonnegative, so the definition agrees with the finite sum; in particular iIci=0 when every ci is 0, and I= gives the empty sum 0.

Splitting identity and small tails. Fix a finite FI. Every finite GI splits as the disjoint union (GF)(GF), so iGci=iGFci+iGFciiFci+iIFci; conversely the finite G with FG satisfy iGci=iFci+iGFci. Taking suprema, with the constant iFci passing through the supremum,

iIci=iFci+iIFci.(1)

Consequently, if S:=iIci is finite, then for every real ε>0 there is a finite FI with iIFci<ε: the finite subsums form a nonempty bounded-above set with supremum S, so by the epsilon characterisation of the supremum (Epsilon characterisation of the supremum) some finite F has Sε<iFci, and (1) gives iIFci=SiFci<ε. Such an F is called a tail-control set for ε.

Sums of scalar families. Now let (ai)iI be a family in F and put sF:=iFai for finite FI. The set Fin(I) with inclusion is a directed preorder: it is nonempty and FG is a common upper bound of F and G (Directed preorders and nets). Hence (sF)FFin(I) is a net in F, the finite-subset net of the family, and the family is summable when this net converges (Convergence and cluster points of a net in a topological space). The scalar metric is the usual real metric or The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane. These metric spaces are Hausdorff by Distinct points of a metric space have disjoint balls around them. A net in F has at most one limit (A topological space is Hausdorff if and only if every net has at most one limit), so for a summable family the limit is unique and we write iIai:=limFsF for it. The family is absolutely summable when iIai<+ in the sense above.

Every absolutely summable family is summable, in ZF. Assume S:=iIai is finite and put SF:=iFai for finite F. For finite F,GI the triangle inequality for finite sums and the fact that a finite subsum is at most the whole nonnegative sum give

sFsGiFGaiSSFG.(2)

Now fix a real ε>0, let F0 be a tail-control set for ε, and let F,GF0 be finite. Then FGF0, so SSFGSSF0<ε and (2) gives sFsG<ε.

First suppose F=R. For each finite F define AF:=inf{sG:GF} and BF:=sup{sG:GF} over finite G. Both are real numbers, because sGSGS, so the two sets are nonempty and bounded, and AFBF. If HF then AHAF and BHBF. Let L:=supFAF and U:=infFBF. Since AFsFHBH for all finite F,H, we get LU. Moreover, the preceding estimate holds for every pair F,GF0; taking the supremum over F and the infimum over G gives BF0AF0ε. Hence 0ULBF0AF0ε for every ε>0, so L=U=:s. If FF0, then both sF and s lie in [AF0,BF0], and therefore sFsε.

If F=C, apply the real argument just proved to the families (Reai) and (Imai). They are absolutely summable because Reai,Imaiai. Their finite-subset nets converge to real numbers r and t, respectively, so sFr+it in C. Thus every absolutely summable real or complex family is summable. No choice principle is used: the construction uses only two-sided suprema in R.

Linearity and absolute value. If (ai) and (bi) are absolutely summable and λF, then so are (ai+bi) and (λai), and

iI(ai+bi)=iIai+iIbi,iIλai=λiIai,iIaiiIai,

because the corresponding identities hold for every finite subsum, both sides are limits of the corresponding finite-subset nets, and addition, scalar multiplication and the modulus are continuous. The splitting identity (1) likewise passes to absolutely summable scalar families: iIai=iFai+iIFai for every finite F, because finite subsums over sets containing F converge to the left-hand side and equal the finite sum over F plus the finite subsum of the tail, whose net converges to the tail sum.

The finite-dimensional Cauchy-Schwarz inequality. Let (uk)0k<m and (vk)0k<m be scalar lists, for mN and let tR. Every term of k<m(uktvk)2 is nonnegative, so for all real t

0k<muk22tk<mukvk+t2k<mvk2.

If k<mvk2>0, substituting t=(k<mukvk)/(k<mvk2) gives (k<mukvk)2(k<muk2)(k<mvk2); if k<mvk2=0 then every vk=0 and both sides are 0. In either case k<mukvk(k<muk2)1/2(k<mvk2)1/2 after taking square roots, and applying the modulus inequality for finite sums to ukvk also gives

k<mukvk(k<muk2)1/2(k<mvk2)1/2.(3)

The space 2(I). For a family a=(ai)iI in F define Q(a):=iIai2. If Q(a) is finite, set a2:=Q(a), using the nonnegative real square root of Square roots exist: a unique a0 with (a)2=a; the positives are {x2:x0}; if Q(a)=+, set a2:=+. This is a case definition, not exponentiation of an extended real. Let

2(I,F):={a=(ai)iI:a2<+}.

The set 2(I,F) is a vector space over F: it contains the zero family, is closed under scalar multiplication because λa2=λa2, and is closed under addition because (3) applied to finite subsums gives a+b2a2+b2<+. The same inequality is the triangle inequality for 2, which is moreover nonnegative, vanishes only for the zero family (an arbitrary sum of nonnegative terms with supremum 0 has every term 0) and satisfies λa2=λa2; thus 2 is a norm on 2(I,F). Finally the pairing a,b:=iIaibi is well defined on 2(I,F)×2(I,F), because aibi=aibi has finite nonnegative sum by (3); it is linear in the first variable, conjugate symmetric, positive definite, and satisfies a,a=a22, all by the corresponding finite identities and the linearity of the sum. Consequently 2(I,F) is an inner-product space, and ei2(I,F) denotes the family that is 1 at i and 0 elsewhere. Nothing here asserts that 2(I,F) is complete; that follows later, from an orthonormal basis of a Hilbert space.

Depends on

Used by

Dependency tree · two levels

65 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