Applications of model theory to analysis

There is a result in functional analysis whose first known proof uses non-standard techniques:

Theorem If a bounded linear operator $ T $ on a Hilbert space $ \mathcal{H} $ is polynomially compact, i.e., $ P(T) $ is compact for some non-zero polynomial $ P $, then $ T $ has an invariant subspace. This means that there is a non-trivial proper subspace $ W $ of $ \mathcal{H} $ such that $ p(T)[W] \subseteq W $.

The proof was given by Allen Bernstein and Abraham Robinson. Their result is significant because it is related to the so-called Invariant-Subspace Conjecture, an important unsolved problem in functional analysis. Paul Halmos, a staunch critic of non-standard analysis, supplied a standard proof of the result almost immediately after reading the pre-print of the Bernstein-Robinson paper. In fact, both proofs were published in the same issue of the Pacific Journal of Mathematics!

Ax found the following application in complex analysis:

Theorem: If $f : \mathbb{C}^n \to \mathbb{C}^n$ is an injective polynomial function, that is there exist $f_1,...,f_n \in \mathbb{C}[X_1,...,X_n]$ such that $f=(f_1,...,f_n)$, then $f$ is surjective.

You can show that the theorem holds for $f : k^n \to k^n$ where $k$ is a locally finite field, therefore it holds for the algebraic closure $\overline{\mathbb{F}_p}= \bigcup\limits_{n \geq 1} \mathbb{F}_{p^n}$ of $\mathbb{F}_p$. Then, it holds for the (non trivial) ultraproduct $K=\prod\limits_{p \in \mathbb{P}} \overline{\mathbb{F}_p} / \omega$ where $\omega$ is a non principal ultrafilter over the set of primes $\mathbb{P}$, because the theorem can be expressed as a set of sentences of the first order. But $K$ is an algebraic closed field of caracteristic $0$ and the theory of algebraic closed fields of caracteristic $0$ is complete, so $K$ and $\mathbb{C}$ are elementary equivalent. Finally, Ax theorem is proved.

Ax theorem was generalized by Grothendieck.

Using continuous model theory, Ilijas Farah, Brad Hart and David Sherman proved `blind man's version' of the Connes Embedding Problem:

There exists a separable ${\rm II}_1$-factor $M$ such that every other separable ${\rm II}_1$-factor embeds into an ultrapower of $M$.

I find this result pretty amusing. On the C*-algebra side, I like results à la the Löwenheim–Skolem theorem: build a non-separable C*-algebra with your favourite axiomatisable properties and go to a separable C*-algebra which inherits those properties.