2.3 Example 7.7: Square Root via Power Series

This section applies the radii polynomial method to prove existence of an analytic branch of \(\sqrt{\lambda }\) near a base point \(\lambda _0 {\gt} 0\). We work in the weighted sequence space \(\ell ^1_\nu \) (Section 2.1) and verify all bounds to establish existence of a fixed point, then interpret this fixed point as a convergent power series.

2.3.1 The Fixed-Point Problem

We seek an analytic function \(x(\lambda ) = \sum _{n=0}^\infty a_n (\lambda - \lambda _0)^n\) satisfying \(x(\lambda )^2 = \lambda \). In coefficient space, this becomes: find \(a \in \ell ^1_\nu \) such that \((a \star a)_n = c_n\) where \(c\) is the parameter sequence.

Definition 2.3.1 Parameter sequence

✓

For \(\lambda _0 \in \mathbb {R}\), the parameter sequence is

\begin{equation*} c_n = \begin{cases} \lambda _0 & n = 0 \\ 1 & n = 1 \\ 0 & n \geq 2 \end{cases}\end{equation*}

This encodes the polynomial \(\lambda _0 + z\) (i.e., \(\lambda \) when \(z = \lambda - \lambda _0\)).

Definition 2.3.2 The map \(F\)

✓

The fixed-point map \(F: \ell ^1_\nu \rightarrow \ell ^1_\nu \) is defined by

\begin{equation*} F(a)_n = (a \star a)_n - c_n. \end{equation*}

A zero of \(F\) corresponds to a power series squaring to \(\lambda _0 + z\).

Definition 2.3.3 Squaring map

✓

The squaring map \(\text{sq}: \ell ^1_\nu \rightarrow \ell ^1_\nu \) is \(\text{sq}(a) = a \star a\).

Theorem 2.3.4 Fréchet derivative of squaring

✓

The squaring map is Fréchet differentiable with derivative at \(a\):

\begin{equation*} D_a[\text{sq}](h) = 2(a \star h). \end{equation*}

Proof ▶

The key identity \((a+h)^2 - a^2 - 2(a \star h) = h^2\) follows from the CommRing instance via the ring tactic. The remainder estimate \(\| h^2\| \leq \| h\| ^2\) uses submultiplicativity, giving the little-o condition. The SMulCommClass instance ensures that \(2 \cdot (a \star h) = a \star (2 \cdot h)\).

2.3.2 Approximate Solution

Definition 2.3.5 Approximate solution structure

✓

An approximate solution of order \(N\) consists of:

Finite coefficients \(\bar{a}_0, \bar{a}_1, \ldots , \bar{a}_N \in \mathbb {R}\)
The extension \(\bar{a} \in \ell ^1_\nu \) defined by \(\bar{a}_n = 0\) for \(n {\gt} N\)

Definition 2.3.6 Concrete approximate solution

✓

For \(\lambda _0 = 1\) and \(N = 2\), the approximate solution is:

\begin{equation*} \bar{a}_0 = 1, \quad \bar{a}_1 = \frac{1}{2}, \quad \bar{a}_2 = -\frac{1}{8}. \end{equation*}

These are the first three Taylor coefficients of \(\sqrt{1 + z}\) at \(z = 0\).

2.3.3 Bound Definitions

Definition 2.3.7 \(Y_0\) bound

✓

The \(Y_0\) bound measures the initial defect:

\begin{equation*} Y_0 = \| A \cdot F(\bar{a})\| _{\ell ^1_\nu } \end{equation*}

where \(A\) is the approximate inverse. For diagonal \(A\) with entries \(A_{nn} = 1/(2\bar{a}_0)\):

\begin{equation*} Y_0 = \sum _{n=0}^N |A_{nn} \cdot F(\bar{a})_n| \nu ^n + Y_0^{\text{tail}} \end{equation*}

where \(Y_0^{\text{tail}}\) accounts for the tail contribution.

Definition 2.3.8 \(Z_0\) bound

✓

The \(Z_0\) bound measures deviation from identity:

\begin{equation*} Z_0 = \| I - A \circ D_{\bar{a}}F\| . \end{equation*}

Since \(D_{\bar{a}}F(h) = 2(\bar{a} \star h)\) and \(A\) is diagonal with \(A_{nn} = 1/(2\bar{a}_0)\):

\begin{equation*} Z_0 = \sup _{n \geq 0} \left|1 - \frac{2(\bar{a} \star e_n)_n}{2\bar{a}_0}\right| \cdot \nu ^n \end{equation*}

where \(e_n\) is the \(n\)-th standard basis sequence.

Definition 2.3.9 \(Z_1\) bound

✓

The \(Z_1\) bound accounts for nonlinearity:

\begin{equation*} Z_1 = \frac{1}{|\bar{a}_0|} \sum _{k=1}^N |\bar{a}_k| \nu ^k. \end{equation*}

Definition 2.3.10 \(Z_2\) bound

✓

The \(Z_2\) bound captures derivative variation:

\begin{equation*} Z_2 = 2 \cdot \max \left(\| A\| , \frac{1}{2|\bar{a}_0|}\right). \end{equation*}

2.3.4 Radii Polynomial

Definition 2.3.11 Radii polynomial

✓

The radii polynomial is

\begin{equation*} p(r) = Z_2 r^2 - (1 - Z_0 - Z_1) r + Y_0. \end{equation*}

Theorem 2.3.12 Existence condition

✓

If there exists \(r_0 {\gt} 0\) such that \(p(r_0) {\lt} 0\), then there exists a unique \(\tilde{a} \in \ell ^1_\nu \) with \(\| \tilde{a} - \bar{a}\| \leq r_0\) satisfying \(F(\tilde{a}) = 0\).

2.3.5 Verification

Theorem 2.3.13 Bounds verification

✓

For \(\lambda _0 = 1/3\), \(\nu = 1/4\), \(N = 2\), the bounds satisfy:

\(Y_0 {\lt} 0.001\)
\(Z_0 {\lt} 0.5\)
\(Z_1 {\lt} 0.3\)
\(Z_2 {\lt} 4\)

These imply \(p(r_0) {\lt} 0\) for some \(r_0 {\gt} 0\).

Theorem 2.3.14 Example 7.7 existence

✓

For \(\lambda _0 = 1/3\) and \(\nu = 1/4\), there exists a unique \(\tilde{a} \in \ell ^1_\nu \) near \(\bar{a}\) satisfying \(\tilde{a} \star \tilde{a} = c\).

2.3.6 Power Series Interpretation

Formal Power Series Connection

Definition 2.3.15 Embedding into PowerSeries

✓

The embedding \(\ell ^1_\nu \hookrightarrow \texttt{PowerSeries}\ \mathbb {R}\) sends \(a \mapsto \sum _{n=0}^\infty a_n X^n\).

Definition 2.3.16 Parameter power series

✓

For \(\lambda _0 \in \mathbb {R}\), the parameter element \(c \in \ell ^1_\nu \) represents \(\lambda _0 + z\):

\begin{equation*} c = (\lambda _0, 1, 0, 0, \ldots ) \in \ell ^1_\nu . \end{equation*}

Theorem 2.3.17 Multiplication equals Cauchy product

✓

For \(a, b \in \ell ^1_\nu \):

\begin{equation*} \texttt{coeff}_n(\texttt{toPowerSeries}(a) \cdot \texttt{toPowerSeries}(b)) = (a \star b)_n. \end{equation*}

This is essentially definitional: multiplication in \(\texttt{PowerSeries}\ \mathbb {R}\) is the Cauchy product.

Theorem 2.3.18 Formal fixed-point equation

✓

If \(F(\tilde{a}) = 0\) (i.e., \((\tilde{a} \star \tilde{a})_n = c_n\) for all \(n\)), then at the formal level:

\begin{equation*} \texttt{toPowerSeries}(\tilde{a})^2 = \texttt{paramPowerSeries}(\lambda _0). \end{equation*}

Analytic Evaluation

Definition 2.3.19 Analytic evaluation

✓

For \(a \in \ell ^1_\nu \) and \(z \in \mathbb {R}\), the evaluation is

\begin{equation*} \texttt{eval}(a, z) := \sum _{n=0}^\infty a_n z^n. \end{equation*}

Lemma 2.3.20 Absolute convergence

✓

If \(a \in \ell ^1_\nu \) and \(|z| \leq \nu \), then \(\sum _{n=0}^\infty a_n z^n\) converges absolutely.

Proof ▶

For \(|z| \leq \nu \): \(\sum _{n=0}^\infty |a_n z^n| \leq \sum _{n=0}^\infty |a_n| \nu ^n = \| a\| _{\ell ^1_\nu } {\lt} \infty \).

Theorem 2.3.21 Mertens’ theorem: evaluation commutes with multiplication

✓

For \(a, b \in \ell ^1_\nu \) and \(|z| \leq \nu \):

\begin{equation*} \texttt{eval}(a, z) \cdot \texttt{eval}(b, z) = \sum _{n=0}^\infty (a \star b)_n z^n. \end{equation*}

Proof ▶

By absolute convergence, apply Mertens’ theorem: the product of absolutely convergent series equals the series of Cauchy products.

Theorem 2.3.22 Squaring identity

✓

If \(\tilde{a} \in \ell ^1_\nu \) satisfies \(F(\tilde{a}) = 0\), then for \(|z| \leq \nu \):

\begin{equation*} \texttt{eval}(\tilde{a}, z)^2 = \lambda _0 + z. \end{equation*}

Proof ▶

By Theorem 2.3.21: \(\texttt{eval}(\tilde{a}, z)^2 = \sum _{n=0}^\infty (\tilde{a} \star \tilde{a})_n z^n = \sum _{n=0}^\infty c_n z^n = \lambda _0 + z\).

Corollary 2.3.23 Evaluation identity

✓

For \(|\lambda - \lambda _0| \leq \nu \):

\begin{equation*} \texttt{eval}(\tilde{a}, \lambda - \lambda _0)^2 = \lambda . \end{equation*}

2.3.7 Branch Selection

The equation \(y^2 = \lambda \) has two solutions: \(\pm \sqrt{\lambda }\). We show that the power series selects the positive branch.

Lemma 2.3.24 Evaluation at zero

✓

For any \(a \in \ell ^1_\nu \):

\begin{equation*} \texttt{eval}(a, 0) = a_0. \end{equation*}

Theorem 2.3.25 Positive branch identification

✓

Suppose:

\(\lambda _0 {\gt} 0\)
\(\lambda {\gt} 0\)
\(|\lambda - \lambda _0| \leq \nu \)
\(\tilde{a}_0 {\gt} 0\)

Then \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0) = \sqrt{\lambda }\).

Proof ▶

Step 1: Evaluate at \(z = 0\): \(\texttt{eval}(\tilde{a}, 0) = \tilde{a}_0\).

Step 2: From \(\texttt{eval}(\tilde{a}, 0)^2 = \lambda _0\) and \(\tilde{a}_0 {\gt} 0\): \(\tilde{a}_0 = \sqrt{\lambda _0} {\gt} 0\).

Step 3: Since \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0)^2 = \lambda {\gt} 0\), we have \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0) \neq 0\).

Step 4 (Positivity by IVT): Suppose for contradiction that \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0) {\lt} 0\). Since \(\texttt{eval}(\tilde{a}, 0) {\gt} 0\) and \(z \mapsto \texttt{eval}(\tilde{a}, z)\) is continuous (uniform convergence of power series), by the Intermediate Value Theorem there exists \(c\) between \(0\) and \(\lambda - \lambda _0\) with \(\texttt{eval}(\tilde{a}, c) = 0\).

But \(\texttt{eval}(\tilde{a}, c)^2 = \lambda _0 + c\), so \(0 = \lambda _0 + c\), giving \(c = -\lambda _0 {\lt} 0\).

Case 1: If \(\lambda \geq \lambda _0\), then \(c \in [0, \lambda - \lambda _0]\) requires \(c \geq 0\), contradicting \(c = -\lambda _0 {\lt} 0\).

Case 2: If \(\lambda {\lt} \lambda _0\), then \(c \in [\lambda - \lambda _0, 0]\) requires \(c \geq \lambda - \lambda _0\), i.e., \(-\lambda _0 \geq \lambda - \lambda _0\), so \(\lambda \leq 0\), contradicting \(\lambda {\gt} 0\).

Therefore \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0) {\gt} 0\).

Step 5: Since \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0) {\gt} 0\) and \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0)^2 = \lambda \), we have \(\texttt{eval}(\tilde{a}, \lambda - \lambda _0) = \sqrt{\lambda }\).

2.3.8 Summary

Theorem 2.3.26 Main result for Example 7.7

For \(\lambda _0 = 1/3\), \(\nu = 1/4\), and \(N = 2\):

(Existence) There exists a unique \(\tilde{a} \in \ell ^1_\nu \) with \(\| \tilde{a} - \bar{a}\| _{\ell ^1_\nu } \leq r_0\) satisfying \(F(\tilde{a}) = \tilde{a} \star \tilde{a} - c = 0\).
(Analytic interpretation) The power series \(\tilde{x}(z) = \sum _{n=0}^\infty \tilde{a}_n z^n\) converges for \(|z| \leq \nu \) and satisfies \(\tilde{x}(\lambda - \lambda _0) = \sqrt{\lambda }\) for \(\lambda \in [\lambda _0 - \nu , \lambda _0 + \nu ]\) with \(\lambda {\gt} 0\).

Proof ▶

Part (1) follows from Theorem 2.3.14 via the radii polynomial method. Part (2) follows from Theorem 2.3.25: the fixed-point equation \(\tilde{a} \star \tilde{a} = c\) implies \(\tilde{x}(z)^2 = \lambda _0 + z\), and the branch selection via continuity and \(\tilde{a}_0 {\gt} 0\) gives the positive square root.