Uniform partial-sum criterion for a Schauder basis (source code)

= Uniform partial-sum criterion for a Schauder basis
{title2=$\sup_n\|P_n\|<\infty\quad\Longleftrightarrow\quad x=\sum_n f_n(x)x_n$}

For a countable <minimal total family in a normed space> in a <Banach space>, let $(x_n,f_n)$ be its unique <biorthogonal system> and let $P_nx=\sum_{j\leq n}f_j(x)x_j$. Uniform boundedness of these projections implies $P_nx\to x$ for every $x$: approximate $x$ by a finite linear combination $y$, eventually fixed by $P_n$, and bound the error by $(1+\sup_n\|P_n\|)\|x-y\|$. Conversely, if every <vector> has a norm-convergent expansion in this family, applying each continuous $f_j$ shows that its coefficients must be $f_j(x)$. Thus $P_nx\to x$, so the projections are pointwise bounded. The <Uniform boundedness principle> gives their uniform operator-norm bound. This proves the criterion and uniqueness of all expansions.