Proof of Products and Sums of Weighted Square-Summable Sequences of Real Numbers

Each result cited is universally quantified over the data in its own statement.

Squares and absolute values. For $s\in\mathbb{R}$, claim 1 of Properties of the Absolute Value in an Ordered Field gives $|s|\in\{s,-s\}$ and $0\le|s|$; in either case $|s|\,|s|=s\,s=s^{2}$, so $|s|^{2}=s^{2}$, and $0\le s^{2}$ by claim 5 of Elementary Arithmetic in an Ordered Field. By claim 4 of Properties of the Absolute Value in an Ordered Field, $|s|\,|t|=|st|$ for all $s,t\in\mathbb{R}$.

Claim 1. Let $s,t\in\mathbb{R}$. By the previous paragraph, $0\le(|s|-|t|)^{2}$, and expanding the square in the field $\mathbb{R}$,

so $2|st|\le s^{2}+t^{2}$ by claim 3 of Elementary Arithmetic in an Ordered Field. For the second bound, claim 3 of Properties of the Absolute Value in an Ordered Field gives $st\le|st|$, hence $2st\le2|st|\le s^{2}+t^{2}$ by claim 5 of Elementary Arithmetic in an Ordered Field and transitivity, and therefore

by claim 3 of Elementary Arithmetic in an Ordered Field.

Claim 2. Fix $k\in\mathbb{N}$. Since $0\le\mu_{k}$ and $0\le(a_{k}+b_{k})^{2}$, claim 5 of Elementary Arithmetic in an Ordered Field gives $0\le\mu_{k}(a_{k}+b_{k})^{2}$; the same claim applied to the inequality $(a_{k}+b_{k})^{2}\le2a_{k}^{2}+2b_{k}^{2}$ of claim 1 and the nonnegative factor $\mu_{k}$ gives

By Elementary Properties of Series of Real Numbers §linearity the series with terms $2\mu_{k}a_{k}^{2}+2\mu_{k}b_{k}^{2}$ converges with sum $2\sum_{k=1}^{\infty}\mu_{k}a_{k}^{2}+2\sum_{k=1}^{\infty}\mu_{k}b_{k}^{2}$, so Series of Nonnegative Real Numbers, Comparison, and the Geometric Series §comparison shows that $\sum_{k=1}^{\infty}\mu_{k}(a_{k}+b_{k})^{2}$ converges with the asserted bound.

For the multiples, $\mu_{k}(\lambda a_{k})^{2}=\lambda^{2}\mu_{k}a_{k}^{2}$ for every $k$ by the field axioms, so Elementary Properties of Series of Real Numbers §linearity gives convergence of $\sum_{k=1}^{\infty}\mu_{k}(\lambda a_{k})^{2}$ with sum $\lambda^{2}\sum_{k=1}^{\infty}\mu_{k}a_{k}^{2}$.

Claim 3. Fix $k\in\mathbb{N}$. Multiplying the first bound of claim 1 by the nonnegative number $\tfrac{1}{2}\mu_{k}$, using claim 5 of Elementary Arithmetic in an Ordered Field, and using $0\le\mu_{k}|a_{k}b_{k}|$,

By Elementary Properties of Series of Real Numbers §linearity the series with these majorant terms converges with sum $\tfrac{1}{2}\bigl(\sum_{k=1}^{\infty}\mu_{k}a_{k}^{2}+\sum_{k=1}^{\infty}\mu_{k}b_{k}^{2}\bigr)$, so by Series of Nonnegative Real Numbers, Comparison, and the Geometric Series §comparison the series $\sum_{k=1}^{\infty}\mu_{k}|a_{k}b_{k}|$ converges and is bounded by that sum, which is the second asserted inequality.

For the convergence of $\sum_{k=1}^{\infty}\mu_{k}a_{k}b_{k}$, the field axioms give

and the three series on the right converge, the first by claim 2; so $\sum_{k=1}^{\infty}\mu_{k}a_{k}b_{k}$ converges by Elementary Properties of Series of Real Numbers §linearity.

Finally, claim 3 of Properties of the Absolute Value in an Ordered Field gives $-|a_{k}b_{k}|\le a_{k}b_{k}\le|a_{k}b_{k}|$, and multiplying by the nonnegative $\mu_{k}$ with claim 5 of Elementary Arithmetic in an Ordered Field gives $-\mu_{k}|a_{k}b_{k}|\le\mu_{k}a_{k}b_{k}\le\mu_{k}|a_{k}b_{k}|$ for every $k$. The series with terms $-\mu_{k}|a_{k}b_{k}|$ converges with sum $-\sum_{k=1}^{\infty}\mu_{k}|a_{k}b_{k}|$ by Elementary Properties of Series of Real Numbers §linearity, so two applications of Elementary Properties of Series of Real Numbers §order give

and claim 6 of Properties of the Absolute Value in an Ordered Field turns this into the first asserted inequality.