Choice-free smooth inverse function theorem in Euclidean space

Take $R,q,C$ from [F1] and choose the explicit positive number $\delta =(1-q)R\mathrm{/}(2C)$. Put $W=B(b,\delta )$. For $y\in W$ and $x\in \bar{B}(a,R)$, $\mathrm{\parallel }{T}_y(x)-a{\mathrm{\parallel }}_2\le \mathrm{\parallel }{T}_y(x)-T_y(a){\mathrm{\parallel }}_2+\mathrm{\parallel }B(y-b){\mathrm{\parallel }}_2\le qR+C\delta =(1+q)R\mathrm{/}2<R\mathrm{.}$ Thus $T_y$ maps the closed ball strictly into its open interior.

The closed ball is complete without choice. Indeed, a Cauchy sequence $(x_k)$ in it is Cauchy in ${\mathbb{R}}^n$, so [F2] gives its unique limit $x$. The triangle inequality yields $\mathrm{\parallel }x-a{\mathrm{\parallel }}_2\le \mathrm{\parallel }x-x_k{\mathrm{\parallel }}_2+R$ for every $k$; if $\mathrm{\parallel }x-a{\mathrm{\parallel }}_2>R$, choosing $k$ with $\mathrm{\parallel }x-x_k{\mathrm{\parallel }}_2<\mathrm{\parallel }x-a{\mathrm{\parallel }}_2-R$ is a contradiction. Hence $x$ remains in the ball. The ball is nonempty because it contains $a$.

For each fixed $y\in W$, [F1], step 1.1, step 1.2, and [F2] give a unique fixed point $g(y)\in \bar{B}(a,R)$. This defines a function without a choice axiom: $g(y)$ is the unique object satisfying the displayed fixed-point property. Its equation is $B(y-f(g(y)))=0$, hence $f(g(y))=y$ because $B$ is injective; step 1.1 puts $g(y)$ in $B(a,R)$.

If $x,z\in \bar{B}(a,R)$ and $f(x)=f(z)=y$, then $T_y(x)=x$ and $T_y(z)=z$, so [F1] gives $\mathrm{\parallel }x-z{\mathrm{\parallel }}_2\le q\mathrm{\parallel }x-z{\mathrm{\parallel }}_2$ and therefore $x=z$. Define $V=B(a,R)\cap f^{-1}[W]$. By [F3], $V$ is open; it contains $a$, lies in $U$, and step 2.1 together with injectivity shows that $f{\mathrm{\mid }}_V:V\to W$ is bijective with inverse $g$.

For $y,z\in W$, the fixed-point equations and [F1] give $\mathrm{\parallel }g(y)-g(z){\mathrm{\parallel }}_2\le q\mathrm{\parallel }g(y)-g(z){\mathrm{\parallel }}_2+C\mathrm{\parallel }y-z{\mathrm{\parallel }}_2,$ so $\mathrm{\parallel }g(y)-g(z){\mathrm{\parallel }}_2\le C(1-q{)}^{-1}\mathrm{\parallel }y-z{\mathrm{\parallel }}_2$. Thus $g$ is Lipschitz and continuous.

Fix $y\in W$, put $x=g(y)$ and $L=Df(x)$. For small $h$ with $y+h\in W$, put $k=g(y+h)-x$. Step 3.2 gives $\mathrm{\parallel }k{\mathrm{\parallel }}_2=O(\mathrm{\parallel }h{\mathrm{\parallel }}_2)$, while [F3] and $f(g(y+h))-f(g(y))=h$ give $h=Lk+r(k)$ with $\mathrm{\parallel }r(k){\mathrm{\parallel }}_2=o(\mathrm{\parallel }k{\mathrm{\parallel }}_2)$. The inverse bound in [F1] therefore gives $k=L^{-1}h-L^{-1}r(k)=L^{-1}h+o(\mathrm{\parallel }h{\mathrm{\parallel }}_2)$, including the case $k=0$. Hence $Dg(y)=Df(g(y){)}^{-1}$. The chain rule in [F5] also gives $Df(g(y))Dg(y)=I$ from $f\circ g={\mathrm{id}}_W$, consistently with this formula.

The map $g$ is $C^1$: it is continuous by step 3.2, $Df\circ g$ is continuous, and [F4] makes its inverse matrix $Dg$ continuous. Inductively, suppose $g$ is $C^r$ for some $r\ge 1$. Because $f$ is smooth, the matrix entries of $Df$ are $C^r$; [F4] makes $Df\circ g$ and then $(Df\circ g{)}^{-1}=Dg$ of class $C^r$. Thus the first partial derivatives of $g$ are $C^r$, so [F4] makes $g$ of class $C^{r+1}$. Induction proves $g$ is smooth, and [F4] and step 3.1 make $f{\mathrm{\mid }}_V$ a diffeomorphism.

The hypothesis $n\ge 1$ excludes the zero-dimensional Euclidean convention; dimension one is included verbatim. The datum $a\in U$ makes the empty-domain case impossible. Invertibility excludes a degenerate derivative, while zero increments are covered in step 4.1. All domains are open, and the closed ball is used only as the complete space for iteration, so no boundary point is asserted to lie in $V$. The construction chooses explicit $\delta$, starts every Newton iteration at the specified point $a$, and defines each value by uniqueness; finite induction on derivative order and unique Euclidean limits use no choice axiom.