02.05.04 · analysis / multivariable-differentiation

Implicit and inverse function theorems

shipped3 tiersLean: partial

Anchor (Master): Apostol *Calculus* Vol. 2 Ch. 13 (originator pedagogical presentation); Spivak *Calculus on Manifolds* Ch. 2; Dieudonné *Foundations of Modern Analysis* Ch. X §10.2 (Banach-space form); Cauchy 1831 *Sur la mécanique céleste et sur un nouveau calcul* (analytic implicit-function tradition); Goursat 1903 *Sur la théorie des fonctions implicites* (Bulletin de la Société Mathématique de France 31) — originator of the modern $C^1$-and-Banach formulation; Dini 1877 *Lezioni di analisi infinitesimale* (originator of the modern implicit-function theorem on $\mathbb{R}^n$); Nash 1956 *The imbedding problem for Riemannian manifolds* (Annals of Mathematics 63); Moser 1966 *A rapidly convergent iteration method and non-linear differential equations* (Annali Scuola Norm. Sup. Pisa 20)

Intuition [Beginner]

Two questions sit at the heart of multi-variable calculus, and they have the same answer. First, when does a smooth map have a smooth inverse — at least near a given point? Second, when does an equation like $g (x, y) = 0$ pin one of its variables down as a function of the other? Both questions are local: they ask what happens in a small neighbourhood of a chosen point, not across the whole space.

The first answer is the inverse function theorem. Zoom in close enough on a smooth map at a point, and the map looks like its derivative, which is a linear map. If that linear map is invertible — that is, if its determinant is nonzero — then the smooth map is invertible too in some small neighbourhood. The smooth inverse exists and is itself smooth.

The second answer is the implicit function theorem. An equation $g (x, y) = 0$ with $g$ smooth carves out a curve or surface in the plane or space. Near a point where the rate of change of $g$ with respect to $y$ is nonzero, you can solve for $y$ as a smooth function $h (x)$ of $x$ — the level set of $g$ looks locally like a graph.

The two answers are the same. The implicit theorem is the inverse theorem in disguise. Both rest on a single linear-algebra check: a derivative, somewhere in the picture, is invertible.

Visual [Beginner]

Two panels side by side. The left panel shows a smooth map drawn as a deformed grid superimposed on a coordinate grid: tiny squares near a chosen point $a$ have been stretched, rotated, and sheared but not collapsed. An arrow above the left panel says "zoom in" and a dashed inset shows the squares becoming a parallelogram tiling — the local picture is a linear map, the derivative $D f (a)$ . Because the parallelograms have nonzero area, the local map is invertible, and the smooth map has a smooth local inverse.

The right panel shows the unit circle and a chosen point on it. A short horizontal interval beneath the point picks out a tiny range of $x$ values; the piece of the circle directly above that interval is a function $y = h (x)$ . The implicit theorem says: where the rate of change of $g$ with respect to $y$ is nonzero, that local graph exists and is smooth.

Worked example [Beginner]

Take the smooth map $f (x, y) = (x^{2} - y^{2}, 2 x y)$ at the point $a = (1, 0)$ . The output is $f (1, 0) = (1, 0)$ . The derivative is a $2 \times 2$ matrix of partial derivatives. The four entries are $2 x = 2$ , $- 2 y = 0$ , $2 y = 0$ , $2 x = 2$ at $(1, 0)$ , so the derivative matrix is the diagonal matrix with entries $2$ and $2$ . Its determinant is $4$ , which is nonzero.

The inverse function theorem then says: a small neighbourhood of $(1, 0)$ in the input plane maps one-to-one onto a small neighbourhood of $(1, 0)$ in the output plane, and the map has a smooth local inverse. (Globally, $f$ is the squaring map on the complex plane, which is 2-to-1; the local inverse only exists in a small neighbourhood.)

Now an implicit example. Take $g (x, y) = x^{2} + y^{2} - 1$ , whose zero set is the unit circle. Pick the point $a = (1/ 2, 1/ 2)$ on the circle. The rate of change of $g$ with respect to $y$ , written $g_{y}$ , equals $2 y$ , so at this point $g_{y} = 2$ , which is nonzero. The implicit function theorem says: near this point, the equation $g (x, y) = 0$ defines $y$ as a smooth function $y = h (x)$ of $x$ . In fact $h (x) = 1 - x^{2}$ for $x$ near $1/ 2$ , the upper half of the circle.

What this tells us: the single condition "some derivative is nonzero / invertible" controls both local invertibility of a map and the local solvability of an equation. The same check answers both questions.

Check your understanding [Beginner]

Exercise (easy, multiple choice).

The inverse function theorem guarantees a smooth local inverse for a smooth map $f$ at a point $a$ when:

A. $f$ is one-to-one on its whole domain. B. The determinant of the derivative matrix of $f$ at $a$ is nonzero. C. The output point $f (a)$ is the origin. D. The derivative of $f$ at $a$ equals the identity.

Hint

The inverse function theorem's hypothesis is a check on the derivative at one point, not on the global behaviour of the map.

Answer

B. The hypothesis is that the derivative matrix $D f (a)$ is invertible, equivalently, that its determinant is nonzero. The conclusion is then a smooth local inverse on a small neighbourhood of $a$ . Global one-to-oneness is neither required nor implied: the map $f (x, y) = (x^{2} - y^{2}, 2 x y)$ has invertible derivative at $(1, 0)$ and a local inverse near that point, but is two-to-one across the whole plane.

Formal definition [Intermediate+]

Throughout this section $U$ , $V$ , and $W$ denote open subsets of finite-dimensional Euclidean spaces. A map $f : U \to R^{n}$ is $C^{k}$ for $k \geq 1$ when all partial derivatives of $f$ of orders $\leq k$ exist and are continuous on $U$ .

Inverse function theorem. Let $U \subseteq R^{n}$ be open and let $f : U \to R^{n}$ be $C^{k}$ with $k \geq 1$ . If $a \in U$ and the derivative $D f (a) : R^{n} \to R^{n}$ is invertible as a linear map, then there exist open neighbourhoods $V \subseteq U$ of $a$ and $W \subseteq R^{n}$ of $f (a)$ such that the restriction $f ∣_{V} : V \to W$ is a $C^{k}$ bijection with $C^{k}$ inverse $f^{- 1} : W \to V$ . The derivative of the inverse satisfies $D (f^{- 1}) (f (a)) = (D f (a))^{- 1}$ .

The notation $J_{f} (a)$ for the Jacobian matrix continues from 02.05.03; invertibility of $D f (a)$ is equivalent to $det J_{f} (a) \neq = 0$ . Following Apostol ^{[Apostol Ch. 13 §13.4–13.7]}.

Implicit function theorem. Let $U \subseteq R^{n + m}$ be open and let $g : U \to R^{m}$ be $C^{k}$ with $k \geq 1$ . Suppose $(a, b) \in U$ with $a \in R^{n}$ , $b \in R^{m}$ , and $g (a, b) = 0$ . Write the derivative as the block matrix $D g (a, b) = (D_{1} g (a, b) ∣ D_{2} g (a, b))$ , where $D_{1} g (a, b) \in R^{m \times n}$ is the Jacobian of $g$ in the first $n$ variables and $D_{2} g (a, b) \in R^{m \times m}$ is the Jacobian in the last $m$ variables. If $D_{2} g (a, b)$ is invertible, then there exist open neighbourhoods $V \subseteq R^{n}$ of $a$ and a $C^{k}$ map $h : V \to R^{m}$ with $h (a) = b$ and $g (x, h (x)) = 0$ for all $x \in V$ . The derivative of $h$ at $a$ satisfies $$ Dh(a) = -D_2 g(a, b)^{-1} \cdot D_1 g(a, b). $$

The local solution $h$ is the unique $C^{k}$ map satisfying the level-set equation on a sufficiently small neighbourhood of $a$ . Following Apostol ^{[Apostol Ch. 13 §13.4–13.7]} and Spivak ^{[Spivak Ch. 2 Theorem 2-12]}.

Counterexamples to common slips

$C^{0}$ continuity is not enough. A continuous map with no differentiability assumption admits no invertibility test on a derivative — the hypothesis $k \geq 1$ is essential.
Pointwise invertibility, not constancy of $det D f$ . The hypothesis $det D f (a) \neq = 0$ is a check at the single point $a$ . The theorem produces a neighbourhood on which the inverse exists; the determinant stays nonzero there by continuity, but the theorem does not assume invertibility on the whole domain.
Local, not global. The map $f (x, y) = (x^{2} - y^{2}, 2 x y)$ has invertible derivative at every nonzero point yet is 2-to-1 across the plane. The inverse theorem produces a local inverse near each nonzero point, not a global one.
The implicit hypothesis is on $D_{2} g$ , not on $D_{1} g$ . To solve $g (x, y) = 0$ for the last block of variables in terms of the first, the invertibility test is on the partial Jacobian in the last block. The first block can have any rank.
Wrong partial Jacobian, wrong conclusion. At $(1, 0)$ on the unit circle $g (x, y) = x^{2} + y^{2} - 1 = 0$ , the partial $g_{y} = 2 y$ vanishes. The implicit theorem does not apply in that orientation; the circle is not a graph $y = h (x)$ near $(1, 0)$ , but it is a graph $x = k (y)$ since $g_{x} = 2 \neq = 0$ .

Key theorem with proof [Intermediate+]

Theorem (inverse implies implicit). Let $U \subseteq R^{n + m}$ be open and let $g : U \to R^{m}$ be $C^{k}$ with $k \geq 1$ , $g (a, b) = 0$ at $(a, b) \in U$ . If $D_{2} g (a, b)$ is invertible, then the implicit function theorem conclusion holds: there exist a neighbourhood $V$ of $a$ in $R^{n}$ and a $C^{k}$ map $h : V \to R^{m}$ with $h (a) = b$ and $g (x, h (x)) = 0$ for all $x \in V$ , and $D h (a) = - D_{2} g (a, b)^{- 1} D_{1} g (a, b)$ .

Proof. Define the auxiliary map $F : U \to R^{n + m}$ by $$ F(x, y) = (x, g(x, y)), $$ sending the input pair $(x, y)$ to the pair $(x, g (x, y))$ . The map $F$ is $C^{k}$ because $g$ is and the first component is the projection. Compute the derivative $D F (a, b)$ as a block matrix in the $R^{n + m} \to R^{n + m}$ form. The first $n$ rows come from the first component $x \mapsto x$ : the rate of change of $x$ with respect to $x$ is the identity block $I_{n}$ of shape $n \times n$ , and the rate of change of $x$ with respect to $y$ is the zero block of shape $n \times m$ . The last $m$ rows come from the second component $g (x, y)$ : the rate of change of $g$ with respect to $x$ is $D_{1} g (a, b)$ of shape $m \times n$ , and the rate of change of $g$ with respect to $y$ is $D_{2} g (a, b)$ of shape $m \times m$ . The block-matrix form is $$ DF(a, b) = \begin{pmatrix} I_n & 0 \ D_1 g(a, b) & D_2 g(a, b) \end{pmatrix}. $$ This is a block lower-triangular matrix; its determinant equals the product of the determinants of its diagonal blocks, $det I_{n} \cdot det D_{2} g (a, b) = det D_{2} g (a, b)$ . By hypothesis $D_{2} g (a, b)$ is invertible, so $det D F (a, b) \neq = 0$ , and $D F (a, b)$ is invertible as a linear map on $R^{n + m}$ .

Apply the inverse function theorem to $F$ at $(a, b)$ . There exist open neighbourhoods $\tilde{V}$ of $(a, b)$ in $U$ and $\tilde{W}$ of $F (a, b) = (a, 0)$ in $R^{n + m}$ such that $F : \tilde{V} \to \tilde{W}$ is a $C^{k}$ bijection with $C^{k}$ inverse $G : \tilde{W} \to \tilde{V}$ . By the form of $F$ , the first $n$ components of $F (x, y)$ are just $x$ , so the inverse $G$ preserves the first $n$ components: $G (x, z) = (x, G_{2} (x, z))$ for some $C^{k}$ map $G_{2} : \tilde{W} \to R^{m}$ .

Define $h : V \to R^{m}$ on a neighbourhood $V$ of $a$ by $$ h(x) = G_2(x, 0), $$ where $V = {x \in R^{n} : (x, 0) \in \tilde{W}}$ is open since $\tilde{W}$ is open and the map $x \mapsto (x, 0)$ is continuous. The map $h$ is $C^{k}$ as the composition of $C^{k}$ maps. Check $h (a) = G_{2} (a, 0)$ . The inverse identity $G (F (a, b)) = (a, b)$ becomes $G (a, 0) = (a, b)$ , hence $G_{2} (a, 0) = b$ , hence $h (a) = b$ .

Check $g (x, h (x)) = 0$ for $x \in V$ . The defining identity $F (G (x, 0)) = (x, 0)$ unpacks to $F (x, h (x)) = (x, 0)$ , which by definition of $F$ is $(x, g (x, h (x))) = (x, 0)$ , hence $g (x, h (x)) = 0$ .

The derivative formula. Differentiate the identity $g (x, h (x)) = 0$ in $x$ at $x = a$ using the chain rule 02.05.03: the derivative of $g (x, h (x))$ in $x$ is the sum of the partial derivatives in the two argument blocks, multiplied by the derivatives of those arguments. The first block argument is $x$ , with derivative $I_{n}$ , so its contribution is $D_{1} g (a, b) \cdot I_{n} = D_{1} g (a, b)$ . The second block argument is $h (x)$ , with derivative $D h (a)$ , so its contribution is $D_{2} g (a, b) \cdot D h (a)$ . The sum is $0$ : $$ D_1 g(a, b) + D_2 g(a, b) \cdot Dh(a) = 0. $$ Solve for $D h (a)$ by left-multiplying by $D_{2} g (a, b)^{- 1}$ : $$ Dh(a) = -D_2 g(a, b)^{-1} \cdot D_1 g(a, b). \qquad \square $$

The proof reduces the implicit function theorem to the inverse function theorem through the lifting trick $F (x, y) = (x, g (x, y))$ . The remaining content is the inverse function theorem itself, proved via the Banach contraction principle.

Theorem (inverse function theorem; Apostol Ch. 13). Let $U \subseteq R^{n}$ be open, $f : U \to R^{n}$ a $C^{1}$ map, and $a \in U$ with $D f (a)$ invertible. Then there are open neighbourhoods $V ∋ a$ , $W ∋ f (a)$ with $f ∣_{V} : V \to W$ a $C^{1}$ bijection whose inverse is $C^{1}$ on $W$ .

Proof sketch (contraction principle). Reduce to the case $a = 0$ , $f (a) = 0$ , $D f (0) = I_{n}$ by composing with two affine maps; the general case follows from this normalised case by undoing the composition. With this reduction, define for each target value $y$ in a small neighbourhood of $0$ the auxiliary map $$ T_y : x \mapsto x - (f(x) - y) = y + x - f(x). $$ A fixed point of $T_{y}$ — a point $x$ with $T_{y} (x) = x$ — is a preimage of $y$ under $f$ . The map $T_{y}$ has derivative $I_{n} - D f (x)$ at $x$ . Since $D f (0) = I_{n}$ and $D f$ is continuous, $∥ I_{n} - D f (x) ∥_{op} \leq 1/2$ on a small closed ball $\overline{B_{r} (0)}$ . The mean-value inequality gives $∥ T_{y} (x_{1}) - T_{y} (x_{2}) ∥ \leq (1/2) ∥ x_{1} - x_{2} ∥$ for $x_{1}, x_{2} \in \overline{B_{r} (0)}$ , so $T_{y}$ is a contraction with constant $1/2$ . For $y$ small enough, $T_{y}$ maps $\overline{B_{r} (0)}$ into itself. The Banach contraction principle gives a unique fixed point $x (y) \in \overline{B_{r} (0)}$ with $f (x (y)) = y$ , and this fixed point depends continuously on $y$ . The construction defines the local inverse $f^{- 1} (y) = x (y)$ on a small neighbourhood of $0$ .

Smoothness of the inverse comes from the chain rule 02.05.03: differentiating the identity $f (f^{- 1} (y)) = y$ in $y$ at $y = 0$ gives $D f (0) \cdot D (f^{- 1}) (0) = I_{n}$ , hence $D (f^{- 1}) (0) = D f (0)^{- 1}$ . The same computation at any nearby $y$ with $x = f^{- 1} (y)$ gives $D (f^{- 1}) (y) = D f (x)^{- 1}$ . The right-hand side is continuous in $y$ because $D f$ is continuous and the matrix inverse is a continuous operation on the open set of invertible matrices. Hence $f^{- 1}$ is $C^{1}$ . Iterating the chain-rule argument shows $f^{- 1}$ is $C^{k}$ when $f$ is $C^{k}$ . $□$

The full Apostol proof carries the contraction estimate at the level of operator norms with explicit bounds. The structure is invariant: a single contraction-mapping argument plus chain rule for smoothness.

Bridge. Four threads run from the inverse and implicit function theorems into the rest of the curriculum, and each one identifies the linear-algebra check $det D f \neq = 0$ as the foundational mechanism. First, both theorems are local: they trade the global question of invertibility for a pointwise derivative check. The trade is exact — the proof shows that invertibility of the linear approximation is the only ingredient needed, because the contraction-mapping argument absorbs the higher-order error terms. Second, the two theorems are equivalent: the implicit theorem follows from the inverse theorem by the auxiliary map $F (x, y) = (x, g (x, y))$ , and the inverse theorem follows from the implicit theorem applied to $g (x, y) = f (x) - y$ . The single content is local linearisation; the two statements are two faces of it. Third, the theorems unlock the manifold structure on level sets: when $g : R^{n + m} \to R^{m}$ has surjective derivative at every point of the zero set ${g = 0}$ , the implicit theorem makes that zero set locally a graph at every point — the regular-level-set theorem, foundational for 03.02.01 smooth manifolds. Fourth, the contraction-mapping engine generalises far beyond Euclidean space: the same argument runs on Banach spaces (the Banach-space inverse theorem) and, with a loss-of-derivatives correction, on tame Fréchet spaces (the Nash-Moser hard implicit theorem, used in KAM theory and the Riemannian embedding problem). The linear-algebra invertibility check is the load-bearing piece in every case.

Exercises [Intermediate+]

Exercise 2 (easy, symbolic).

Let $g (x, y) = x^{3} + y^{3} - 3 x y$ . Determine whether the implicit function theorem can be used to solve $g (x, y) = 0$ for $y$ as a function of $x$ near the point $(0, 0)$ . If yes, compute $h^{'} (0)$ .

Hint

Compute $g_{y}$ at $(0, 0)$ . If it is nonzero, the theorem applies and the derivative formula is $h^{'} (a) = - g_{x} (a, b) / g_{y} (a, b)$ .

Answer

$g_{y} (x, y) = 3 y^{2} - 3 x$ , so $g_{y} (0, 0) = 0$ . The implicit function theorem hypothesis fails at $(0, 0)$ in this orientation, and the equation cannot be solved for $y$ as a $C^{1}$ function of $x$ near the origin (the curve is the folium of Descartes, which has a self-intersection at the origin). The same hypothesis fails for solving for $x$ as a function of $y$ , since $g_{x} (0, 0) = 0$ too. Rubric: full credit for computing $g_{y} (0, 0) = 0$ and noting the theorem does not apply.

Exercise 3 (medium, symbolic).

Let $g (x, y, z) = x^{2} + y^{2} + z^{2} - 1$ . The zero set is the unit sphere. At the point $(0, 0, 1)$ , write down the implicit function theorem's local-graph conclusion and compute the partial derivatives of the local solution at $(0, 0)$ .

Hint

The variables being solved for are the last block: $z$ as a function of $(x, y)$ . Use $D h (a) = - D_{2} g (a, b)^{- 1} D_{1} g (a, b)$ .

Answer

$D_{2} g (0, 0, 1) = g_{z} (0, 0, 1) = 2$ , nonzero, so the theorem applies. Locally, $z = h (x, y)$ with $h (0, 0) = 1$ and $g (x, y, h (x, y)) = 0$ on a small neighbourhood of $(0, 0)$ . The derivative formula gives $D h (0, 0) = - (2)^{- 1} (g_{x}, g_{y}) ∣_{(0, 0, 1)} = - (1/2) (0, 0) = (0, 0)$ . So $h_{x} (0, 0) = 0$ and $h_{y} (0, 0) = 0$ . Explicitly $h (x, y) = 1 - x^{2} - y^{2}$ , the upper hemisphere, whose partial derivatives at $(0, 0)$ are indeed $0$ . Rubric: full credit for identifying $D_{2} g$ as invertible, applying the derivative formula, and verifying both partials equal $0$ .

Exercise 4 (medium, numeric).

Let $f (x, y) = (x + y, x y)$ . Compute $det D f$ at the point $(1, 2)$ . Then compute the $(1, 1)$ -entry of $(D f (1, 2))^{- 1}$ , which is the rate of change of the first component of the local inverse with respect to the first output coordinate.

Hint

$det D f (x, y) = x - y$ . The inverse of a $2 \times 2$ matrix $(a c b d)$ is $\frac{1}{a d - b c} (d - c - b a)$ .

Answer

$- 2$ . $D f (x, y) = (1 y 1 x)$ , $det D f (x, y) = x - y$ , so $det D f (1, 2) = - 1$ . The inverse is $\frac{1}{- 1} (1 - 2 - 1 1) = (- 1 2 1 - 1)$ . The $(1, 1)$ -entry of this matrix is $- 1$ — careful: the question asks for the rate of change of the first inverse component with respect to the first output coordinate, which is the $(1, 1)$ -entry of $(D f)^{- 1}$ . The numerical answer is $- 1$ , not $- 2$ as the original computation drift might suggest; rubric: full credit for the determinant $- 1$ and the inverse-entry value $- 1$ . (Cross-check: differentiate $u = x + y$ , $v = x y$ to solve for $x, y$ in terms of $u, v$ .)

Exercise 5 (medium, short-answer).

State and prove the regular-value form of the implicit function theorem: if $g : U \subseteq R^{n + m} \to R^{m}$ is $C^{k}$ and the derivative $D g (p)$ is surjective at every point $p$ in the zero set $Z = {p : g (p) = 0}$ , then $Z$ is locally a $C^{k}$ graph at every one of its points.

Hint

Surjectivity of $D g (p)$ on a target $R^{m}$ from a source $R^{n + m}$ means the $m \times (n + m)$ Jacobian matrix has full row rank. By rearranging coordinates, find a square submatrix that is invertible.

Answer

The Jacobian matrix $D g (p) \in R^{m \times (n + m)}$ has full row rank $m$ at every $p \in Z$ by surjectivity. So there is some $m$ -element subset $S$ of the $n + m$ columns at which the corresponding $m \times m$ submatrix is invertible. Permute coordinates on $R^{n + m}$ to put the columns of $S$ in the last $m$ positions, so that in the new ordering $D_{2} g (p)$ is invertible. The implicit function theorem applied in this coordinate system gives a local $C^{k}$ graph $y = h (x)$ for $g (x, y) = 0$ near $p$ . The subset $Z$ is locally a $C^{k}$ graph at $p$ in some choice of coordinates, which is the defining property of an $n$ -dimensional $C^{k}$ submanifold of $R^{n + m}$ . Rubric: full credit for the rank argument, the coordinate permutation, and the application of the implicit theorem in the new coordinates.

Exercise 6 (hard, short-answer).

Let $f : R^{n} \to R^{n}$ be a $C^{1}$ map with $det D f (x) \neq = 0$ for all $x \in R^{n}$ . Prove that the image $f (R^{n})$ is open in $R^{n}$ . (This is the open mapping property for everywhere-regular $C^{1}$ maps.)

Hint

The inverse function theorem applied at each point of $R^{n}$ produces a local diffeomorphism, hence a local homeomorphism, hence an open map locally.

Answer

Pick any $y_{0} \in f (R^{n})$ , say $y_{0} = f (x_{0})$ . The inverse function theorem at $x_{0}$ gives open neighbourhoods $V ∋ x_{0}$ and $W ∋ y_{0}$ with $f ∣_{V} : V \to W$ a $C^{1}$ bijection. In particular $W \subseteq f (V) \subseteq f (R^{n})$ , so $f (R^{n})$ contains an open neighbourhood of $y_{0}$ . Since the point $y_{0}$ was arbitrary, $f (R^{n})$ is open. The same argument shows that for any open $U \subseteq R^{n}$ , the image $f (U)$ is open — the open-map property holds for any $C^{1}$ map with everywhere-invertible derivative. Rubric: full credit for the local-diffeomorphism step, the inclusion $W \subseteq f (R^{n})$ , and the open-map conclusion.

Exercise 7 (hard, short-answer).

Derive the Lagrange multiplier rule from the implicit function theorem. Specifically: let $f, g : R^{n} \to R$ be $C^{1}$ and suppose $a \in R^{n}$ is a local extremum of $f$ subject to the constraint $g (x) = 0$ . If $\nabla g (a) \neq = 0$ , prove there is a scalar $λ \in R$ with $\nabla f (a) = λ \nabla g (a)$ .

Hint

Use the implicit function theorem on $g$ to parametrise the constraint surface locally. Then $f$ restricted to the parametrisation has $a$ as a free local extremum.

Answer

Since $\nabla g (a) \neq = 0$ , at least one component $g_{x_{i}} (a) \neq = 0$ ; relabel so that $g_{x_{n}} (a) \neq = 0$ . The implicit function theorem applied to $g$ at $a$ in the coordinate split $(x_{1}, \dots, x_{n - 1}; x_{n})$ gives a $C^{1}$ map $h$ with $g (x^{'}, h (x^{'})) = 0$ on a neighbourhood of $a^{'} = (a_{1}, \dots, a_{n - 1})$ . Differentiating in $x^{'}$ at $a^{'}$ , the chain rule 02.05.03 gives the row identity $$ (g_{x_1}(a), \ldots, g_{x_{n-1}}(a)) + g_{x_n}(a) \nabla h(a') = 0, $$ hence $\nabla h (a^{'}) = - (g_{x_{1}}, \dots, g_{x_{n - 1}}) (a) / g_{x_{n}} (a)$ . The restricted function $F (x^{'}) = f (x^{'}, h (x^{'}))$ has a free local extremum at $a^{'}$ , so $\nabla F (a^{'}) = 0$ . By chain rule again, $\nabla F (a^{'}) = (f_{x_{1}}, \dots, f_{x_{n - 1}}) (a) + f_{x_{n}} (a) \nabla h (a^{'}) = 0$ . Substituting the expression for $\nabla h (a^{'})$ and clearing denominators gives $\nabla f (a) = λ \nabla g (a)$ for $λ = f_{x_{n}} (a) / g_{x_{n}} (a)$ . Rubric: full credit for the implicit-function reduction, the chain-rule application to $F$ , and the algebraic extraction of $λ$ .

Exercise 8 (hard, short-answer).

Show that the inverse function theorem fails for $C^{0}$ maps even when a continuous inverse exists. Specifically, construct a continuous bijection $f : R \to R$ whose inverse $f^{- 1}$ is not differentiable at some point, despite $f$ being smooth elsewhere.

Hint

Take $f (x) = x^{3}$ . It is smooth, strictly increasing, and bijective on $R$ . Examine its derivative at the origin.

Answer

The map $f (x) = x^{3}$ is smooth (in fact $C^{\infty}$ ), strictly increasing, and a continuous bijection on $R$ , with continuous inverse $f^{- 1} (y) = y^{1/3}$ . But $f^{'} (0) = 0$ , so the inverse function theorem hypothesis (invertibility of the derivative at the point) fails at $x = 0$ . The conclusion of the theorem also fails: the inverse $f^{- 1} (y) = y^{1/3}$ is not differentiable at $y = 0$ , because $(f^{- 1})^{'} (y) = y^{- 2/3} /3 \to \infty$ as $y \to 0$ . The example shows that smoothness of $f$ alone is not enough — the derivative-invertibility hypothesis is essential. Rubric: full credit for the example, the noting that $f^{'} (0) = 0$ kills the hypothesis, and the noting that $(f^{- 1})^{'}$ diverges at $0$ .

Lean formalization [Intermediate+]

lean_status: partial — Mathlib provides the inverse function theorem in Fréchet-derivative form through HasFDerivAt.localInverse, HasStrictFDerivAt.to_localInverse, and the contraction-mapping driver. The implicit function theorem is packaged as HasStrictFDerivAt.implicitFunction with the split-domain $C^{k}$ map and the derivative formula. The textbook-style packaging in Apostol notation and the constant-rank theorem under one named result is the Codex-facing gap.

[object Promise]

The companion module at Codex.Analysis.MultiVariable.ImplicitInverse re-exports these statements and records the unification gap.

Advanced results [Master]

Banach-space inverse function theorem. Let $X$ , $Y$ be Banach spaces, $U \subseteq X$ open, $f : U \to Y$ a $C^{1}$ Fréchet-differentiable map, and $a \in U$ with $D f (a) : X \to Y$ a topological linear isomorphism (a continuous linear bijection with continuous inverse). Then there are open neighbourhoods $V ∋ a$ and $W ∋ f (a)$ with $f ∣_{V} : V \to W$ a $C^{1}$ bijection whose inverse is $C^{1}$ on $W$ ^{[Dieudonné Ch. X §10.2]}. The proof transcribes the Euclidean contraction-mapping argument: the $T_{y} : x \mapsto x - D f (a)^{- 1} (f (x) - y)$ construction is a contraction on a closed ball in $X$ , and completeness of $X$ delivers the fixed point. The hypothesis that $D f (a)$ is a topological isomorphism — not just an algebraic bijection — is essential: on Banach spaces, a continuous linear bijection $X \to Y$ has continuous inverse iff $X$ and $Y$ are complete and the open mapping theorem applies, but a Fréchet derivative that is merely algebraically bijective without topological inverse can fail to deliver a $C^{1}$ local inverse.

Holomorphic inverse function theorem. Let $U \subseteq C^{n}$ be open and $f : U \to C^{n}$ a holomorphic map. If $a \in U$ and the complex Jacobian $D f (a) \in C^{n \times n}$ is invertible (equivalently, $det D f (a) \neq = 0$ ), then there exist open neighbourhoods $V ∋ a$ and $W ∋ f (a)$ with $f ∣_{V} : V \to W$ a biholomorphism — a holomorphic bijection with holomorphic inverse. The proof runs the same contraction-mapping argument with holomorphicity preserved at each step, and the resulting local inverse is automatically holomorphic by the Cauchy-Riemann equations applied to the inverse relation $f \circ f^{- 1} = id$ . The holomorphic version powers the local theory of complex manifolds and underlies the definition of an étale morphism in algebraic geometry: a morphism of smooth schemes over $C$ is étale at a point iff the induced map on the algebraic tangent space is an isomorphism, which by the holomorphic IFT is equivalent to being a local biholomorphism.

Real-analytic inverse function theorem. If $f : U \to R^{n}$ is real-analytic and $D f (a)$ is invertible at $a \in U$ , the local inverse $f^{- 1}$ is real-analytic on a neighbourhood of $f (a)$ . Proved via the Cauchy-Kovalevskaya majorant-series technique: bound the Taylor coefficients of $f^{- 1}$ by a geometric series, conclude convergence on a small ball. Originator: Cauchy 1831 in his Turin lectures on celestial mechanics ^{[Cauchy 1831]}.

Constant rank theorem. Let $U \subseteq R^{n}$ be open and $f : U \to R^{m}$ a $C^{k}$ map with constant rank $r$ on $U$ — that is, $rank D f (p) = r$ for every $p \in U$ . Then for each $a \in U$ there exist $C^{k}$ local diffeomorphisms $ϕ$ near $a$ in $R^{n}$ and $ψ$ near $f (a)$ in $R^{m}$ such that $ψ \circ f \circ ϕ^{- 1}$ is the linear projection $(x_{1}, \dots, x_{n}) \mapsto (x_{1}, \dots, x_{r}, 0, \dots, 0)$ on a neighbourhood of the origin. The proof iterates the inverse function theorem on a rearrangement of coordinates that makes the top-left $r \times r$ block of the Jacobian invertible; the implicit function theorem then absorbs the remaining $m - r$ output coordinates as functions of the first $r$ inputs, and a final coordinate change linearises the structure. The constant rank theorem is the geometric statement that subsumes both inverse (case $r = n = m$ ) and implicit (case $r = m < n$ ) function theorems: every $C^{k}$ map of constant rank is locally a linear projection up to diffeomorphism.

Nash-Moser hard implicit function theorem. Let $X$ , $Y$ be tame Fréchet spaces (a class of locally convex topological vector spaces with a graded sequence of seminorms and a smoothing-operator family). Let $f : U \to Y$ be a smooth map with $D f (a)$ admitting a tame right inverse $L (a) : Y \to X$ — meaning the inverse loses a finite, controlled number of derivatives but remains tame. Under appropriate quantitative hypotheses on the loss of derivatives and the smoothing operators, there is a neighbourhood $W$ of $f (a)$ in $Y$ and a smooth map $g : W \to X$ with $f (g (y)) = y$ for $y \in W$ and $g (f (a)) = a$ . The proof runs a Newton-style iteration with smoothing at each step to compensate the loss of derivatives. Originator: John Nash 1956 ^{[Nash 1956]} in solving the Riemannian embedding problem; refined by Jürgen Moser 1966 ^{[Moser 1966]} for the KAM theorem on persistence of quasi-periodic orbits in Hamiltonian systems. The hard IFT extends the classical inverse function theorem from Banach spaces, where the linearised inverse has zero loss of derivatives, to the much wider class of nonlinear PDE problems where Sobolev-space estimates show a loss but only by a bounded amount.

Failure on Banach spaces with non-topological-isomorphism derivatives. On infinite-dimensional Banach spaces, a continuous Fréchet derivative $D f (a) : X \to Y$ that is algebraically a bijection but lacks a continuous inverse is insufficient to conclude $f$ has a local inverse. The standard witness: take $X = Y = c_{0}$ (the Banach space of sequences converging to $0$ ), and let $T : c_{0} \to c_{0}$ send $(x_{1}, x_{2}, \dots) \mapsto (x_{1}, x_{2} /2, x_{3} /3, \dots)$ . The map $T$ is a continuous linear bijection with set-theoretic inverse $T^{- 1} (y_{1}, y_{2}, \dots) = (y_{1}, 2 y_{2}, 3 y_{3}, \dots)$ , but $T^{- 1}$ is unbounded. A $C^{1}$ map $f$ with $D f (a) = T$ cannot be inverted locally as a $C^{1}$ map. The topological-isomorphism hypothesis in the Banach-space IFT is essential.

Synthesis. Five observations organise the unit. First, the inverse and implicit function theorems are two presentations of one content: local linearisation. The auxiliary map $F (x, y) = (x, g (x, y))$ converts each into the other, and the linear-algebra check on $D f$ or $D_{2} g$ is the same condition in different coordinates. Second, the proof rests on the Banach contraction principle applied to the displacement map $T_{y} (x) = x - D f (a)^{- 1} (f (x) - y)$ . The contraction estimate uses the operator-norm bound on $I - D f (a)^{- 1} D f (x)$ , which is small near $a$ because $D f$ is continuous. Third, smoothness of the inverse is a chain-rule 02.05.03 consequence: differentiate $f (f^{- 1} (y)) = y$ to obtain $D (f^{- 1}) (y) = D f (f^{- 1} (y))^{- 1}$ , then iterate to push $C^{k}$ regularity through. Fourth, the theorems generalise smoothly to Banach spaces with the same contraction-mapping argument, holomorphically with the Cauchy-Riemann equations preserving complex-differentiability through the contraction, real-analytically with majorant series, and to tame Fréchet spaces with the Nash-Moser smoothing iteration. The single argument re-runs across four function-space categories with appropriate adjustments. Fifth, the theorems are the foundational mechanism connecting infinitesimal invertibility (the linear-algebra check at one point) to local invertibility (a smooth inverse on a neighbourhood). The bridge is the contraction-mapping argument; the linear-algebra check is the only ingredient. Both theorems unlock the manifold structure on regular level sets and the constant-rank theorem, and together they form the backbone of the local theory of smooth maps.

Full proof set [Master]

Inverse implies implicit. Proved in §"Key theorem with proof" above by the auxiliary map $F (x, y) = (x, g (x, y))$ , its block-triangular derivative with invertible diagonal blocks, the inverse function theorem applied to $F$ , and the chain rule 02.05.03 applied to the identity $g (x, h (x)) = 0$ to extract the derivative formula.

Inverse function theorem (contraction-mapping proof). Sketched in §"Key theorem with proof" above and detailed here. Statement above. Normalise to $a = 0$ , $f (0) = 0$ , $D f (0) = I_{n}$ by left-composing with $D f (a)^{- 1}$ and translating. Define $T_{y} (x) = y + x - f (x)$ ; fixed points of $T_{y}$ are preimages of $y$ under $f$ . The derivative $D T_{y} (x) = I_{n} - D f (x)$ tends to $0$ in operator norm as $x \to 0$ by continuity of $D f$ . Choose $r > 0$ so $∥ I_{n} - D f (x) ∥_{op} \leq 1/2$ on $\overline{B_{r} (0)}$ . The mean-value inequality gives $∥ T_{y} (x_{1}) - T_{y} (x_{2}) ∥ \leq (1/2) ∥ x_{1} - x_{2} ∥$ for $x_{1}, x_{2} \in \overline{B_{r} (0)}$ . Choose $δ > 0$ so $∥ y ∥ < δ$ forces $∥ T_{y} (0) ∥ = ∥ y ∥ < r /2$ , hence $T_{y} (\overline{B_{r} (0)}) \subseteq \overline{B_{r} (0)}$ by the contraction estimate. Banach contraction principle on the complete metric space $\overline{B_{r} (0)}$ gives a unique fixed point $x (y)$ depending continuously on $y$ . Set $f^{- 1} (y) = x (y)$ on the open ball $∥ y ∥ < δ$ . Smoothness of $f^{- 1}$ comes from chain rule 02.05.03 applied to $f \circ f^{- 1} = id$ : $D f (f^{- 1} (y)) \cdot D (f^{- 1}) (y) = I_{n}$ , hence $D (f^{- 1}) (y) = D f (f^{- 1} (y))^{- 1}$ , a continuous function of $y$ . Iterate to push $C^{k}$ regularity through. $□$

Regular value theorem. Stated as Exercise 5. Surjectivity of $D g (p)$ at $p \in Z = {g = 0}$ gives an $m \times m$ invertible submatrix of $D g (p)$ . Permute coordinates so this submatrix sits in the last $m$ columns. The implicit function theorem produces a local $C^{k}$ graph. The zero set $Z$ is locally an $n$ -dimensional graph at every $p \in Z$ — the defining property of an $n$ -dimensional $C^{k}$ submanifold of $R^{n + m}$ . $□$

Banach-space inverse function theorem. Statement above. The Euclidean proof transcribes with $T_{y} (x) = x - D f (a)^{- 1} (f (x) - y)$ now a map on a closed ball in $X$ . The contraction estimate uses the operator norm on bounded linear maps between Banach spaces; the mean-value inequality holds for $C^{1}$ maps on Banach spaces by an integration of the derivative along a line segment. Completeness of $X$ is what makes the closed ball complete in the induced metric and powers the Banach contraction principle. The smoothness of the inverse is again a chain-rule consequence; the matrix inverse is continuous on the open set of topological isomorphisms in the operator-norm topology. $□$

Holomorphic inverse function theorem. Statement above. The contraction-mapping argument runs verbatim with complex differentiability replacing real differentiability throughout. The Cauchy-Riemann equations for $f$ pass through the contraction to the limit $f^{- 1}$ . The matrix inverse is a polynomial-rational function of the matrix entries, hence holomorphic in the entries; the local inverse is holomorphic as the composition of holomorphic operations. $□$

Constant rank theorem. Statement above. By rearranging coordinates on the source and target, place the invertible $r \times r$ submatrix of $D f (a)$ in the top-left position. The first $r$ output coordinates $(f_{1}, \dots, f_{r})$ , viewed as a map from $R^{n}$ to $R^{r}$ , have full-rank Jacobian at $a$ in the first $r$ input coordinates; the inverse function theorem applied to the augmented map $(x_{1}, \dots, x_{n}) \mapsto (f_{1} (x), \dots, f_{r} (x), x_{r + 1}, \dots, x_{n})$ yields a local diffeomorphism $ϕ$ in $R^{n}$ . In the new $ϕ$ -coordinates, the first $r$ components of $f \circ ϕ^{- 1}$ are simply the first $r$ coordinates. Constant rank then forces the remaining $m - r$ components of $f \circ ϕ^{- 1}$ to depend only on the first $r$ coordinates (since the rank in the last $n - r$ coordinates is already saturated by the first $r$ output components). A final target-side diffeomorphism $ψ$ kills the dependence of the trailing $m - r$ components on the first $r$ , yielding the canonical projection. $□$

Nash-Moser hard IFT (sketch). Statement above. The proof runs a smoothed Newton iteration $u_{k + 1} = u_{k} - S_{t_{k}} L (u_{k}) f (u_{k})$ where $S_{t}$ are smoothing operators that compress the function space onto its low-frequency component up to scale $t$ , and $L (u_{k})$ is the approximate right inverse of $D f (u_{k})$ . The loss of derivatives in $L$ is compensated by the smoothing $S_{t_{k}}$ with $t_{k} \to \infty$ at a geometrically rapid rate. Quantitative tame estimates on the smoothing operators and the inverse $L$ are what makes the iteration converge in the Fréchet topology. Full proof in Hamilton's 1982 survey ^{[Hamilton 1982]} (under the bibliography below) building on Nash 1956 and Moser 1966. $□$

Connections [Master]

Chain rule for multi-variable functions 02.05.03 — the chain rule supplies both the proof structure for the inverse function theorem (smoothness of $f^{- 1}$ is recovered by differentiating $f (f^{- 1} (y)) = y$ and applying the chain rule) and the derivative formula for the implicit function theorem (differentiating $g (x, h (x)) = 0$ and solving for $D h (a)$ ). Every quantitative output of this unit is a chain-rule consequence with a contraction-mapping kernel.

Multi-variable limit and continuity 02.05.01 — the contraction-mapping argument that powers the inverse function theorem uses the completeness of closed balls in $R^{n}$ as a complete metric space, and the operator-norm continuity of $D f$ inherits from the multi-variable continuity framework. The Banach contraction principle is the topological engine of the proof; metric-space continuity is its scaffolding.

Smooth manifold 03.02.01 — the regular level set theorem (Exercise 5) gives the implicit-function-theorem certificate that the zero set of a $C^{k}$ submersion is a $C^{k}$ submanifold. The constant rank theorem extends this: a $C^{k}$ map of constant rank has fibres and image both submanifolds. These are the two foundational constructions of submanifolds in $R^{n}$ and on abstract manifolds.

Banach spaces (pending unit 02.11.04) — the Banach-space inverse function theorem packages the contraction-mapping engine on complete normed spaces. The Picard-Lindelöf existence theorem for ODEs and Newton's method on Banach spaces share the same engine. The Nash-Moser hard IFT extends the construction to tame Fréchet spaces, used in KAM theory and the Riemannian embedding problem.

Étale morphisms in algebraic geometry [04.*] — a morphism $f : X \to Y$ of smooth schemes over a field is étale at $x \in X$ iff the induced map on Zariski tangent spaces is an isomorphism. Over $C$ with the analytic topology, étale at $x$ means the holomorphic IFT applies, hence $f$ is a local biholomorphism near $x$ . The two characterisations coincide.

KAM theorem and the Nash-Moser machinery [05.09. — pending unit]* — Kolmogorov-Arnold-Moser theory establishes the persistence of quasi-periodic orbits under small Hamiltonian perturbations. The Nash-Moser hard IFT is the analytic engine: the linearised perturbation equation loses derivatives, the smoothing operators compensate, and the Newton iteration converges in the Fréchet topology. KAM was the original application that motivated the hard IFT.

Riemann surfaces and Riemannian embedding [06., 03.05.] — the holomorphic IFT powers the local theory of Riemann surfaces, where charts are biholomorphisms. The Nash-Moser hard IFT was developed to solve the isometric Riemannian embedding problem: every $C^{k}$ Riemannian manifold for $k$ sufficiently large embeds isometrically into some $R^{N}$ . The proof is a smoothed Newton iteration on a quadratic functional with a loss-of-derivatives linearised inverse.

Historical & philosophical context [Master]

The implicit function theorem in its modern form has a long lineage. Single-variable forerunners go back to Newton's Method of Fluxions (1671, published 1736), where solving an implicit equation for one variable in terms of another was treated via series expansion. In multi-variable form, Lagrange in his Théorie des fonctions analytiques (1797) gave a series-based version, and Cauchy in his Turin lectures of 1831 ^{[Cauchy 1831]} gave the first rigorous analytic-function form via majorant series — the technique that survives in the modern real-analytic IFT. Ulisse Dini's 1877 Lezioni di analisi infinitesimale ^{[Dini 1877]} established the modern form on $R^{n}$ under the now-standard hypothesis of continuous partial derivatives, and the theorem carries his name in Italian and French mathematical traditions.

Édouard Goursat's 1903 Sur la théorie des fonctions implicites ^{[Goursat 1903]} in the Bulletin de la Société Mathématique de France gave the contraction-mapping proof under the modern $C^{1}$ hypothesis, packaging the theorem in essentially the form taught today. The Banach-space generalisation came with Stefan Banach's 1922 introduction of complete normed spaces and the contraction principle, and was developed in textbook form by Jean Dieudonné in his 1960 Foundations of Modern Analysis ^{[Dieudonné Ch. X §10.2]}. Apostol's 1969 Calculus Vol. 2 Ch. 13 ^{[Apostol Ch. 13]} gave the canonical undergraduate pedagogical presentation, with the inverse and implicit theorems proved together via the contraction-mapping reduction. Spivak's 1965 Calculus on Manifolds Ch. 2 ^[Spivak] gave the parallel honours-undergraduate presentation in the modern coordinate-free language.

The hard implicit function theorem came from a different tradition. John Nash in his 1956 paper The imbedding problem for Riemannian manifolds ^{[Nash 1956]} in the Annals of Mathematics introduced a smoothed Newton iteration to solve the isometric embedding problem, in which the linearised equation loses derivatives. Jürgen Moser in 1966 ^{[Moser 1966]} generalised and clarified the technique, applying it to the KAM theorem on persistence of quasi-periodic orbits and to nonlinear differential equations on the torus. Richard Hamilton's 1982 survey The inverse function theorem of Nash and Moser (Bulletin of the American Mathematical Society 7) packaged the technique into the modern tame-Fréchet-space framework, in which the Nash-Moser IFT is a tool used routinely in geometric analysis, nonlinear PDE, and dynamical systems.

Bibliography [Master]

[object Promise]

Prerequisites

02.05.03

Tier anchors

beginner: 3Blue1Brown style local-zoom-into-linear-map framing; Strogatz informal 'level-curve as graph' picture
intermediate: Apostol *Calculus* Vol. 2 Ch. 13 §13.4–13.7 (implicit and inverse function theorems with contraction-mapping proofs); Rudin *Principles of Mathematical Analysis* Ch. 9 §9.17–9.29; Spivak *Calculus on Manifolds* Ch. 2 Theorem 2-11 and Theorem 2-12
master: Apostol *Calculus* Vol. 2 Ch. 13 (originator pedagogical presentation); Spivak *Calculus on Manifolds* Ch. 2; Dieudonné *Foundations of Modern Analysis* Ch. X §10.2 (Banach-space form); Cauchy 1831 *Sur la mécanique céleste et sur un nouveau calcul* (analytic implicit-function tradition); Goursat 1903 *Sur la théorie des fonctions implicites* (Bulletin de la Société Mathématique de France 31) — originator of the modern $C^1$-and-Banach formulation; Dini 1877 *Lezioni di analisi infinitesimale* (originator of the modern implicit-function theorem on $\mathbb{R}^n$); Nash 1956 *The imbedding problem for Riemannian manifolds* (Annals of Mathematics 63); Moser 1966 *A rapidly convergent iteration method and non-linear differential equations* (Annali Scuola Norm. Sup. Pisa 20)

References

TODO_REF
Apostol — Calculus Vol. 2 · Ch. 13 §13.4–13.7, implicit and inverse function theorems with the contraction-mapping proof
TODO_REF
Spivak — Calculus on Manifolds · Ch. 2 Theorems 2-11 and 2-12, the inverse and implicit function theorems with the Banach fixed-point proof
TODO_REF
Rudin — Principles of Mathematical Analysis · Ch. 9 §9.17–9.29, the inverse function theorem, the implicit function theorem, and the rank theorem
TODO_REF
Dieudonné — Foundations of Modern Analysis · Ch. X §10.2, the Banach-space inverse and implicit function theorems with the Fréchet-derivative form
TODO_REF
Cauchy 1831 — Sur la mécanique céleste et sur un nouveau calcul · the analytic implicit-function tradition through majorant-series convergence arguments
TODO_REF
Goursat 1903 — Sur la théorie des fonctions implicites · Bulletin de la Société Mathématique de France 31, the modern $C^1$-and-Banach formulation
TODO_REF
Dini 1877 — Lezioni di analisi infinitesimale · originator of the modern implicit-function theorem on $\mathbb{R}^n$ with continuous partial derivatives
TODO_REF
Nash 1956 — The imbedding problem for Riemannian manifolds · Annals of Mathematics 63, the hard-IFT loss-of-derivatives iteration scheme
TODO_REF
Moser 1966 — A rapidly convergent iteration method and non-linear differential equations · Annali Scuola Norm. Sup. Pisa 20, the Nash-Moser tame-Fréchet implicit function theorem with applications to KAM theory

Lean module

Codex.Analysis.MultiVariable.ImplicitInverse

Mathlib gap

Mathlib provides the inverse function theorem in Fréchet-derivative form
through `HasFDerivAt.localInverse`, `HasStrictFDerivAt.to_localInverse`,
and the contraction-mapping driver `ContractingWith.fixedPoint`. The
implicit function theorem lives under `ImplicitFunction` with
`HasStrictFDerivAt.implicitFunction` packaging the split-domain
$C^k$ map and the derivative formula. The Banach-space generalisation
is available through the same APIs since Mathlib's Fréchet derivative
is defined on arbitrary normed spaces. What is not packaged in Mathlib
is a single textbook-style namespace that names the two theorems in
Apostol notation side by side, exhibits the canonical reduction of the
implicit theorem to the inverse theorem via the auxiliary map
$F(x, y) = (x, g(x, y))$, records the Jacobian-matrix derivative
formula $Dh(a) = -D_2 g(a, b)^{-1} D_1 g(a, b)$ explicitly, and
collects the constant-rank theorem and the Nash-Moser hard-IFT under
the same namespace. The Codex module collects these into the textbook
presentation and records the unification gap.

Reviewer

TBD

Estimated time

beginner: 18m
intermediate: 45m
master: 80m