Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Corollary 2.3.23Evaluation identity

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

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

LaTeX Lean

Corollary 2.1.34Commutative Banach algebra

\(\ell ^1_\nu \) is a commutative Banach algebra over \(\mathbb {R}\):

Complete normed space (Banach)
Commutative ring under \(\star \)
\(\mathbb {R}\)-algebra with compatible scalar multiplication
Submultiplicative: \(\| a \star b\| \leq \| a\| \cdot \| b\| \)
Scalar-norm compatibility: \(\| c \cdot a\| = |c| \cdot \| a\| \)
\(\| 1\| = 1\)

This is the full Mathlib NormedAlgebra + CompleteSpace structure.

LaTeX Lean

Corollary 1.2.4Mean Value Inequality

Consider an open set \(U \subset \mathbb {R}^n\). Let \(f: U \rightarrow \mathbb {R}^n\) be a \(C^1\) function. Fix a point \(x_0 \in U\) and assume \(\overline{B}_\rho (x_0) \subset U\) for some \(\rho {\gt} 0\). Then, for all \(x, y \in \overline{B}_\rho (x_0)\),

\begin{equation*} \| f(y) - f(x)\| \leq \left(\sup _{z \in \overline{B}_\rho (x_0)} \| \text{Df}(z)\| \right) \| y-x\| , \end{equation*}

where \(\| \text{Df}(\cdot )\| \) denotes the operator norm.

LaTeX Lean

Corollary 1.4.7

There exists a unique \(\tilde{x} \in \overline{B}_{3/20}(13/10)\) with \(\tilde{x}^2 = 2\).

LaTeX Lean

Definition 2.3.5Approximate 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\)

LaTeX Lean

Definition 2.1.8Cauchy product

The Cauchy product of sequences \(a, b : \mathbb {N} \rightarrow R\) is:

\begin{equation*} (a \star b)_n = \sum _{k+l=n} a_k b_l = \sum _{j=0}^{n} a_{n-j} b_j. \end{equation*}

LaTeX Lean

Definition 2.1.14Identity sequence

The identity element is the Kronecker delta:

\begin{equation*} e_n = \delta _{n,0} = \begin{cases} 1 & n = 0 \\ 0 & n \geq 1. \end{cases}\end{equation*}

LaTeX Lean

Definition 1.1.1Complete metric space

A metric space \((X, d)\) is complete if every Cauchy sequence converges in \(X\), i.e., if given any \(\varepsilon {\gt} 0\) there exists \(N(\varepsilon )\) such that \(n, m {\gt} N(\varepsilon )\) implies \(d(x_n, x_m) {\lt} \varepsilon \), then there is some \(y \in X\) with \(\lim _{n\rightarrow \infty } x_n = y\).

LaTeX Lean

Definition 2.3.6Concrete 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\).

LaTeX Lean

Definition 1.1.2Contraction mapping

Let \((X, d)\) be a metric space. A function \(T: X \rightarrow X\) is a contraction if there is a number \(\kappa \in [0, 1)\), called a contraction constant, such that

\begin{equation*} d(T(x), T(y)) \leq \kappa \cdot d(x, y) \end{equation*}

for all \(x, y \in X\).

LaTeX Lean

Definition 2.3.19Analytic 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*}

LaTeX Lean

Definition 2.3.2The 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\).

LaTeX Lean

Definition 2.2.6General radii polynomial

For constants \(Y_0, Z_0, Z_1 \geq 0\) and function \(Z_2: (0,\infty ) \rightarrow [0,\infty )\), the general radii polynomial is

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

LaTeX Lean

Definition 2.1.4Weighted \(\ell ^1\) space

Specialization of \(\ell ^p_\nu \) to \(p = 1\):

\begin{equation*} \ell ^1_\nu = \left\{ a : \mathbb {N} \rightarrow \mathbb {R} \; \middle |\; \| a\| _{1,\nu } := \sum _{n=0}^\infty |a_n| \nu ^n {\lt} \infty \right\} . \end{equation*}

LaTeX Lean

Definition 2.1.20Multiplication on \(\ell ^1_\nu \)

\(\texttt{mul}(a, b) := a \star b\) lifted to \(\ell ^1_\nu \).

LaTeX Lean

Definition 2.1.22Identity element

The identity \(e \in \ell ^1_\nu \) with \(e_0 = 1\), \(e_n = 0\) for \(n \geq 1\).

LaTeX Lean

Definition 2.1.3Weighted \(\ell ^p\) space

The weighted \(\ell ^p_\nu \) space is realized as \(\texttt{lp}\ (\texttt{ScaledReal}\ \nu )\ p\). The norm is:

\begin{equation*} \| a\| _{p,\nu } := \left(\sum _{n=0}^\infty |a_n|^p \nu ^{pn}\right)^{1/p}. \end{equation*}

LaTeX Lean

Definition 2.2.4Newton-like map for E to F

For a function \(f: E \rightarrow F\) and an approximate inverse \(A: F \rightarrow E\), the Newton-like map is

\begin{equation*} T(x) = x - A(f(x)). \end{equation*}

Note that \(T: E \rightarrow E\) even though \(f\) maps between different spaces.

LaTeX Lean

Definition 1.3.1Newton-like map

Let \(E, F\) be Banach spaces, \(f: E \rightarrow F\) a function, and \(A: F \rightarrow E\) a continuous linear map. The Newton-like map is defined by

\begin{equation*} T(x) = x - A(f(x)). \end{equation*}

LaTeX Lean

Definition 1.2.1Operator norm

Let \((X, \| \cdot \| _X)\) and \((Y, \| \cdot \| _Y)\) be normed linear spaces and let \(A: X \rightarrow Y\) be a continuous linear map. The operator norm on \(A\) is given by

\begin{equation*} \| A\| := \sup _{x \in X \setminus \{ 0\} } \frac{\| Ax\| _Y}{\| x\| _X} = \sup _{\| x\| _X = 1} \| Ax\| _Y. \end{equation*}

LaTeX Lean

Definition 2.3.16Parameter 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*}

LaTeX Lean

Definition 2.3.1Parameter 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\)).

LaTeX Lean

Definition 2.1.1Positive real numbers

The type of positive real numbers: \(\texttt{PosReal} := \{ x : \mathbb {R} \mid 0 {\lt} x\} \).

LaTeX Lean

Definition 2.3.11Radii polynomial

The radii polynomial is

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

LaTeX Lean

Definition 1.4.2Radii polynomial

Given constants \(Y_0, Z_0 \geq 0\) and a function \(Z_2: (0,\infty ) \rightarrow [0,\infty )\), the radii polynomial is defined by

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

LaTeX Lean

Definition 2.1.2Scaled real type

For \(\nu {\gt} 0\) and \(n \in \mathbb {N}\), the type \(\texttt{ScaledReal}\ \nu \ n\) is \(\mathbb {R}\) equipped with the scaled norm \(\| x\| _n := |x| \cdot \nu ^n\).

LaTeX Lean

Definition 2.2.10Simple radii polynomial

For \(Y_0 \geq 0\) and \(Z: (0,\infty ) \rightarrow [0,\infty )\), the simple radii polynomial is

\begin{equation*} p(r) := (Z(r) - 1)r + Y_0. \end{equation*}

LaTeX Lean

Definition 2.3.3Squaring map

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

LaTeX Lean

Definition 2.3.15Embedding into PowerSeries

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

LaTeX Lean

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.

LaTeX Lean

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.

LaTeX Lean

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*}

LaTeX Lean

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*}

LaTeX Lean

Definition 1.4.3Combined bound

The combined bound is defined as

\begin{equation*} Z(r) := Z_0 + Z_2(r) \cdot r. \end{equation*}

LaTeX Lean

Definition 2.2.7Combined bound (general case)

The combined bound is

\begin{equation*} Z(r) := Z_0 + Z_1 + Z_2(r) \cdot r. \end{equation*}

LaTeX Lean

Theorem 1.4.6Square root verification (Example 2.4.5)

Consider \(f(x) = x^2 - 2\). Choose initial guess \(\bar{x} = \frac{13}{10} = 1.3\), approximate inverse \(A = \frac{19}{50} = 0.38 \approx (f'(\bar{x}))^{-1} = (2\bar{x})^{-1}\), bounds \(Y_0 = \frac{3}{25} = 0.12\), \(Z_0 = \frac{3}{250} = 0.012\), \(Z_2 = \frac{19}{25} = 0.76\), and radius \(r_0 = \frac{3}{20} = 0.15\).

The radii polynomial \(p(r) = 0.76r^2 - 0.988r + 0.12\) satisfies \(p(0.15) {\lt} 0\).

Therefore, there exists a unique \(\tilde{x} \in \overline{B}_{0.15}(1.3) = [1.15, 1.45]\) with \(\tilde{x}^2 = 2\) and \(f'(\tilde{x}) = 2\tilde{x}\) invertible.

LaTeX Lean

Lemma 2.1.7Weight factorization

For \(k + l = n\): \(\nu ^k \cdot \nu ^l = \nu ^n\). This is the key property enabling submultiplicativity.

LaTeX Lean

Lemma 2.2.16Closed balls are complete

In a complete space \(E\), closed balls \(\overline{B}_r(x)\) are complete.

LaTeX Lean

Lemma 2.2.18Constructing derivative inverse

If \(A: F \rightarrow E\) is injective and \(\| I_E - A \circ B\| {\lt} 1\) for \(B: E \rightarrow F\), then \(B\) is invertible with inverse \(B^{-1} = (A \circ B)^{-1} \circ A\).

LaTeX Lean

Lemma 2.2.17Extended distance is finite

In normed spaces, extended distance is always finite: \(d_{\text{ext}}(x,y) \neq \top \).

LaTeX Lean

Lemma 2.3.24Evaluation at zero

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

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

LaTeX Lean

Lemma 2.2.2Explicit two-sided inverse

If \(\| I_E - B\| {\lt} 1\) for \(B: E \rightarrow E\), then there exists \(B^{-1}: E \rightarrow E\) such that

\begin{equation*} B \circ B^{-1} = I_E \quad \text{and} \quad B^{-1} \circ B = I_E. \end{equation*}

LaTeX Lean

Lemma 2.2.8Alternative form (general)

The general radii polynomial can be rewritten as \(p(r) = (Z(r) - 1)r + Y_0\).

LaTeX Lean

Lemma 2.2.9General polynomial negativity implies contraction

If \(Y_0 \geq 0\), \(r_0 {\gt} 0\), and \(p(r_0) {\lt} 0\) for the general radii polynomial, then \(Z(r_0) {\lt} 1\).

LaTeX Lean

Lemma 2.2.3Composition form

If \(\| I_E - B\| {\lt} 1\), then there exists \(B^{-1}\) such that

\begin{equation*} B.\text{comp}(B^{-1}) = I_E \quad \text{and} \quad B^{-1}.\text{comp}(B) = I_E. \end{equation*}

LaTeX Lean

Lemma 2.1.6Membership criterion

A sequence \(a\) belongs to \(\ell ^1_\nu \) iff \(\sum _{n=0}^\infty |a_n| \nu ^n\) converges.

LaTeX Lean

Lemma 2.1.19Closure under multiplication

If \(a, b \in \ell ^1_\nu \), then \(a \star b \in \ell ^1_\nu \).

LaTeX Lean

Lemma 2.1.5Completeness

The space \(\ell ^p_\nu \) is complete (a Banach space) for \(p \geq 1\).

LaTeX Lean

Lemma 2.2.19Ball mapping property

Given \(T: E \rightarrow E\) differentiable with: (a) \(\| T(\bar{x}) - \bar{x}\| \leq Y_0\); (b) \(\| \text{DT}(c)\| \leq Z(r_0)\) for all \(c \in \overline{B}_{r_0}(\bar{x})\); (c) \(Z(r_0) \geq 0\); (d) \(p(r_0) = (Z(r_0) - 1)r_0 + Y_0 {\lt} 0\). Then \(T: \overline{B}_{r_0}(\bar{x}) \rightarrow \overline{B}_{r_0}(\bar{x})\).

LaTeX Lean

Lemma 2.2.14General derivative bound

Suppose for all \(c \in \overline{B}_r(\bar{x})\):

\begin{equation*} \| I_E - A \circ A^\dagger \| \leq Z_0 \end{equation*}

\begin{equation*} \| A \circ (A^\dagger - \text{Df}(\bar{x}))\| \leq Z_1 \end{equation*}

\begin{equation*} \| A \circ (\text{Df}(c) - \text{Df}(\bar{x}))\| \leq Z_2(r) \cdot r \end{equation*}

Then \(\| \text{DT}(c)\| \leq Z_0 + Z_1 + Z_2(r) \cdot r = Z(r)\).

LaTeX Lean

Lemma 2.2.15Simple derivative bound

When \(A^\dagger = \text{Df}(\bar{x})\) (so \(Z_1 = 0\)), for all \(c \in \overline{B}_r(\bar{x})\): if \(\| I_E - A \circ \text{Df}(\bar{x})\| \leq Z_0\) and \(\| A \circ (\text{Df}(c) - \text{Df}(\bar{x}))\| \leq Z_2(r) \cdot r\), then \(\| \text{DT}(c)\| \leq Z_0 + Z_2(r) \cdot r\).

LaTeX Lean

Lemma 2.2.13Derivative of Newton operator

For \(T(x) = x - A(f(x))\) where \(f: E \rightarrow F\) is differentiable: \(\text{DT}(x) = I_E - A \circ \text{Df}(x)\).

LaTeX Lean

Lemma 2.2.12\(Y_0\) bound for Newton operator

If \(\| A(f(\bar{x}))\| \leq Y_0\), then for \(T(x) = x - A(f(x))\): \(\| T(\bar{x}) - \bar{x}\| \leq Y_0\).

LaTeX Lean

Lemma 2.1.23Norm of identity

\(\| e\| _{1,\nu } = 1\).

LaTeX Lean

Lemma 2.1.33Norm bound for powers

For \(a \in \ell ^1_\nu \) and \(n \in \mathbb {N}\):

\begin{equation*} \| a^n\| _{1,\nu } \leq \| a\| _{1,\nu }^n. \end{equation*}

LaTeX Lean

Lemma 2.1.31Norm of scalar multiplication

For \(c \in \mathbb {R}\) and \(a \in \ell ^1_\nu \):

\begin{equation*} \| c \cdot a\| _{1,\nu } = |c| \cdot \| a\| _{1,\nu }. \end{equation*}

LaTeX

Lemma 1.4.5Polynomial negativity implies contraction

If \(Y_0 \geq 0\), \(r_0 {\gt} 0\), and \(p(r_0) {\lt} 0\), then \(Z(r_0) {\lt} 1\).

LaTeX Lean

Lemma 1.4.4Alternative form of radii polynomial

The radii polynomial can be rewritten as

\begin{equation*} p(r) = (Z(r) - 1)r + Y_0. \end{equation*}

LaTeX Lean

Lemma 2.2.11Simple polynomial negativity implies contraction

If \(Y_0 \geq 0\), \(r_0 {\gt} 0\), and \(p(r_0) {\lt} 0\) for the simple radii polynomial, then \(Z(r_0) {\lt} 1\).

LaTeX Lean

Lemma 2.3.20Absolute convergence

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

LaTeX Lean

Proposition 1.3.2Fixed points \(\Leftrightarrow \) Zeros (Proposition 2.3.1)

Let \(E, F\) be vector spaces, \(f: E \rightarrow F\), and \(A: F \rightarrow E\) an injective linear map. Let \(T(x) = x - A(f(x))\) be the Newton-like operator. Then:

\begin{equation*} T(x) = x \quad \Leftrightarrow \quad f(x) = 0. \end{equation*}

LaTeX Lean

Proposition 2.2.5Fixed points \(\Leftrightarrow \) Zeros for E to F

Let \(f: E \rightarrow F\) and \(A: F \rightarrow E\) be injective. Then for the Newton-like operator \(T(x) = x - A(f(x))\):

\begin{equation*} T(x) = x \quad \Leftrightarrow \quad f(x) = 0. \end{equation*}

This holds even when \(E \neq F\); injectivity of \(A\) is sufficient.

LaTeX Lean

Proposition 1.2.2Properties of operator norm

Let \((X, \| \cdot \| )\) be a normed linear space and let \(A, B: X \rightarrow X\) be linear maps. Then:

(1) \(\| Ax\| \leq \| A\| \| x\| \) for all \(x \in X\)

(2) \(\| AB\| \leq \| A\| \| B\| \) (submultiplicativity)

LaTeX

Lean

ContinuousLinearMap.opNorm_comp_le
ContinuousLinearMap.le_opNorm

Theorem 2.3.25Positive 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 }\).

LaTeX Lean

Theorem 2.3.13Bounds 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\).

LaTeX Lean

Theorem 2.1.10Associativity

\((a \star b) \star c = a \star (b \star c)\).

LaTeX Lean

Theorem 2.1.11Commutativity

\(a \star b = b \star a\) (when \(R\) is commutative).

LaTeX Lean

Theorem 2.1.12Left distributivity

\(a \star (b + c) = a \star b + a \star c\).

LaTeX Lean

Theorem 2.1.16Right identity

\(a \star e = a\).

LaTeX Lean

Theorem 2.1.18Right scalar multiplication

Scalars pull out on the right: \(a \star (c \cdot b) = c \cdot (a \star b)\). Requires commutativity of the coefficient ring.

LaTeX Lean

Theorem 2.1.15Left identity

\(e \star a = a\).

LaTeX Lean

Theorem 2.1.13Right distributivity

\((a + b) \star c = a \star c + b \star c\).

LaTeX Lean

Theorem 2.1.17Left scalar multiplication

Scalars pull out on the left: \((c \cdot a) \star b = c \cdot (a \star b)\).

LaTeX Lean

Theorem 2.3.17Multiplication 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.

LaTeX Lean

Theorem 1.1.3Contraction Mapping Theorem

Let \((X, d)\) be a complete metric space. If \(T: X \rightarrow X\) is a contraction with contraction constant \(\kappa \), then there exists a unique fixed point \(\tilde{x} \in X\) of \(T\). Furthermore, \(\tilde{x}\) is globally attracting, and for any \(x \in X\),

\begin{equation*} d(T^n(x), \tilde{x}) \leq \frac{\kappa ^n}{1-\kappa } d(T(x), x). \end{equation*}

LaTeX Lean

Theorem 2.3.21Mertens’ 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*}

LaTeX Lean

Theorem 2.3.22Squaring 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*}

LaTeX Lean

Theorem 2.3.14Example 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\).

LaTeX Lean

Theorem 2.3.26Main 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\).

LaTeX Lean

Theorem 2.3.12Existence 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\).

LaTeX Lean

Theorem 2.3.4Fré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*}

LaTeX Lean

Theorem 1.4.1Fixed point theorem with radii polynomial (Theorem 2.4.1)

Consider a map \(T \in C^1(\mathbb {R}^n, \mathbb {R}^n)\) and let \(\bar{x} \in \mathbb {R}^n\). Let \(Y_0 \geq 0\) and \(Z: (0,\infty ) \rightarrow [0,\infty )\) be a non-negative function satisfying

\begin{equation*} \| T(\bar{x}) - \bar{x}\| \leq Y_0 \end{equation*}

\begin{equation*} \| \text{DT}(c)\| \leq Z(r), \quad \text{for all } c \in \overline{B}_r(\bar{x}) \text{ and all } r {\gt} 0. \end{equation*}

Define

\begin{equation*} p(r) := (Z(r) - 1)r + Y_0. \end{equation*}

If there exists \(r_0 {\gt} 0\) such that \(p(r_0) {\lt} 0\), then there exists a unique \(\tilde{x} \in \overline{B}_{r_0}(\bar{x})\) such that \(T(\tilde{x}) = \tilde{x}\).

LaTeX Lean

Theorem 2.3.18Formal 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*}

LaTeX Lean

Theorem 2.2.20General Fixed Point Theorem (Theorem 7.6.1)

Let \(T: E \rightarrow E\) be Fréchet differentiable and \(\bar{x} \in E\). Suppose:

\begin{equation*} \| T(\bar{x}) - \bar{x}\| \leq Y_0 \end{equation*}

\begin{equation*} \| \text{DT}(x)\| \leq Z(r) \quad \text{for all } x \in \overline{B}_r(\bar{x}) \end{equation*}

Define \(p(r) := (Z(r) - 1)r + Y_0\).

If there exists \(r_0 {\gt} 0\) such that \(p(r_0) {\lt} 0\), then there exists a unique \(\tilde{x} \in \overline{B}_{r_0}(\bar{x})\) such that \(T(\tilde{x}) = \tilde{x}\).

LaTeX Lean

Theorem 2.2.21General Radii Polynomial Theorem (Theorem 7.6.2)

Let \(E\) and \(F\) be Banach spaces and \(f: E \rightarrow F\) be Fréchet differentiable. Suppose \(\bar{x} \in E\), \(A^\dagger : E \rightarrow F\), and \(A: F \rightarrow E\) with \(A\) injective. Assume:

\begin{equation*} \| A(f(\bar{x}))\| \leq Y_0 \end{equation*}

\begin{equation*} \| I_E - A \circ A^\dagger \| \leq Z_0 \end{equation*}

\begin{equation*} \| A \circ [\text{Df}(\bar{x}) - A^\dagger ]\| \leq Z_1 \end{equation*}

\begin{equation*} \| A \circ [\text{Df}(c) - \text{Df}(\bar{x})]\| \leq Z_2(r) \cdot r \quad \text{for } c \in \overline{B}_r(\bar{x}) \end{equation*}

Define \(p(r) := Z_2(r)r^2 - (1 - Z_0 - Z_1)r + Y_0\).

If there exists \(r_0 {\gt} 0\) such that \(p(r_0) {\lt} 0\), then there exists a unique \(\tilde{x} \in \overline{B}_{r_0}(\bar{x})\) with \(f(\tilde{x}) = 0\).

LaTeX Lean

Theorem 2.1.30\(\mathbb {R}\)-Algebra instance

\(\ell ^1_\nu \) is an \(\mathbb {R}\)-algebra. The algebra map \(\mathbb {R} \rightarrow \ell ^1_\nu \) sends \(r\) to \(r \cdot e\) where \(e\) is the identity sequence.

LaTeX Lean

Theorem 2.1.25Commutative ring instance

\(\ell ^1_\nu \) is a commutative ring.

LaTeX Lean

Theorem 2.1.29Scalar tower property

For \(c \in \mathbb {R}\) and \(a, b \in \ell ^1_\nu \):

\begin{equation*} (c \cdot a) \star b = c \cdot (a \star b). \end{equation*}

This is the IsScalarTower instance.

LaTeX Lean

Theorem 2.1.32Normed \(\mathbb {R}\)-Algebra instance

\(\ell ^1_\nu \) is a normed \(\mathbb {R}\)-algebra, satisfying \(\| c \cdot a\| \leq |c| \cdot \| a\| \). (In fact, equality holds.)

LaTeX Lean

Theorem 2.1.26Normed ring instance

\(\ell ^1_\nu \) is a normed ring (submultiplicativity holds).

LaTeX Lean

Theorem 2.1.27Norm one class

\(\| 1\| = 1\) in \(\ell ^1_\nu \).

LaTeX Lean

Theorem 2.1.24Ring instance

\(\ell ^1_\nu \) is a ring under Cauchy product multiplication.

LaTeX Lean

Theorem 2.1.28Scalar commutes with multiplication

For \(c \in \mathbb {R}\) and \(a, b \in \ell ^1_\nu \):

\begin{equation*} c \cdot (a \star b) = a \star (c \cdot b). \end{equation*}

This is the SMulCommClass instance.

LaTeX Lean

Theorem 1.2.3Mean Value Theorem

Suppose that \(U \subset \mathbb {R}^n\) is open and that \(f: U \rightarrow \mathbb {R}^n\) is \(C^1\). Consider \(x, y \in U\) such that the line segment \((1-t)x + ty\), \(t \in [0,1]\), is contained in \(U\). Then,

\begin{equation*} f(y) - f(x) = \left(\int _0^1 \text{Df}((1-t)x + ty) \, dt\right)(y-x), \end{equation*}

where \(\text{Df}\) denotes the Jacobian of \(f\).

LaTeX

Theorem 2.2.1Neumann series invertibility

Let \(E\) be a Banach space and \(B: E \rightarrow E\) a continuous linear operator. If \(\| I_E - B\| {\lt} 1\), then \(B\) is invertible (a unit in the multiplicative sense).

LaTeX Lean

Theorem 2.1.21Submultiplicativity

\(\| a \star b\| _{1,\nu } \leq \| a\| _{1,\nu } \cdot \| b\| _{1,\nu }\).

This is axiom (4) of Definition 7.4.1, the key analytic property. The proof uses Mertens’ theorem and weight factorization \(\nu ^n = \nu ^k \cdot \nu ^l\).

LaTeX Lean

Theorem 2.2.22Simple Radii Polynomial for E to F

Given \(f: E \rightarrow F\) Fréchet differentiable and injective \(A: F \rightarrow E\) satisfying \(\| A(f(\bar{x}))\| \leq Y_0\), \(\| I_E - A \circ \text{Df}(\bar{x})\| \leq Z_0\), and \(\| A \circ [\text{Df}(c) - \text{Df}(\bar{x})]\| \leq Z_2(r) \cdot r\) for \(c \in \overline{B}_r(\bar{x})\). If \(p(r_0) = Z_2(r_0)r_0^2 - (1-Z_0)r_0 + Y_0 {\lt} 0\), then there exists unique \(\tilde{x} \in \overline{B}_{r_0}(\bar{x})\) with \(f(\tilde{x}) = 0\).

LaTeX Lean

Theorem 2.2.23Simple Radii Polynomial (Same Space)

Consider \(f: E \rightarrow E\) Fréchet differentiable, \(\bar{x} \in E\), and \(A: E \rightarrow E\) injective. Assume \(\| A(f(\bar{x}))\| \leq Y_0\), \(\| I_E - A \circ \text{Df}(\bar{x})\| \leq Z_0\), and \(\| A \circ [\text{Df}(c) - \text{Df}(\bar{x})]\| \leq Z_2(r) \cdot r\) for \(c \in \overline{B}_r(\bar{x})\). Define \(p(r) := Z_2(r)r^2 - (1-Z_0)r + Y_0\).

If \(p(r_0) {\lt} 0\), then there exists unique \(\tilde{x} \in \overline{B}_{r_0}(\bar{x})\) with \(f(\tilde{x}) = 0\) and \(\text{Df}(\tilde{x})\) invertible.

LaTeX Lean

Theorem 2.1.9Connection to PowerSeries

Let \(\texttt{toPowerSeries}(a) = \sum _n a_n X^n\). Then:

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

This bridge lets us transport all ring axioms from PowerSeries R.

LaTeX Lean