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
Definition
Throughout, is or and families are indexed by an arbitrary set , 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, , and modulus is definite, multiplicative, and subadditive; all suprema and infima of real sets below are taken in the complete ordered field (Complete ordered field (least-upper-bound property)) or in (The extended real line , its order, and the arithmetic that is left undefined, Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in ).
Sums of nonnegative families. Let be a family of nonnegative reals and let be the set of finite subsets of , ordered by inclusion. Define
The set of finite subsums is nonempty, since contributes the empty sum , so the supremum exists in ; it is a real number exactly when the finite subsums are bounded above in , and otherwise. For finite the finite subsum at is the largest of all finite subsums, because all terms are nonnegative, so the definition agrees with the finite sum; in particular when every is , and gives the empty sum .
Splitting identity and small tails. Fix a finite . Every finite splits as the disjoint union , so ; conversely the finite with satisfy . Taking suprema, with the constant passing through the supremum,
Consequently, if is finite, then for every real there is a finite with : the finite subsums form a nonempty bounded-above set with supremum , so by the epsilon characterisation of the supremum (Epsilon characterisation of the supremum) some finite has , and (1) gives . Such an is called a tail-control set for .
Sums of scalar families. Now let be a family in and put for finite . The set with inclusion is a directed preorder: it is nonempty and is a common upper bound of and (Directed preorders and nets). Hence is a net in , 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 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 for it. The family is absolutely summable when in the sense above.
Every absolutely summable family is summable, in ZF. Assume is finite and put for finite . For finite the triangle inequality for finite sums and the fact that a finite subsum is at most the whole nonnegative sum give
Now fix a real , let be a tail-control set for , and let be finite. Then , so and (2) gives .
First suppose . For each finite define and over finite . Both are real numbers, because , so the two sets are nonempty and bounded, and . If then and . Let and . Since for all finite , we get . Moreover, the preceding estimate holds for every pair ; taking the supremum over and the infimum over gives . Hence for every , so . If , then both and lie in , and therefore .
If , apply the real argument just proved to the families and . They are absolutely summable because . Their finite-subset nets converge to real numbers and , respectively, so in . Thus every absolutely summable real or complex family is summable. No choice principle is used: the construction uses only two-sided suprema in .
Linearity and absolute value. If and are absolutely summable and , then so are and , and
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: for every finite , because finite subsums over sets containing converge to the left-hand side and equal the finite sum over plus the finite subsum of the tail, whose net converges to the tail sum.
The finite-dimensional Cauchy-Schwarz inequality. Let and be scalar lists, for and let . Every term of is nonnegative, so for all real
If , substituting gives ; if then every and both sides are . In either case after taking square roots, and applying the modulus inequality for finite sums to also gives
The space . For a family in define . If is finite, set , using the nonnegative real square root of Square roots exist: a unique with ; the positives are ; if , set . This is a case definition, not exponentiation of an extended real. Let
The set is a vector space over : it contains the zero family, is closed under scalar multiplication because , and is closed under addition because (3) applied to finite subsums gives . The same inequality is the triangle inequality for , which is moreover nonnegative, vanishes only for the zero family (an arbitrary sum of nonnegative terms with supremum has every term ) and satisfies ; thus is a norm on . Finally the pairing is well defined on , because has finite nonnegative sum by (3); it is linear in the first variable, conjugate symmetric, positive definite, and satisfies , all by the corresponding finite identities and the linearity of the sum. Consequently is an inner-product space, and denotes the family that is at and elsewhere. Nothing here asserts that is complete; that follows later, from an orthonormal basis of a Hilbert space.
Depends on
- Directed preorders and nets
- Convergence and cluster points of a net in a topological space
- A topological space is Hausdorff if and only if every net has at most one limit
- The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, its order, and the arithmetic that is left undefined
- Every subset of $\overline{\mathbb{R}}$ has a least upper bound and a greatest lower bound in $\overline{\mathbb{R}}$, agreeing with the real supremum and infimum on nonempty sets bounded in $\mathbb{R}$
- Finite sums and finite products, by recursion
- Complete ordered field (least-upper-bound property)
- Epsilon characterisation of the supremum
- Real and imaginary parts, complex conjugation, and modulus
- The real numbers
- A finite sum in a commutative monoid indexed by an arbitrary finite set
- Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- Distinct points of a metric space have disjoint balls around them
- The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
Used by
- A separable infinite-dimensional Hilbert space is ℓ² Corollary
- A compact operator can have nondense range Counterexample
- Compact does not imply Hilbert Schmidt Counterexample
- Compactness is not preserved by strong operator limits Counterexample
- Hilbert Schmidt does not imply trace class Counterexample
- Identity is compact iff the space is finite dimensional Counterexample
- The unilateral shift obstructs a cyclic linear trace extension Counterexample
- The unilateral shift obstructs a cyclic linear trace extension Counterexample
- Hilbert–Schmidt operator and Hilbert–Schmidt norm Definition
- Trace of a trace class operator Definition
- Diagonal Schatten class criteria on ell two Example
- Finite-rank truncations of a square-integrable kernel Example
- Functional calculus for a diagonal operator Example
- Polar decomposition of the unilateral shift Example
- Pvm of a diagonal normal operator Example
- The Fourier series of a sawtooth and the Basel sum Example
- The Fourier series of a square wave and the odd reciprocal-square sum Example
- The standard basis of ℓ²(ℕ) Example
- Only countably many coefficients of a square-summable family are nonzero Lemma
- Positive square root of a compact positive operator Lemma
- Square-summable orthogonal families have norm-convergent finite sums Lemma
- Schatten p classes Remark
- A Hilbert space with a given orthonormal basis is ℓ² of the index set Theorem
- Cyclicity of the trace Theorem
- Fourier expansion in a Hilbert space Theorem
- Fourier series converge in mean square Theorem
- Hilbert Schmidt operators form a two sided ideal Theorem
- Hilbert–Schmidt operators are compact Theorem
- L two kernels give Hilbert–Schmidt operators Theorem
- Parseval equivalences for an orthonormal family Theorem
- Riesz–Fischer: the Fourier coefficient map is onto the space of square-summable families Theorem
- Singular value decomposition for compact operators Theorem
- Spectral theorem for compact self adjoint operators Theorem
- The Bessel inequality for an arbitrary orthonormal family Theorem
- The Hilbert–Schmidt norm is basis independent Theorem
- The Parseval identity for Fourier series Theorem
- Trace class iff product of two Hilbert Schmidt operators Theorem
- Trace is absolutely convergent and basis independent Theorem
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
- Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.1, pp.48–49 and p.52 (standard reference, not scraped)
- Theo Bühler and Dietmar Salamon, Functional Analysis — Exercise 2.64, p.87 (standard reference, not scraped)