Nash–Moser theorem

Statement

A graded Fréchet space is a Fréchet space $F$ with a fixed increasing sequence of seminorms $\norm{\cdot}_0 \le \norm{\cdot}_1 \le \norm{\cdot}_2 \le \cdots$ that defines its topology. Let $F$ and $G$ be graded Fréchet spaces and let $U \subseteq F$ be open. A continuous map $P \colon U \to G$ is tame if each point of $U$ has a neighbourhood $V$ with this property. There are integers $r, b \ge 0$ and constants $C_n$ with $\norm{P(f)}_n \le C_n(1 + \norm{f}_{n+r})$ for all $f \in V$ and all $n \ge b$. It is smooth tame if it is smooth and all its derivatives are tame. A graded Fréchet space is tame if it is a tame direct summand of a space of exponentially decreasing sequences in a Banach space. For a compact manifold $M$, the space $C^\infty(M)$ graded by the $C^n$ norms is tame.

Let $F$ and $G$ be tame Fréchet spaces, let $U \subseteq F$ be open, and let $P \colon U \to G$ be a smooth tame map. Suppose that for every $f \in U$ the derivative $DP(f) \colon F \to G$ is bijective, and that the family of inverses $VP \colon U \times G \to F$, $VP(f, k) = DP(f)^{-1} k$, is a smooth tame map. Then $P$ is locally invertible: each $f_0 \in U$ has an open neighbourhood $U_0$ such that $P(U_0)$ is open and $P \colon U_0 \to P(U_0)$ is a bijection. Moreover, each such local inverse is a smooth tame map.