Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \section{Analytic regularity of the local solution map}
2 \label{sec:regularity}
3 The deformation estimates control how far an exact root moves under a small
4 perturbation. We now show that its local dependence on the parameters is
5 analytic, and compute the derivative from the polynomial Jacobian. The
6 analytic argument takes place over a complete normed field. For integral
7 $p$-adic data, we first include the coefficients and base point in $\Qp$;
8 $\Zp$ itself is not a vector space over $\Qp$.
9 
10 Let $\mathbb K$ be a complete nontrivially normed field. Let $e,k\in\N$, and
11 write the variables as $(Y,T)\in\mathbb K^e\times\mathbb K^k$. For
12 \[
13  F\in\mathbb K[Y_1,\ldots,Y_e,T_1,\ldots,T_k]^e,
14  \qquad a=(y_0,t_0),
15 \]
16 define the matrices of evaluated formal partial derivatives
17 \begin{equation}
18  J=D_YF(a)\in M_e(\mathbb K),\qquad
19  K=D_TF(a)\in M_{e\times k}(\mathbb K).
20  \label{eq:regularity-blocks}
21 \end{equation}
22 Rows index equations and columns index variables. We first establish that
23 these formal derivatives are the derivatives of the evaluation map.
24 
Statement: Derivative of polynomial evaluation · Go to proof · Read statement and proof side by side25 \begin{lemma}[Derivative of polynomial evaluation]
26 \label{lem:actual-polynomial-derivative}
27 For $P\in\mathbb K[X_1,\ldots,X_n]$, polynomial evaluation is analytic at
28 every point. At $a\in\mathbb K^n$ its strict Fr\'echet derivative is
29 \[
30  v\longmapsto\sum_{j=1}^n (\partial_jP)(a)v_j.
31 \]
32 For a finite system, its strict derivative is the continuous linear map
33 represented by the matrix of evaluated formal partial derivatives.
34 \end{lemma}
Proof block: Derivative of polynomial evaluation · Go to statement · Read statement and proof side by side35 \begin{proof}
36 For the derivative statement, use polynomial induction on constants,
37 addition, and multiplication by a variable. Constants have zero derivative.
38 The sum rule agrees with the additivity of formal partial differentiation.
39 For $PX_j$, the product rule gives
40 \[
41  d(PX_j)_a(v)=a_j\,dP_a(v)+P(a)v_j,
42 \]
43 which agrees with the evaluated formal product rule for every coordinate.
44 The finite product rule for maps to coordinate spaces then assembles the
45 system derivative. Each matrix defines a continuous linear map because the
46 coordinate spaces are finite-dimensional over the complete field.
47 Polynomial analyticity follows from the corresponding polynomial induction
48 in Mathlib and its finite-coordinate assembly.
49 \end{proof}
50 The derivative bridge and analytic statements are
51 \lean{Komorebi.PolynomialAnalyticEvaluation.hasStrictFDerivAt_evalSystem},
52 \lean{Komorebi.PolynomialAnalyticEvaluation.analyticAt_evalSystem}, and
53 \lean{Komorebi.PolynomialAnalyticEvaluation.analyticOnNhd_evalSystem}.
54 
Statement: The augmented derivative · Go to proof · Read statement and proof side by side55 \begin{lemma}[The augmented derivative]
56 \label{lem:augmented-analytic-inverse}
57 If $J\in\operatorname{GL}_e(\mathbb K)$, the polynomial map
58 \[
59  \Phi(Y,T)=(F(Y,T),T)
60 \]
61 has invertible strict derivative at $a$, with
62 \begin{equation}
63  D\Phi(a)=\begin{pmatrix}J&K\\0&I_k\end{pmatrix},\qquad
64  D\Phi(a)^{-1}=\begin{pmatrix}J^{-1}&-J^{-1}K\\0&I_k\end{pmatrix}.
65  \label{eq:analytic-block-inverse}
66 \end{equation}
67 The local inverse supplied by this derivative is analytic near $\Phi(a)$.
68 \end{lemma}
Proof block: The augmented derivative · Go to statement · Read statement and proof side by side69 \begin{proof}
70 The lower coordinates of $\Phi$ are the parameter variables. Differentiating
71 them gives the blocks $0$ and $I_k$. Lemma~\ref{lem:actual-polynomial-derivative}
72 identifies the remaining blocks with~\eqref{eq:regularity-blocks}.
73 Multiplication of the two matrices in~\eqref{eq:analytic-block-inverse},
74 in both orders, gives the identity. The resulting linear equivalence is
75 continuous, as is its inverse. Apply the strict inverse-function theorem to
76 $\Phi$. The analytic inverse theorem applies to the same open partial
77 homeomorphism, because $\Phi$ is analytic and its derivative is that
78 continuous linear equivalence. It supplies a convergent local power-series
79 representation of this inverse.
80 \end{proof}
81 The augmented Jacobian is identified in
82 \lean{Komorebi.PolynomialJointSystem.jacobian_augmented}.
83 The continuous inverse block and its restriction are
84 \lean{Komorebi.PolynomialAnalyticBlocks.upperEquiv} and
85 \lean{Komorebi.PolynomialAnalyticBlocks.inverse_solved_zero}.
86 Analyticity of the same constructed inverse is
87 \lean{Komorebi.PolynomialAnalyticInverse.analyticAt_inverse}.
88 
Statement: Analytic local root graph · Go to proof · Read statement and proof side by side89 \begin{theorem}[Analytic local root graph]
90 \label{thm:analytic-local-graph}
91 Suppose $F(a)=0$ and $J\in\operatorname{GL}_e(\mathbb K)$. There are open
92 neighborhoods $t_0\in U\subseteq\mathbb K^k$ and
93 $y_0\in V\subseteq\mathbb K^e$, and a map
94 $\psi:\mathbb K^k\to\mathbb K^e$, such that
95 \begin{gather}
96  \psi(t_0)=y_0,\qquad \psi(U)\subseteq V,\qquad
97  \psi\text{ is analytic at every point of }U,\label{eq:analytic-psi}\\
98  F(y,t)=0\quad\Longleftrightarrow\quad y=\psi(t)
99  \qquad(t\in U,\ y\in V).\label{eq:analytic-root-graph}
100 \end{gather}
101 At the base parameter, the strict Fr\'echet derivative is
102 \begin{equation}
103  \boxed{D\psi(t_0)=-J^{-1}K.}
104  \label{eq:implicit-derivative}
105 \end{equation}
106 In particular, $\psi$ is differentiable on $U$.
107 \end{theorem}
Proof block: Analytic local root graph · Go to statement · Read statement and proof side by side108 \begin{proof}
109 Let $g$ be the analytic local inverse of $\Phi$ supplied by
110 Lemma~\ref{lem:augmented-analytic-inverse}. Since $F(a)=0$,
111 $\Phi(a)=(0,t_0)$ and $g(0,t_0)=a$. Define
112 \[
113  \psi(t)=\pi_Yg(0,t),
114 \]
115 where $\pi_Y$ projects to the solved coordinates. This gives the base value
116 and analyticity at $t_0$. The chain rule and
117 \eqref{eq:analytic-block-inverse} give
118 \[
119  D\psi(t_0)v
120  =\pi_Y\begin{pmatrix}J^{-1}&-J^{-1}K\\0&I_k\end{pmatrix}
121        \binom{0}{v}
122  =-J^{-1}Kv.
123 \]
124 
125 To obtain the root equivalence on a product neighborhood, we choose the
126 neighborhoods as follows. The source of the open partial homeomorphism defined by
127 $\Phi$ is open around $a$; its inverse is $g$. Choose open sets $V$ and $U_0$
128 containing $y_0$ and $t_0$ such that
129 $V\times U_0$ lies in that source. Restrict $U_0$ further by the preimage of
130 an open analytic inverse neighborhood under $t\mapsto(0,t)$, the open locus
131 where this same $\psi$ is analytic, and the interior of $\psi^{-1}(V)$.
132 All of these sets contain $t_0$. For the last set, use the continuity of
133 $\psi$ at $t_0$ and $\psi(t_0)=y_0\in V$. Their intersection is an open
134 neighborhood $U$ with $\psi(U)\subseteq V$.
135 
136 If $t\in U$, $y\in V$ and $F(y,t)=0$, then
137 $\Phi(y,t)=(0,t)$. The left inverse identity forces
138 $g(0,t)=(y,t)$, hence $y=\psi(t)$. Conversely, the right inverse identity
139 $\Phi(g(0,t))=(0,t)$ says both that its solved equations vanish and that its
140 parameter coordinates are exactly $t$. Thus
141 $g(0,t)=(\psi(t),t)$ and $F(\psi(t),t)=0$.
142 Analyticity at every point of $U$ implies differentiability there.
143 \end{proof}
144 This is
145 \lean{Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit}.
146 Differentiability is also included explicitly in the statement contract
147 \lean{Komorebi.PolynomialRegularityContracts.actual_padic_analytic_root_graph}.
148 
Statement: Regularity of a supplied root selection · Go to proof · Read statement and proof side by side149 \begin{theorem}[Regularity of a supplied root selection]
150 \label{thm:selection-regularity}
151 Under the hypotheses of Theorem~\ref{thm:analytic-local-graph}, let
152 $h:\mathbb K^k\to\mathbb K^e$ be continuous at $t_0$, with
153 $h(t_0)=y_0$. Suppose $F(h(t),t)=0$ for every $t$ in some neighborhood of
154 $t_0$. Then $h$ and $\psi$ agree in a neighborhood of $t_0$. Consequently
155 $h$ is analytic there as a germ and has strict derivative
156 $Dh(t_0)=-J^{-1}K$.
157 \end{theorem}
Proof block: Regularity of a supplied root selection · Go to statement · Read statement and proof side by side158 \begin{proof}
159 Continuity at $t_0$ places $h(t)$ inside $V$ for all sufficiently close
160 parameters. Intersect this neighborhood with $U$ and the neighborhood on
161 which the root equation holds. Equation~\eqref{eq:analytic-root-graph} gives
162 $h(t)=\psi(t)$ throughout the intersection. Analyticity and strict
163 differentiability at a point are unchanged by agreement on a neighborhood.
164 \end{proof}
165 The formal result is
166 \lean{Komorebi.PolynomialAnalyticSelection.continuous_selection_regularity}.
167 Its formulation derives $F(a)=0$ from the root equation near the base
168 parameter and the specified base value.
169 
Statement: Regularity throughout an open parameter set · Go to proof · Read statement and proof side by side170 \begin{corollary}[Regularity throughout an open parameter set]
171 \label{cor:selection-open-regularity}
172 Let $U\subseteq\mathbb K^k$ be open, and let $h$ be continuous on $U$.
173 Suppose that for every $t\in U$,
174 \[
175  F(h(t),t)=0,
176  \qquad J_t=D_YF(h(t),t)\in\operatorname{GL}_e(\mathbb K).
177 \]
178 Then $h$ is analytic at every point of $U$ and its strict derivative is
179 \[
180  Dh(t)=-J_t^{-1}D_TF(h(t),t)\qquad(t\in U).
181 \]
182 \end{corollary}
Proof block: Regularity throughout an open parameter set · Go to statement · Read statement and proof side by side183 \begin{proof}
184 At each $t\in U$, openness turns continuity on $U$ into continuity at $t$
185 and makes the root equation hold on a neighborhood of $t$. Apply
186 Theorem~\ref{thm:selection-regularity} at $(h(t),t)$.
187 \end{proof}
188 This is
189 \lean{Komorebi.PolynomialAnalyticSelection.continuous_selection_analyticOnNhd}.
190 The pointwise invertibility assumption is part of this corollary.
191 
Statement: Integral coefficients and centers · Go to proof · Read statement and proof side by side192 \begin{corollary}[Integral coefficients and centers]
193 \label{cor:integral-analytic-graph}
194 Let $p$ be any prime. Suppose $F\in\Zp[Y,T]^e$, $a\in\Zp^{e+k}$,
195 and $F(a)=0$. Let $\iota:\Zp\hookrightarrow\Qp$ be the inclusion.
196 If $\iota(D_YF(a))\in\operatorname{GL}_e(\Qp)$, the polynomial system
197 obtained by including the original coefficients in $\Qp$ has the analytic
198 local root graph of Theorem~\ref{thm:analytic-local-graph} at $\iota(a)$.
199 The strict derivative at the base is
200 \[
201  -\iota(D_YF(a))^{-1}\iota(D_TF(a)).
202 \]
203 The open neighborhoods and the output map are in the ambient spaces over
204 $\Qp$.
205 \end{corollary}
Proof block: Integral coefficients and centers · Go to statement · Read statement and proof side by side206 \begin{proof}
207 Coefficient inclusion commutes with evaluation and formal partial
208 differentiation. Consequently both Jacobian blocks after inclusion are the
209 entrywise inclusions of the original blocks, and the original exact root
210 remains an exact root. Apply Theorem~\ref{thm:analytic-local-graph} to the system with included
211 coefficients.
212 \end{proof}
213 This is
214 \lean{Komorebi.PolynomialRegularityIntegral.exists_analytic_integral_implicit}.
215 It requires no invertibility modulo $p$. In particular, it includes solved
216 Jacobians singular modulo $p$ but invertible over the fraction field.
217 
218 \begin{example}[The derivative sign and a nonlinear control]
219 For $F(Y,T)=Y+T$, the exact branch is $\psi(T)=-T$ and $J=K=1$.
220 The derivative is $-1$. Uniqueness of the derivative rules out $+1$ over
221 $\Qp$, including $p=2$. The nonlinear polynomial $F(Y,T)=Y+Y^2+T$
222 has $F(0,0)=0$ and $J=K=1$ there. Applying the formal theorem to this polynomial constructs an analytic
223 local root graph with derivative $-1$. Thus the example checks the existence
224 conclusion as well as the derivative formula.
225 The declarations and the deliberately rejected positive-sign statement are
226 in the regularity control and statement-contract files.
227 \end{example}
228 
229 The results cover arbitrary finite $e$ and $k$, including zero. The local
230 inverse machinery explicitly handles a zero-dimensional domain. The analytic theorem does not assign a uniform numerical radius to its
231 neighborhoods. The earlier
232 weighted lifting and joint deformation theorems retain their quantitative
233 radii and error bounds, while the present statements establish regularity
234 of the local solution germ. A direct Lean identification with each
235 historical subtype-valued chart is an additional interface task. General
236 persistence at a fraction-field singular solved block is a separate problem.

Back to source controls

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation