11 Analytic regularity of the local solution map
On this page · Permalink · Source line 1
The deformation estimates control how far an exact root moves under a small perturbation. We now show that its local dependence on the parameters is analytic, and compute the derivative from the polynomial Jacobian. The analytic argument takes place over a complete normed field. For integral \(p\)-adic data, we first include the coefficients and base point in \({\mathbb Q_p}\); \({\mathbb Z_p}\) itself is not a vector space over \({\mathbb Q_p}\).
Let \(\mathbb K\) be a complete nontrivially normed field. Let \(e,k\in{\mathbb N}\), and write the variables as \((Y,T)\in\mathbb K^e\times\mathbb K^k\). For
define the matrices of evaluated formal partial derivatives
Rows index equations and columns index variables. We first establish that these formal derivatives are the derivatives of the evaluation map.
Lemma 11.1: Derivative of polynomial evaluation
For \(P\in\mathbb K[X_1,\ldots,X_n]\), polynomial evaluation is analytic at every point. At \(a\in\mathbb K^n\) its strict Fréchet derivative is
For a finite system, its strict derivative is the continuous linear map represented by the matrix of evaluated formal partial derivatives.
Read proof · Read statement and proof side by side · Permalink · Source line 25 · Claim record · Lean coverage · Code · Worked examples
Proof of Lemma 11.1
For the derivative statement, use polynomial induction on constants, addition, and multiplication by a variable. Constants have zero derivative. The sum rule agrees with the additivity of formal partial differentiation. For \(PX_j\), the product rule gives
which agrees with the evaluated formal product rule for every coordinate. The finite product rule for maps to coordinate spaces then assembles the system derivative. Each matrix defines a continuous linear map because the coordinate spaces are finite-dimensional over the complete field. Polynomial analyticity follows from the corresponding polynomial induction in Mathlib and its finite-coordinate assembly.
Back to statement · Read statement and proof side by side · Permalink · Source line 35 · Claim record · Lean coverage · Code · Worked examples
The derivative bridge and analytic statements are Komorebi.PolynomialAnalyticEvaluation.hasStrictFDerivAt_evalSystem, Komorebi.PolynomialAnalyticEvaluation.analyticAt_evalSystem, and Komorebi.PolynomialAnalyticEvaluation.analyticOnNhd_evalSystem.
Lemma 11.2: The augmented derivative
If \(J\in\operatorname{GL}_e(\mathbb K)\), the polynomial map
has invertible strict derivative at \(a\), with
The local inverse supplied by this derivative is analytic near \(\Phi(a)\).
Read proof · Read statement and proof side by side · Permalink · Source line 55 · Claim record · Lean coverage · Code · Worked examples
Proof of Lemma 11.2
The lower coordinates of \(\Phi\) are the parameter variables. Differentiating them gives the blocks \(0\) and \(I_k\). Lemma 11.1 identifies the remaining blocks with (11.1). Multiplication of the two matrices in (11.2), in both orders, gives the identity. The resulting linear equivalence is continuous, as is its inverse. Apply the strict inverse-function theorem to \(\Phi\). The analytic inverse theorem applies to the same open partial homeomorphism, because \(\Phi\) is analytic and its derivative is that continuous linear equivalence. It supplies a convergent local power-series representation of this inverse.
Back to statement · Read statement and proof side by side · Permalink · Source line 69 · Claim record · Lean coverage · Code · Worked examples
The augmented Jacobian is identified in Komorebi.PolynomialJointSystem.jacobian_augmented. The continuous inverse block and its restriction are Komorebi.PolynomialAnalyticBlocks.upperEquiv and Komorebi.PolynomialAnalyticBlocks.inverse_solved_zero. Analyticity of the same constructed inverse is Komorebi.PolynomialAnalyticInverse.analyticAt_inverse.
Theorem 11.3: Analytic local root graph
Suppose \(F(a)=0\) and \(J\in\operatorname{GL}_e(\mathbb K)\). There are open neighborhoods \(t_0\in U\subseteq\mathbb K^k\) and \(y_0\in V\subseteq\mathbb K^e\), and a map \(\psi:\mathbb K^k\to\mathbb K^e\), such that
At the base parameter, the strict Fréchet derivative is
In particular, \(\psi\) is differentiable on \(U\).
Read proof · Read statement and proof side by side · Permalink · Source line 89 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 11.3
Let \(g\) be the analytic local inverse of \(\Phi\) supplied by Lemma 11.2. Since \(F(a)=0\), \(\Phi(a)=(0,t_0)\) and \(g(0,t_0)=a\). Define
where \(\pi_Y\) projects to the solved coordinates. This gives the base value and analyticity at \(t_0\). The chain rule and (11.2) give
To obtain the root equivalence on a product neighborhood, we choose the neighborhoods as follows. The source of the open partial homeomorphism defined by \(\Phi\) is open around \(a\); its inverse is \(g\). Choose open sets \(V\) and \(U_0\) containing \(y_0\) and \(t_0\) such that \(V\times U_0\) lies in that source. Restrict \(U_0\) further by the preimage of an open analytic inverse neighborhood under \(t\mapsto(0,t)\), the open locus where this same \(\psi\) is analytic, and the interior of \(\psi^{-1}(V)\). All of these sets contain \(t_0\). For the last set, use the continuity of \(\psi\) at \(t_0\) and \(\psi(t_0)=y_0\in V\). Their intersection is an open neighborhood \(U\) with \(\psi(U)\subseteq V\).
If \(t\in U\), \(y\in V\) and \(F(y,t)=0\), then \(\Phi(y,t)=(0,t)\). The left inverse identity forces \(g(0,t)=(y,t)\), hence \(y=\psi(t)\). Conversely, the right inverse identity \(\Phi(g(0,t))=(0,t)\) says both that its solved equations vanish and that its parameter coordinates are exactly \(t\). Thus \(g(0,t)=(\psi(t),t)\) and \(F(\psi(t),t)=0\). Analyticity at every point of \(U\) implies differentiability there.
Back to statement · Read statement and proof side by side · Permalink · Source line 108 · Claim record · Lean coverage · Code · Worked examples
This is Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit. Differentiability is also included explicitly in the statement contract Komorebi.PolynomialRegularityContracts.actual_padic_analytic_root_graph.
Theorem 11.4: Regularity of a supplied root selection
Under the hypotheses of Theorem 11.3, let \(h:\mathbb K^k\to\mathbb K^e\) be continuous at \(t_0\), with \(h(t_0)=y_0\). Suppose \(F(h(t),t)=0\) for every \(t\) in some neighborhood of \(t_0\). Then \(h\) and \(\psi\) agree in a neighborhood of \(t_0\). Consequently \(h\) is analytic there as a germ and has strict derivative \(Dh(t_0)=-J^{-1}K\).
Read proof · Read statement and proof side by side · Permalink · Source line 149 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 11.4
Continuity at \(t_0\) places \(h(t)\) inside \(V\) for all sufficiently close parameters. Intersect this neighborhood with \(U\) and the neighborhood on which the root equation holds. Equation (11.4) gives \(h(t)=\psi(t)\) throughout the intersection. Analyticity and strict differentiability at a point are unchanged by agreement on a neighborhood.
Back to statement · Read statement and proof side by side · Permalink · Source line 158 · Claim record · Lean coverage · Code · Worked examples
The formal result is Komorebi.PolynomialAnalyticSelection.continuous_selection_regularity. Its formulation derives \(F(a)=0\) from the root equation near the base parameter and the specified base value.
Corollary 11.5: Regularity throughout an open parameter set
Let \(U\subseteq\mathbb K^k\) be open, and let \(h\) be continuous on \(U\). Suppose that for every \(t\in U\),
Then \(h\) is analytic at every point of \(U\) and its strict derivative is
Read proof · Read statement and proof side by side · Permalink · Source line 170 · Claim record · Lean coverage · Code · Worked examples
Proof of Corollary 11.5
At each \(t\in U\), openness turns continuity on \(U\) into continuity at \(t\) and makes the root equation hold on a neighborhood of \(t\). Apply Theorem 11.4 at \((h(t),t)\).
Back to statement · Read statement and proof side by side · Permalink · Source line 183 · Claim record · Lean coverage · Code · Worked examples
This is Komorebi.PolynomialAnalyticSelection.continuous_selection_analyticOnNhd. The pointwise invertibility assumption is part of this corollary.
Corollary 11.6: Integral coefficients and centers
Let \(p\) be any prime. Suppose \(F\in{\mathbb Z_p}[Y,T]^e\), \(a\in{\mathbb Z_p}^{e+k}\), and \(F(a)=0\). Let \(\iota:{\mathbb Z_p}\hookrightarrow{\mathbb Q_p}\) be the inclusion. If \(\iota(D_YF(a))\in\operatorname{GL}_e({\mathbb Q_p})\), the polynomial system obtained by including the original coefficients in \({\mathbb Q_p}\) has the analytic local root graph of Theorem 11.3 at \(\iota(a)\). The strict derivative at the base is
The open neighborhoods and the output map are in the ambient spaces over \({\mathbb Q_p}\).
Read proof · Read statement and proof side by side · Permalink · Source line 192 · Claim record · Lean coverage · Code · Worked examples
Proof of Corollary 11.6
Coefficient inclusion commutes with evaluation and formal partial differentiation. Consequently both Jacobian blocks after inclusion are the entrywise inclusions of the original blocks, and the original exact root remains an exact root. Apply Theorem 11.3 to the system with included coefficients.
Back to statement · Read statement and proof side by side · Permalink · Source line 206 · Claim record · Lean coverage · Code · Worked examples
This is Komorebi.PolynomialRegularityIntegral.exists_analytic_integral_implicit. It requires no invertibility modulo \(p\). In particular, it includes solved Jacobians singular modulo \(p\) but invertible over the fraction field.
Example 11.7: The derivative sign and a nonlinear control
For \(F(Y,T)=Y+T\), the exact branch is \(\psi(T)=-T\) and \(J=K=1\). The derivative is \(-1\). Uniqueness of the derivative rules out \(+1\) over \({\mathbb Q_p}\), including \(p=2\). The nonlinear polynomial \(F(Y,T)=Y+Y^2+T\) has \(F(0,0)=0\) and \(J=K=1\) there. Applying the formal theorem to this polynomial constructs an analytic local root graph with derivative \(-1\). Thus the example checks the existence conclusion as well as the derivative formula. The declarations and the deliberately rejected positive-sign statement are in the regularity control and statement-contract files.
The results cover arbitrary finite \(e\) and \(k\), including zero. The local inverse machinery explicitly handles a zero-dimensional domain. The analytic theorem does not assign a uniform numerical radius to its neighborhoods. The earlier weighted lifting and joint deformation theorems retain their quantitative radii and error bounds, while the present statements establish regularity of the local solution germ. A direct Lean identification with each historical subtype-valued chart is an additional interface task. General persistence at a fraction-field singular solved block is a separate problem.