I was studying the following theorem:
Theorem [Hadamard-Lévy]. Let $f\colon \mathbb R^n\to \mathbb R^n$ of class $C^2$. Then $f$ is a $C^1$-diffeomorphism on $\mathbb R^n\to \mathbb R^n$ if, and only if, $f$ is a proper map and the determinant of the Jacobian matrix is non-null everywhere.
Do you know any application, any theorem where this is a useful result?
The Hadamard-Lévy theorem is a powerful tool to build all kind of diffeomorphisms of the Euclidean space. Here is an example of these constructions:
Theorem. There exists $\varepsilon>0$ such that for all $a\in\mathbb{R}^n$ with $\|a\|\leqslant\varepsilon$ and $A\in\textrm{GL}(n,\mathbb{R})$ with $\|A-I_n\|\leqslant\varepsilon$, there exists $f\colon\mathbb{R}^n\rightarrow\mathbb{R}^n$ a diffeomorphism such that: $$f_{\vert B(0,1)}=A+a\textrm{ and }f_{\vert\mathbb{R}^n\setminus B(0,2)}=\textrm{id}.$$
Proof. Let $g\colon\mathbb{R}^n\rightarrow\mathbb{R}^n$ be a smooth function such that $g(t)=1$ for $|t|<1$ and $g(t)=0$ for $|t|\geqslant 2$, then let define the map $f\colon\mathbb{R}^n\rightarrow\mathbb{R}^n$ by: $$f(x)=x+g(\|x\|^2)(Ax+a-x).$$ Notice that $f$ is clearly a proper map since $\lim\limits_{\|x\|\to+\infty}\|f(x)\|=+\infty$ and that one also has: $$\forall x\in\mathbb{R}^n,(\|x\|<1\textrm{ or }\|x\|\geqslant 2)\implies\mathrm{d}_xf\in\textrm{GL}(n,\mathbb{R}).$$ Therefore, using Hadamard-Lévy's theorem it suffices to see that $\mathrm{d}_xf$ is still invertible for all $1\leqslant \|x\|<2$. To do so, notice that: $$\mathrm{d}_xf\cdot h=h+g(\|x\|^2)(Ah-h)+2\langle x,h\rangle g'(\|x\|^2)(Ax+a-x).$$ Let $M$ be an upper bound for $g'$, then: $$\|\mathrm{d}_xf-\textrm{id}\|<(1+4M)\|A-I_n\|+4M\|a\|.$$ Playing on $\varepsilon$, $\mathrm{d}_xf$ can be arbitrarly close of $I_n$. Whence, $\mathrm{d}_xf$ is invertible, since $\textrm{GL}(n,\mathbb{R})$ is open. $\Box$
The meaning is that an affine isomorphism of $\mathbb{R}^n$ sufficiently close of $\textrm{id}$ can be extended to a diffeomorphism of $\mathbb{R}^n$ which is equal to $\textrm{id}$ away from $0$.
Even stronger, let define $F\colon[0,1]\times\mathbb{R}^n\rightarrow\mathbb{R}^n$ by: $$F(t,x)=x+tg(\|x\|^2)(Ax+a-x).$$ For all $t\in[0,1]$, the same proof leads to $F(t,\cdot)$ being a diffeomorphism of $\mathbb{R}^n$ and $f$ is even isotopic to $\textrm{id}$ i.e. there is a continuous path of diffeomorphisms between $f$ and $\textrm{id}$.
