Added the inverse function theorem.

src/dg/derivative/index.tex

@@ -7,3 +7,4 @@
 \input{./higher.tex}
 \input{./taylor.tex}
 \input{./power.tex}
+\input{./inverse.tex}

src/dg/derivative/inverse.tex

@@ -0,0 +1,52 @@
+\section{Inverse Mappings}
+\label{section:inverse-function-theorem}
+
+\begin{theorem}[Inverse Function Theorem]
+\label{theorem:inverse-function-theorem}
+    Let $E$ be a Banach space, $U \subset E$ be open, $p \ge 1$, $f \in C^p(U; E)$ be $p$-times continuously Fréchet-differentiable, and $x_0 \in U$. If $Df(x_0)$ is an isomorphism, then:
+    \begin{enumerate}
+        \item There exists $V \in \cn_E(x_0)$ such that $f|_V$ is a $C^p$-isomorphism. 
+        \item Let $f^{-1}: f(V) \to V$ be the local inverse of $f$ on $V$, then $Df^{-1}(x_0) = [Df(x_0)]^{-1}$. 
+    \end{enumerate}
+    
+\end{theorem}
+\begin{proof}[Proof, {{\cite[Theorem XIV.1.2]{Lang}}}. ]
+    By translation, assume without loss of generality that $x_0 = f(x_0) = 0$ and $Df(x_0) = Df(0) = I$. 
+
+    \textit{Existence and Uniqueness of Inverse}: Since $f \in C^1$, there exists $r > 0$ such that $\norm{Df(x) - I}_{L(E; E)} < 1/2$ for all $x \in \ol{B_E(0, r)}$. In which case, by \autoref{lemma:neumann-series}, $Df(x)$ is an isomorphism for all $x \in B(0, r)$. Let
+    \[
+    g: \overline{B_E(0, r)} \to E \quad x \mapsto x - f(x)
+    \]
+
+    For any $x, y \in \overline{B_E(0, r)}$, by the \hyperref[Mean Value Theorem]{theorem:mean-value-theorem}, 
+    \[
+    \norm{g(x) - g(y)}_E \le \norm{x}_E \cdot \sup_{y \in \overline{B_E(0, r)}}\norm{Dg(y)}_E \le \frac{\norm{x - y}_E}{2}
+    \]
+    
+    In particular, for any $x \in \overline{B_E(0, r)}$, $\norm{g(x)}_E = \norm{g(x) - g(0)}_E \le \norm{x}_E/2$, so $g: \ol{B_E(0, r)} \to \ol{B_E(0, r/2)}$ is a contraction. 
+
+    For each $y \in B(0, r/2)$, the mapping
+    \[
+    g_y: \overline{B(0, r)} \to \overline{B(0, r)} \quad x \mapsto x - f(x) + y
+    \]
+
+    is also a contraction. By \hyperref[Banach's Fixed Point Theorem]{theorem:banach-fixed-point}, there exists a unique $x \in B(0, r)$ such that $g_y(x) = x$. In which case, $f(x) = y$. Therefore $f$ restricted to $V = f^{-1}(B(0, r))$ is invertible. 
+
+    \textit{Differentiability of Inverse}: Let $f^{-1}: f(V) \to V$ be the local inverse of $f$ on $V$. By assumption, it is sufficient to show that $Df^{-1}(0) = I$ as well. For each $y \in \overline{B(0, r/2)}$, 
+    \begin{align*}
+        \norm{f^{-1}(y) - y}_E &= \norm{f^{-1}(y) - f(f^{-1}(y))}_E \\
+        &= \norm{f^{-1}(y) - f^{-1}(y) - r(f^{-1}(y))}_E = \norm{r(f^{-1}(y))}_E
+    \end{align*}
+
+    where $r(x)/\norm{x}_E \to 0$ as $x \to 0$. In addition, 
+    \begin{align*}
+        \norm{f^{-1}(y)}_E &= \norm{f^{-1}(y) - y + y}_E \\
+        &\le \norm{g(f^{-1}(y))}_E + \norm{y}_E \le 2\norm{y}_E
+    \end{align*}
+
+    so $[f^{-1}(y) - y]/\norm{y}_E \to 0$ as $y \to 0$. Therefore $f^{-1}$ is differentiable at $0$ with $Df^{-1} = I$. 
+
+    \textit{Smoothness of Inverse}: By the above argument, the inverse is differentiable on every point in $B(0, r/2)$, and $Df^{-1}(f(x)) = [Df(x)]^{-1}$ for all $x \in V$. By \autoref{proposition:banach-algebra-inverse}, the inversion map $T \mapsto T^{-1}$ is smooth. Therefore if $Df \in C^{p - 1}$, then $f \in C^{p - 1}$ as well. 
+\end{proof}
+
+