Square-summable orthogonal families have norm-convergent finite sums

For every finite $F\subseteq I$ Pythagoras gives $\mathrm{\parallel }{s}_F{\mathrm{\parallel }}^2={\sum }_{i\in F}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2$, and then $\mathrm{\parallel }{s}_F{\mathrm{\parallel }}^2\le S$ because a finite subsum is at most the supremum $S$.

For finite $F\subseteq G\subseteq I$, the difference $s_G-s_F={\sum }_{i\in G\setminus F}{x}_i$ is a sum of pairwise orthogonal vectors, so $\mathrm{\parallel }{s}_G-s_F{\mathrm{\parallel }}^2={\sum }_{i\in G\setminus F}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2$, a value at most ${\sum }_{i\in I\setminus F}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2$.

The net $t_F:={\sum }_{i\in F}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2$ is nondecreasing with respect to inclusion and has supremum $S$, so for every real $\epsilon >0$ there is a finite $F_0$ with $S-t_F<\epsilon$ for every finite $F\supseteq F_0$.

For each natural $n\ge 1$ the set of finite $F$ with ${\sum }_{i\in I\setminus F}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2<1\mathrm{/}n$ is nonempty by [A2], so Countable Choice selects one such finite set $F_n$ for every $n\ge 1$; replacing $F_n$ by $F_1\cup \cdots \cup F_n$ gives finite sets with $F_1\subseteq F_2\subseteq \cdots$ and ${\sum }_{i\in I\setminus F_n}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2<1\mathrm{/}n$ still, since the tail of a larger set is smaller.

For $m\ge n$ the estimate of step 1.2 gives $\mathrm{\parallel }{s}_{F_m}-s_{F_n}{\mathrm{\parallel }}^2\le {\sum }_{i\in I\setminus F_n}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2<1\mathrm{/}n$, so $(s_{F_n}{)}_{n\ge 1}$ is a Cauchy sequence: for $\epsilon >0$ choose $n$ with $1\mathrm{/}n<{\epsilon }^2$, then $\mathrm{\parallel }{s}_{F_m}-s_{F_n}\mathrm{\parallel }<\epsilon$ for all $m\ge n$ by monotonicity of squaring on nonnegative reals. Hence $(s_{F_n})$ converges to some $s\in H$ by completeness.

The limit satisfies $\mathrm{\parallel }s{\mathrm{\parallel }}^2=S$: the splitting identity for the nonnegative family gives $t_{F_n}=S-{\sum }_{i\in I\setminus F_n}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2$, and the subtracted tails are below $1\mathrm{/}n$ and hence tend to $0$, so $t_{F_n}\to S$; by step 1.1, step 2.1 and continuity of the norm, $\mathrm{\parallel }s{\mathrm{\parallel }}^2={\lim }_n\mathrm{\parallel }{s}_{F_n}{\mathrm{\parallel }}^2={\lim }_n{t}_{F_n}=S$.

The whole finite-subset net converges to $s$: given a real $\delta >0$, choose $n$ with $1\mathrm{/}n<{\delta }^2\mathrm{/}4$ and $\mathrm{\parallel }{s}_{F_n}-s\mathrm{\parallel }<\delta \mathrm{/}2$, which is possible because $(s_{F_n})$ converges to $s$; then every finite $F\supseteq F_n$ satisfies $\mathrm{\parallel }{s}_F-s_{F_n}{\mathrm{\parallel }}^2\le {\sum }_{i\in I\setminus F_n}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2<1\mathrm{/}n<{\delta }^2\mathrm{/}4$, hence $\mathrm{\parallel }{s}_F-s\mathrm{\parallel }\le \mathrm{\parallel }{s}_F-s_{F_n}\mathrm{\parallel }+\mathrm{\parallel }{s}_{F_n}-s\mathrm{\parallel }<\delta$.

For the orthonormal case let $x_i:=a_i{e}_i$; the family $(x_i)$ is orthogonal with $\mathrm{\parallel }{x}_i\mathrm{\parallel }=\mathrm{\mid }{a}_i\mathrm{\mid }$, and ${\sum }_{i\in I}\mathrm{\parallel }{x}_i{\mathrm{\parallel }}^2={\sum }_{i\in I}\mathrm{\mid }{a}_i{\mathrm{\mid }}^2<+\mathrm{\infty }$ because $a\in {\mathrm{\ell }}^2(I,\mathbb{F})$, so steps 3.2 and 3.1 give a limit $s$ of the net ${\sum }_{i\in F}{a}_i{e}_i$ with $\mathrm{\parallel }s{\mathrm{\parallel }}^2={\sum }_{i\in I}\mathrm{\mid }{a}_i{\mathrm{\mid }}^2$; and for each fixed $j\in I$, $⟨s_F,e_j⟩=a_j$ for every finite $F\ni j$, so the coefficients converge, $⟨s,e_j⟩={\lim }_F⟨s_F,e_j⟩=a_j$, by continuity of the pairing in the first variable.