Orthonormal Bases, Parseval and Fourier Series

Let $H$ be a real or complex inner-product space (Real and complex inner-product spaces and their induced length), with inner product linear in the first argument and conjugate-linear in the second, and with the induced length $\mathrm{\parallel }v\mathrm{\parallel }=\sqrt{⟨v,v⟩}$. The definitions below do not require completeness. When the term Hilbert basis is used, $H$ is additionally assumed complete (Hilbert space).

Orthonormal indexed family. Let $I$ be any set. An indexed family $(e_i{)}_{i\in I}$ of vectors of $H$ is orthonormal when

$⟨e_i,e_j⟩={\delta }_{ij}:=\{\begin{array}{ll}1,& i=j,\\ 0,& i\mathrm{\ne }j,\end{array}\text{for all }i,j\in I\mathrm{.}$Because $1\mathrm{\ne }0$ in the scalar field, the family contains no zero vector: $\mathrm{\parallel }{e}_i{\mathrm{\parallel }}^2=⟨e_i,e_i⟩=1$, so $\mathrm{\parallel }{e}_i\mathrm{\parallel }=1$ for every $i$ (Real and complex inner-product spaces and their induced length); and the index map is injective, since $e_i=e_j$ with $i\mathrm{\ne }j$ would give $0=⟨e_i,e_j⟩=1$. Thus an orthonormal family is the same thing as an orthonormal set together with a labelling of it, and in the sequel no choice is hidden in passing between the two descriptions. Orthonormal set. A subset $S\subseteq H$ is orthonormal when every $s\in S$ has $\mathrm{\parallel }s\mathrm{\parallel }=1$ and $⟨s,t⟩=0$ for all distinct $s,t\in S$. For such an $S$ the family $(e_s{)}_{s\in S}$ with $e_s:=s$ is orthonormal in the indexed sense, and the image of an orthonormal indexed family is an orthonormal set. Orthogonal means $⟨s,t⟩=0$ (Orthogonality and the orthogonal complement). Independence and unique coefficients. Let $(e_i{)}_{i\in I}$ be orthonormal, let $F\subseteq I$ be finite, and let scalars $c_i$ satisfy ${\sum }_{i\in F}{c}_i{e}_i=0$. For each fixed $j\in F$, linearity in the first argument gives$0=⟨{\sum }_{i\in F}{c}_i{e}_i,e_j⟩={\sum }_{i\in F}{c}_i⟨e_i,e_j⟩=c_j,$

so every finite subfamily of an orthonormal family is linearly independent. In particular the coefficients in a finite expansion are unique: if ${\sum }_{i\in F}{c}_i{e}_i={\sum }_{i\in F}{d}_i{e}_i$, then applying the computation to $c-d$ gives $c_i=d_i$ for every $i\in F$.

Closed linear span and completeness. The span of an indexed family is the set of all finite linear combinations ${\sum }_{i\in F}{c}_i{e}_i$ with $F\subseteq I$ finite and scalars $c_i$; it is the smallest linear subspace of $H$ containing every $e_i$ (Linear subspace of a vector space). Its closure in the induced norm is the closed linear span of the family, the smallest closed linear subspace of $H$ containing every $e_i$. The family is complete, or is a complete orthonormal system, when its closed linear span is all of $H$. A Hilbert basis, or orthonormal basis, of $H$ is a complete orthonormal family in $H$.

The empty family. The span of the empty family is $\{0\}$, which is already closed, so the empty family is complete exactly when $H=\{0\}$. Thus the zero Hilbert space always has a Hilbert basis, namely the empty one.

Not a Hamel basis, and no order is assumed. A Hilbert basis is a basis only in the sense of closed linear span: for an infinite-dimensional $H$ the vectors of $H$ are in general not finite linear combinations of a Hilbert basis, and the expansion of an arbitrary vector is a norm limit of finite partial sums, not a finite sum. No enumeration, ordering or countability of the index set is part of the definition; the partial sums are indexed by the finite subsets of $I$, ordered by inclusion, and that is the convention used on this page.

Coefficient notation. For orthonormal $(e_i{)}_{i\in I}$ and $x\in H$ the scalars $⟨x,e_i⟩$ are the coefficients of $x$ with respect to the family. They are well defined for every $x$, without any assumption that the family is complete.

Let $(e_i{)}_{i\in I}$ be an orthonormal family in a real or complex inner-product space $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases), let $F\subseteq I$ be finite, and for $x\in H$ put

$P_{F}x:={\sum }_{i\in F}⟨x,e_i⟩e_i\mathrm{.}$Then: 1. $P_{F}x$ lies in the span of $\{e_i:i\in F\}$, and $\mathrm{\parallel }{P}_{F}x{\mathrm{\parallel }}^2={\sum }_{i\in F}\mathrm{\mid }⟨x,e_i⟩{\mathrm{\mid }}^2$; 2. the residual $x-P_{F}x$ is orthogonal to every $e_j$ with $j\in F$, hence to every vector of the span of $\{e_i:i\in F\}$; 3. $\mathrm{\parallel }x-P_{F}x{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2-{\sum }_{i\in F}\mathrm{\mid }⟨x,e_i⟩{\mathrm{\mid }}^2$, and therefore the finite Bessel inequality holds:${\sum }_{i\in F}\mathrm{\mid }⟨x,e_i⟩{\mathrm{\mid }}^2\le \mathrm{\parallel }x{\mathrm{\parallel }}^2;$4. $P_{F}x$ is the unique best approximation to $x$ from the span of $\{e_i:i\in F\}$: for every $y$ in that span,$\mathrm{\parallel }x-y{\mathrm{\parallel }}^2=\mathrm{\parallel }x-P_{F}x{\mathrm{\parallel }}^2+\mathrm{\parallel }{P}_{F}x-y{\mathrm{\parallel }}^2\ge \mathrm{\parallel }x-P_{F}x{\mathrm{\parallel }}^2,$ with equality if and only if $y=P_{F}x$.

At $F=\mathrm{\varnothing }$ the sum defining $P_{F}x$ is empty, so $P_{F}x=0$ and the identities read $\mathrm{\parallel }x{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2$.

Throughout, $\mathbb{F}$ is $\mathbb{R}$ or $\mathbb{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, $z\bar{z}=\mathrm{\mid }z{\mathrm{\mid }}^2$, and modulus is definite, multiplicative, and subadditive; all suprema and infima of real sets below are taken in the complete ordered field $\mathbb{R}$ (Complete ordered field (least-upper-bound property)) or in $[0,+\mathrm{\infty }]\subseteq \bar{\mathbb{R}}$ (The extended real line $\bar{\mathbb{R}}=\mathbb{R}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$, its order, and the arithmetic that is left undefined, Every subset of $\bar{\mathbb{R}}$ has a least upper bound and a greatest lower bound in $\bar{\mathbb{R}}$, agreeing with the real supremum and infimum on nonempty sets bounded in $\mathbb{R}$).

Sums of nonnegative families. Let $(c_i{)}_{i\in I}$ be a family of nonnegative reals and let $\mathrm{Fin}(I)$ be the set of finite subsets of $I$, ordered by inclusion. Define

${\sum }_{i\in I}{c}_i:=\sup \{{\sum }_{i\in F}{c}_i:F\in \mathrm{Fin}(I)\}\in [0,+\mathrm{\infty }]\mathrm{.}$

The set of finite subsums is nonempty, since $\mathrm{\varnothing }$ contributes the empty sum $0$, so the supremum exists in $[0,+\mathrm{\infty }]$; it is a real number exactly when the finite subsums are bounded above in $\mathbb{R}$, and $+\mathrm{\infty }$ 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 ${\sum }_{i\in I}{c}_i=0$ when every $c_i$ is $0$, and $I=\mathrm{\varnothing }$ gives the empty sum $0$.

Splitting identity and small tails. Fix a finite $F\subseteq I$. Every finite $G\subseteq I$ splits as the disjoint union $(G\cap F)\cup (G\setminus F)$, so ${\sum }_{i\in G}{c}_i={\sum }_{i\in G\cap F}{c}_i+{\sum }_{i\in G\setminus F}{c}_i\le {\sum }_{i\in F}{c}_i+{\sum }_{i\in I\setminus F}{c}_i$; conversely the finite $G$ with $F\subseteq G$ satisfy ${\sum }_{i\in G}{c}_i={\sum }_{i\in F}{c}_i+{\sum }_{i\in G\setminus F}{c}_i$. Taking suprema, with the constant ${\sum }_{i\in F}{c}_i$ passing through the supremum,

${\sum }_{i\in I}{c}_i={\sum }_{i\in F}{c}_i+{\sum }_{i\in I\setminus F}{c}_i\mathrm{.}(1)$

Consequently, if $S:={\sum }_{i\in I}{c}_i$ is finite, then for every real $\epsilon >0$ there is a finite $F\subseteq I$ with ${\sum }_{i\in I\setminus F}{c}_i<\epsilon$: 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-\epsilon <{\sum }_{i\in F}{c}_i$, and (1) gives ${\sum }_{i\in I\setminus F}{c}_i=S-{\sum }_{i\in F}{c}_i<\epsilon$. Such an $F$ is called a tail-control set for $\epsilon$.

Sums of scalar families. Now let $(a_i{)}_{i\in I}$ be a family in $\mathbb{F}$ and put $s_F:={\sum }_{i\in F}{a}_i$ for finite $F\subseteq I$. The set $\mathrm{Fin}(I)$ with inclusion is a directed preorder: it is nonempty and $F\cup G$ is a common upper bound of $F$ and $G$ (Directed preorders and nets). Hence $(s_F{)}_{F\in \mathrm{Fin}(I)}$ is a net in $\mathbb{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 $\mathbb{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 ${\sum }_{i\in I}{a}_i:={\lim }_F{s}_F$ for it. The family is absolutely summable when ${\sum }_{i\in I}\mathrm{\mid }{a}_i\mathrm{\mid }<+\mathrm{\infty }$ in the sense above.

Every absolutely summable family is summable, in ZF. Assume $S:={\sum }_{i\in I}\mathrm{\mid }{a}_i\mathrm{\mid }$ is finite and put $S_F:={\sum }_{i\in F}\mathrm{\mid }{a}_i\mathrm{\mid }$ for finite $F$. For finite $F,G\subseteq I$ the triangle inequality for finite sums and the fact that a finite subsum is at most the whole nonnegative sum give

$\mathrm{\mid }{s}_F-s_G\mathrm{\mid }\le {\sum }_{i\in F\mathrm{△}G}\mathrm{\mid }{a}_i\mathrm{\mid }\le S-S_{F\cap G}\mathrm{.}(2)$

Now fix a real $\epsilon >0$, let $F_0$ be a tail-control set for $\epsilon$, and let $F,G\supseteq F_0$ be finite. Then $F\cap G\supseteq F_0$, so $S-S_{F\cap G}\le S-S_{F_0}<\epsilon$ and (2) gives $\mathrm{\mid }{s}_F-s_G\mathrm{\mid }<\epsilon$.

First suppose $\mathbb{F}=\mathbb{R}$. For each finite $F$ define $A_F:=\inf \{s_G:G\supseteq F\}$ and $B_F:=\sup \{s_G:G\supseteq F\}$ over finite $G$. Both are real numbers, because $\mathrm{\mid }{s}_G\mathrm{\mid }\le S_G\le S$, so the two sets are nonempty and bounded, and $A_F\le B_F$. If $H\supseteq F$ then $A_H\ge A_F$ and $B_H\le B_F$. Let $L:={\sup }_F{A}_F$ and $U:={\inf }_F{B}_F$. Since $A_F\le s_{F\cup H}\le B_H$ for all finite $F,H$, we get $L\le U$. Moreover, the preceding estimate holds for every pair $F,G\supseteq F_0$; taking the supremum over $F$ and the infimum over $G$ gives $B_{F_0}-A_{F_0}\le \epsilon$. Hence $0\le U-L\le B_{F_0}-A_{F_0}\le \epsilon$ for every $\epsilon >0$, so $L=U=:s$. If $F\supseteq F_0$, then both $s_F$ and $s$ lie in $[A_{F_0},B_{F_0}]$, and therefore $\mathrm{\mid }{s}_F-s\mathrm{\mid }\le \epsilon$.

If $\mathbb{F}=\mathbb{C}$, apply the real argument just proved to the families $(\mathrm{Re}{a}_i)$ and $(\mathrm{Im}{a}_i)$. They are absolutely summable because $\mathrm{\mid }\mathrm{Re}{a}_i\mathrm{\mid },\mathrm{\mid }\mathrm{Im}{a}_i\mathrm{\mid }\le \mathrm{\mid }{a}_i\mathrm{\mid }$. Their finite-subset nets converge to real numbers $r$ and $t$, respectively, so $s_F\to r+it$ in $\mathbb{C}$. Thus every absolutely summable real or complex family is summable. No choice principle is used: the construction uses only two-sided suprema in $\mathbb{R}$.

Linearity and absolute value. If $(a_i)$ and $(b_i)$ are absolutely summable and $\lambda \in \mathbb{F}$, then so are $(a_i+b_i)$ and $(\lambda a_i)$, and

${\sum }_{i\in I}(a_i+b_i)={\sum }_{i\in I}{a}_i+{\sum }_{i\in I}{b}_i,{\sum }_{i\in I}\lambda a_i=\lambda {\sum }_{i\in I}{a}_i,\mid {\sum }_{i\in I}{a}_i\mid \le {\sum }_{i\in I}\mathrm{\mid }{a}_i\mathrm{\mid },$

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: ${\sum }_{i\in I}{a}_i={\sum }_{i\in F}{a}_i+{\sum }_{i\in I\setminus F}{a}_i$ 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 $(u_k{)}_{0\le k<m}$ and $(v_k{)}_{0\le k<m}$ be scalar lists, for $m\in \mathbb{N}$ and let $t\in \mathbb{R}$. Every term of ${\sum }_{k<m}(\mathrm{\mid }{u}_k\mathrm{\mid }-t\mathrm{\mid }{v}_k\mathrm{\mid }{)}^2$ is nonnegative, so for all real $t$

$0\le {\sum }_{k<m}\mathrm{\mid }{u}_k{\mathrm{\mid }}^2-2t{\sum }_{k<m}\mathrm{\mid }{u}_k\mathrm{\mid }\mathrm{\mid }{v}_k\mathrm{\mid }+t^2{\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2\mathrm{.}$

If ${\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2>0$, substituting $t=\left({\sum }_{k<m}\mathrm{\mid }{u}_k\mathrm{\mid }\mathrm{\mid }{v}_k\mathrm{\mid }\right)\mathrm{/}\left({\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2\right)$ gives $({\sum }_{k<m}\mathrm{\mid }{u}_k\mathrm{\mid }\mathrm{\mid }{v}_k\mathrm{\mid }{)}^2\le ({\sum }_{k<m}\mathrm{\mid }{u}_k{\mathrm{\mid }}^2\left)\right({\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2)$; if ${\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2=0$ then every $v_k=0$ and both sides are $0$. In either case ${\sum }_{k<m}\mathrm{\mid }{u}_k\mathrm{\mid }\mathrm{\mid }{v}_k\mathrm{\mid }\le \left({\sum }_{k<m}\mathrm{\mid }{u}_k{\mathrm{\mid }}^2{)}^{1\mathrm{/}2}\right({\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2{)}^{1\mathrm{/}2}$ after taking square roots, and applying the modulus inequality for finite sums to $u_k\overline{v_k}$ also gives

$\mid {\sum }_{k<m}{u}_k\overline{v_k}\mid \le \left({\sum }_{k<m}\mathrm{\mid }{u}_k{\mathrm{\mid }}^2{)}^{1\mathrm{/}2}\right({\sum }_{k<m}\mathrm{\mid }{v}_k{\mathrm{\mid }}^2{)}^{1\mathrm{/}2}\mathrm{.}(3)$

The space ${\mathrm{\ell }}^2(I)$. For a family $a=(a_i{)}_{i\in I}$ in $\mathbb{F}$ define $Q(a):={\sum }_{i\in I}\mathrm{\mid }{a}_i{\mathrm{\mid }}^2$. If $Q(a)$ is finite, set $\mathrm{\parallel }a{\mathrm{\parallel }}_2:=\sqrt{Q(a)}$, using the nonnegative real square root of Square roots exist: a unique $\sqrt{a}\ge 0$ with $(\sqrt{a}{)}^2=a$; the positives are $\{x^2:x\mathrm{\ne }0\}$; if $Q(a)=+\mathrm{\infty }$, set $\mathrm{\parallel }a{\mathrm{\parallel }}_2:=+\mathrm{\infty }$. This is a case definition, not exponentiation of an extended real. Let

${\mathrm{\ell }}^2(I,\mathbb{F}):=\{a=(a_i{)}_{i\in I}:\mathrm{\parallel }a{\mathrm{\parallel }}_2<+\mathrm{\infty }\}\mathrm{.}$

The set ${\mathrm{\ell }}^2(I,\mathbb{F})$ is a vector space over $\mathbb{F}$: it contains the zero family, is closed under scalar multiplication because $\mathrm{\parallel }\lambda a{\mathrm{\parallel }}_2=\mathrm{\mid }\lambda \mathrm{\mid }\mathrm{\parallel }a{\mathrm{\parallel }}_2$, and is closed under addition because (3) applied to finite subsums gives $\mathrm{\parallel }a+b{\mathrm{\parallel }}_2\le \mathrm{\parallel }a{\mathrm{\parallel }}_2+\mathrm{\parallel }b{\mathrm{\parallel }}_2<+\mathrm{\infty }$. The same inequality is the triangle inequality for $\mathrm{\parallel }\cdot {\mathrm{\parallel }}_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 $\mathrm{\parallel }\lambda a{\mathrm{\parallel }}_2=\mathrm{\mid }\lambda \mathrm{\mid }\mathrm{\parallel }a{\mathrm{\parallel }}_2$; thus $\mathrm{\parallel }\cdot {\mathrm{\parallel }}_2$ is a norm on ${\mathrm{\ell }}^2(I,\mathbb{F})$. Finally the pairing $⟨a,b⟩:={\sum }_{i\in I}{a}_i\overline{b_i}$ is well defined on ${\mathrm{\ell }}^2(I,\mathbb{F})\times {\mathrm{\ell }}^2(I,\mathbb{F})$, because $\mathrm{\mid }{a}_i\overline{b_i}\mathrm{\mid }=\mathrm{\mid }{a}_i\mathrm{\mid }\mathrm{\mid }{b}_i\mathrm{\mid }$ has finite nonnegative sum by (3); it is linear in the first variable, conjugate symmetric, positive definite, and satisfies $⟨a,a⟩=\mathrm{\parallel }a{\mathrm{\parallel }}_2^2$, all by the corresponding finite identities and the linearity of the sum. Consequently ${\mathrm{\ell }}^2(I,\mathbb{F})$ is an inner-product space, and $e_i\in {\mathrm{\ell }}^2(I,\mathbb{F})$ denotes the family that is $1$ at $i$ and $0$ elsewhere. Nothing here asserts that ${\mathrm{\ell }}^2(I,\mathbb{F})$ is complete; that follows later, from an orthonormal basis of a Hilbert space.

Let $(e_i{)}_{i\in I}$ be an orthonormal family in a real or complex inner-product space $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases). Then for every $x\in H$ the nonnegative family $(\mathrm{\mid }⟨x,e_i⟩{\mathrm{\mid }}^2{)}_{i\in I}$ has finite sum in the finite-subset-supremum convention (Square-summable families on an arbitrary index set and the space ${\mathrm{\ell }}^2(I)$) and

${\sum }_{i\in I}\mathrm{\mid }⟨x,e_i⟩{\mathrm{\mid }}^2\le \mathrm{\parallel }x{\mathrm{\parallel }}^2\mathrm{.}$

In particular the coefficient family $(⟨x,e_i⟩{)}_{i\in I}$ belongs to ${\mathrm{\ell }}^2(I,\mathbb{F})$, and the inequality holds with no hypothesis on the cardinality of $I$ and with no completeness of $H$.

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)).

1. If $a=(a_i{)}_{i\in I}\in {\mathrm{\ell }}^2(I,\mathbb{F})$ (Square-summable families on an arbitrary index set and the space ${\mathrm{\ell }}^2(I)$), then its support $\{i\in I:a_i\mathrm{\ne }0\}$ is at most countable (Finite, countably infinite, countable, uncountable).
2. If $(e_i{)}_{i\in I}$ is an orthonormal family in a real or complex inner-product space $H$ and $x\in H$, then the set $\{i\in I:⟨x,e_i⟩\mathrm{\ne }0\}$ of nonzero coefficients of $x$ is at most countable.

The hypothesis is not decoration. The countable-union step below selects one surjection of $\mathbb{N}$ onto each of the countable sets in a countable family, which is exactly the Axiom of Countable Choice; the threshold sets themselves and their finiteness are ZF.

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)). Let $(x_i{)}_{i\in I}$ be an orthogonal family in a real or complex Hilbert space $H$ whose square sum is finite,

$S:={\sum }_{i\in I}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2<+\mathrm{\infty }$

in the finite-subset-supremum convention (Square-summable families on an arbitrary index set and the space ${\mathrm{\ell }}^2(I)$), and for finite $F\subseteq I$ put $s_F:={\sum }_{i\in F}{x}_i$.

1. The finite-subset net $(s_F{)}_{F\in \mathrm{Fin}(I)}$ converges in $H$; its limit $s$ satisfies $\mathrm{\parallel }s{\mathrm{\parallel }}^2={\sum }_{i\in I}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2=S$.
2. In particular, if $(e_i{)}_{i\in I}$ is an orthonormal family in $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases) and $a=(a_i{)}_{i\in I}\in {\mathrm{\ell }}^2(I,\mathbb{F})$, then the finite-subset net ${\sum }_{i\in F}{a}_i{e}_i$ converges to a limit $s$ with $\mathrm{\parallel }s{\mathrm{\parallel }}^2={\sum }_{i\in I}\mathrm{\mid }{a}_i{\mathrm{\mid }}^2$, and $⟨s,e_j⟩=a_j$ for every $j\in I$.

The hypothesis is exactly ${\mathrm{A}\mathrm{C}}_{\omega }$. It is spent once, in selecting one finite tail-control set for each natural number; no enumeration of $I$ and no maximal orthonormal family is used.