Are Banach manifolds (or other types of infinitedimensional manifolds) just curiosities, or have they been utilized to prove some interesting/important results? Where do they turn up? Important examples?

Some pretty fundamental objects in manifold theory are Banach manifolds. Perhaps the simplest would be the space of $C^k$ diffeomorphisms of a compact manifold M for $k > 0$ finite. There's of course all kinds of variations on this theme: embedding spaces, diffeomorphisms that preserve a structure of some sort, the space of smooth maps between two manifolds, etc, etc. So they're used to prove a variety of results, and they are the "targets" of many important theorems. For example, Smale's theorem on the homotopy type of $Diff(S^2)$, or the SmaleHirsch theorem on the homotopy type of the space of immersions of one manifold in another. Palais's theorem that restriction maps are fiber bundles (more easily seen to be fibrations) was used by Fadell and Neuwirth to show the pure braid groups are iterated semidirect products of free groups. The fact that $Diff(S^1)$ has the homotopy type of $O_2$ says that a circle bundle over a space is always equivalent to a circle bundle with linear structure group, etc. IMO the answer to your question can be summed up in a little nugget of an observation that if you value manifolds, it's only natural to value the automorphisms of manifolds, and mapping spaces of manifolds. And since these mapping spaces have a natural structure (of a Banach manifold) certainly that should be relevant. 


As a counterpoint to some of the other answers, actually Banach (and Hilbert) manifolds aren't quite as useful as might be hoped. Two indicators of this are:
So Banach and Hilbert manifolds tend to be used as places to put other things. They are big enough to contain just about everything but simple enough that they don't add any extra complications. This leads to their use as extreme examples of "very big spaces" and means that for any particular situation one can often chop the infinite down to the finite (but very big). So, for example, with regard to representing Ktheory, for any particular finite dimensional manifold there's a finite dimensional Grassmannian that will do but if you want to represent Ktheory for all finite dimensional manifolds then you need an infinite dimensional Grassmannian. However, the situation changes once you allow other model spaces (the largest category of such is the category of convenient vector spaces, the introduction of which is a very interesting read on calculus in infinite dimensions). There you can and do get much more interesting behaviour and you discover that you can study infinite dimensional manifolds as objects in their own right. One example of this is the notion of semiinfinite structure. This is, almost by definition, only available in infinite dimensions (there are shadows in finite) and has proved an important source of ideas, if not actual techniques. Of course, many of the techniques involve bringing things back down to finite dimensions in the final analysis but that's because we want to actually compute something and so end up with a number; and the easiest way to get a number is to count a finite number of things. But that's no different to any other computation, so shouldn't be seen as a disadvantage. So back to the original question. Well, I don't really have a good answer to that because I work with infinite dimensional manifolds so I don't spend any time worrying about what others want to apply this work to, I just get on with it. But nonetheless, one theme that I see a lot is that of the infinite dimensional "picture" being the right one and the one that gives the intuition for how the finite dimensional approximations fit together. Thus we see that Floer theory is really Morse theory applied to loop spaces, but not many will compute it as such. We see that the elliptic genus is (was originally!) really index theory applied to loop spaces, but again that's not useful for computations! In general, anywhere where you've got functions that can vary, you've got an infinite dimensional manifold and it behoves you to remember it because it can give you important insights on how to proceed. 


Infinitedimensional Grassmannians and their tautological bundles arise in topological Ktheory and bordism. See Thom's Quelques propriétés globales des variétés differentiables. 


One needs to use the implicit function theorem and Sard's theorem in the setting of Banach manifolds in order to get the theory of Jholomorphic curves off the ground, which is one of the pillars of symplectic topology. 


Eilenberg Maclane spaces are basic building blocks of homotopy theory. 


Infinite jet spaces are widely used in the geometric theory of PDEs, for instance, when you deal with the infinitesimal higher symmetries that arise in the study of integrable systems. 


Fréchet manifolds show up in some "higher geometry" situations. Here are three which I particularly like: 1.) The group of smooth loops (both based at 1 or free) in a Lie group forms a nice infinitedimensional Lie group. These turn out to be exceptionally useful in integrable systems. For example, there is the DorfmeisterPeditWu generalized Weierstrass representation which gives an explicit parameterization of harmonic maps to symmetric spaces in terms of some holomorphic data on a loop group. 2.) Len Gross uses the Fréchet manifold of piecewise smooth paths in $\mathbb{R}^n$ to analyze the field copy problem. This is the issue that two (nonabelian) $\mathfrak{g}$valued connections on $\mathbb{R}^n$ can have the same curvature without being gaugeequivalent. This is pretty weird; the observables of a gauge field are built out of the curvature, but with field copies you have two inequivalent fields with the same observables. At least, that's how I understand it. I'm curious if there is a tamer explanation. 3.) Brylinski does some stuff with the Fréchet manifolds of loops in a manifold in his book. I don't have it handy for reference, but there are some interesting observations. For example, the path space of a symplectic manifold is almostcomplex. 


Hitchin’s Moduli Space in Geometric Langlands is obtained by a reduction from an infinitedimensional space of connections. See



Douady introduced Banach analytic manifolds in order to solve a conjecture of Grothendieck's on the existence of a moduli space for compact analytic subspaces of a given fixed analytic space. These Banach analytic manifolds were then put to good use in many subsequent important papers (Barlet, Palamodov, Grauert,...). The use of infinitedimensional analytic manifolds is characteristic for this area. Here are the first lines of Douady's spectacular thesis [my translation]: "The aim of this work is to provide its author with the status of Doctor in Mathematics and the set H(X) of compact analytic subspaces of X with the structure of an analytic space. In order to formulate the second problem more precisely..." A link to the thesis: 


This is encompassed by some of the fancier examples above, but a good "classic" example of natural infinite dimensional manifolds is the space of paths connecting two points on a finitedimensional base manifold. For example a natural interpretation of deriving the Euler equations from the Calculus of Variations is to find points in the path manifold where the derivative of the action functional vanishes. If you use the length functional you get the geodesic equations of a Riemannian manifold. Going a step further and studying the second derivative in the path manifold leads to some nice theorems relating the curvature of the base manifold and its topology. 


Malliavin introduced his analysis of functionals on the Wiener space to obtain a probabilistic proof of the Hoermander theorem. Hoermander theorem states that the generalized Heat equation on R^n has a smooth solution whenever the driving function is smooth, provided that the Lie algebra of the heat operator generators span the whole of R^n at each point. Of course, analysis on Wiener spaces have many applications in other areas also. This is a reference to a review of "Stochstic analysis" by Malliavin 


David Ebin and Jerry Marsden proved in a 1970 paper in the Annals that the Euler and NavierStokes equations are wellposed for short amounts of time. This result uses the geometry of infinitedimensional manifolds in a very fundamental way: the configuration space of an incompressible fluid in a container $M$ is the group of volumepreserving diffeomorphisms $\mathrm{Diff}_{\mathrm{vol}}(M)$ of $M$ and this is of course an infinitedimensional manifold. The proof then relies on the fact that the Euler equations define a Hamiltonian vector field on this space, and by carefully unwinding the definitions and putting everything in the right Sobolev space you can essentially use existence and uniqueness theorems for ODEs to prove the desired result. I'm of course glossing over many details. One of the problems, for instance, when trying to make this idea rigorous is that the convective term $\mathbf{u} \cdot \nabla \mathbf{u}$ in the Euler equations leads to derivative loss, but this can be surmounted by rewriting the equations in Lagrangian form. If you want to do all this going back and forth in a proper way, you need a good understanding of the underlying geometry of $\mathrm{Diff}_{\mathrm{vol}}(M)$. In my opinion, this is quite an amazing result, since it is both powerful and conceptually very clear. There are essentially no hard estimates in the paper, just applications of the Sobolev embedding theorems, Hodge decompositions, properties of vector fields, .... Global analysis at its best! 


Loop groups (spaces of maps $S^1 \to G$ where $G$ is a Lie group) are nice examples of infinite dimensional manifolds, and they are important in physics and string theory. They have a rich and interesting theory, the basics of which are developed for example in the book "Loop Groups" by Pressley and Segal. See also the paper "Unitary representations of some infinite dimensional groups" by Segal. As for interesting results, there is the recent work of FreedHopkinsTeleman which relates the representation theory of the loop group $LG$ ("Verlinde ring") and the twisted equivariant $K$theory of the Lie group $G$. In general, infinite dimensional things come up often in quantum field theory. For example the fields under consideration might be sections of a vector bundle, or say spaces of maps of surfaces into a manifold. It is important to understand these spaces of fields, because we want to do "integrals" over them. 


The Wasserstein space of a compact Riemannian manifold is the set of Borel probablity measures endowed with a distance defined using optimal transportation (roughly, the distance between two measures is the least cost needed to transport one to the other, given that it costs $m d^2$ to move an amount $m$ of mass by a distance $d$.) It has been noticed by Otto that this Wasserstein space can be considered an infinitedimensional manifold. He used this insight to convert some PDEs into gradient flows on the Wasserstein space, the goal being to get existence and uniqueness result more easily. I should add that Gigli recently proposed a rigorous framework for the differentiable structure of Wasserstein spaces. 


There are far to be just curiosities. Infinite dimensional Finsler manifolds are fundamental tools in Variational Calculus. There is a lot of old/recent papers dealing with the infinite dimensional LusternikSchnirelmann theory. Just to select one (sorry for writing the hyperlink on three lines, but it seems it's the only way, I do not know why): http://archive.numdam.org/ARCHIVE/AIHPC/AIHPC_1988__5_2/ AIHPC_1988__5_2_119_0/ AIHPC_1988__5_2_119_0.pdf [and the references therein]. 

