Smooth inverse and implicit maps
Selected AN-03 programme proof; CC0 1.0. Original ownership is retained. See licence, rights, and selection history.
The scalar calculus and topology, §§12–13, finite algebra, §§10.1–10.6, and integration proofs, §§15.0–15.1 and 16, supply the stated foundational inputs.
16.4. Constructing the inverse without changing the map or norms
Let be the original real finite-dimensional normed coordinate spaces of the same dimension , with their original norms . Let be , , on the original open set, and let have the actual invertible derivative . We keep and both norms, and never replace by an identity or by a changed coordinate expression.
Choose . Continuity of the actual derivative gives such that the original closed ball is inside and
The closed ball is complete in the original norm by the existing finite-coordinate completeness proof. For , use the actual correction map
The denominator is positive for . The full segment fundamental theorem gives
for in the original closed ball. Also
for . Thus the whole original closed ball maps into itself.
Start , . All iterates remain in that ball. The entire contraction estimate is
The finite sum and its convergent geometric tail prove that the sequence is Cauchy. Completeness gives its limit in the original closed ball. Continuity gives , hence . Letting tend to infinity in IV3 retains the exact tail bound
.
At a fixed point,
.
If two fixed points existed, their distance would be at most times itself; since , they agree. These arguments prove every existence and uniqueness step of the contraction construction.
For any in the original closed ball, the same full segment formula gives
Every ordered matrix factor and the entire integral remain. The reverse triangle inequality proves the second line. Put , an original open neighborhood of . The map is injective by IV4 and surjective by the constructed interior fixed points. Thus is its actual inverse, and IV4 gives its precise Lipschitz bound . In particular both maps are continuous.
For in the ball set . Retain both finite product identities
.
The full operator-norm tail is at most . Operator completeness therefore gives both actual inverse products and
The rightmost original inverse factor has not been absorbed into a changed derivative. The uniformly convergent series also proves continuous dependence on , since every finite matrix power is continuous.
For , write , . The original differentiability remainder gives
The remainder is zero at . IV4 bounds by
;
IV5 then makes the last remainder .
Consequently , and its continuity follows from IV5 and continuity of . This proves regularity of the actual inverse before any higher smoothness is used.
16.5. Every higher inverse derivative and the implicit map
Matrix inversion is smooth on the original invertible matrices: the full cofactor inverse proved in Polynomial and contour tools Section10 is a matrix of polynomial entries divided by its actual nonzero determinant. The proved finite product, reciprocal and chain rules therefore apply at every available order. Differentiating both original inverse products gives . For every integer , iteration retains every ordered factor:
Each differentiation either adds its label to one existing derivative block or inserts a singleton block at one of the inverse factors. The sign changes precisely in the latter case. Every ordered partition of the new label set has one such predecessor, proving IV7 by induction with no commutation of matrix factors. Repeated equal directions keep all labeled multiplicities.
Starting from the proved inverse, the identity and this smooth inversion map prove by induction. Precisely, if with , then is , so the right side is ; hence is and is . This covers every finite order and all orders when .
For , set with every original direction label retained, and differentiate the exact composition by the full higher chain rule. The partition with one block is ; all other partitions keep their original derivatives. Thus the complete inverse derivative is
The full higher chain rule itself follows by the same labeled-partition induction: differentiating a block derivative adds the new label to that block, while differentiating the outer derivative creates its singleton block. This accounts for every partition once. The derivatives of the outer map are symmetric multilinear maps, so the bracket order across blocks can be read in increasing least-label order without changing a matrix product. All lower inverse derivatives, repeated-direction multiplicities and the original left inverse matrix remain in IV8.
For the actual implicit problem , where lies in its original finite-coordinate parameter space and is invertible, apply the just proved inverse construction to the unchanged augmented map . At the original point its two block matrices are
Multiplying in both orders proves the inverse, including the lower-left term. Use the original product norm and an open product contained in the constructed image neighborhood. The first component of must be exactly , because 's first component is . Its second component is therefore the unique local solution of the actual original implicit equation. It has the proved regularity and
with every derivative of evaluated at the original . All higher derivatives are IV8 applied to the entire augmented map and then its second projection; this retains its full parameter blocks and ordered inverse factors. No implicit-function theorem was assumed in constructing this map.
If the solved coordinate dimension is zero, its original domain and range are the singleton spaces and the local inverse is the identity there; the implicit augmented map is exactly the identity on its parameter component. Its empty matrix determinant is one, and no division by the zero operator norm is made. Empty open domains have no base point and make no local assertion.