Are infinite dimensional constructions needed to prove finite dimensional results? Infinite dimensional constructions, such as spaces of diffeomorphisms, spectra, spaces of paths, and spaces of connections, appear all over topology. I rather like them, because they sometimes help me to develop a good mental picture of what is going on. Emmanuel Farjoun, in the first lecture of an Algebraic Topology course about a decade ago, described "becoming comfortable with the idea of infinite dimensional manifolds" as being "one of the main conceptual advances in topology in the latter half of the 20th century". But, as I realized in a discussion yesterday, I don't understand whether infinite dimensional spaces are needed, or whether they are merely an intuitive crutch.

Are there situations in which a significant finite dimensional result strictly requires an infinite dimensional construction in order to prove it or in order to properly understand it? 
If the answer is no, then at least are there important finite-dimensional theorems for which infinite-dimensional proofs are "clearly"  the easiest and the most natural? (for some conceptual reason which you can explain; not just "a finite-dimensional proof isn't known yet"). 

A closely related question is this, although its focus is somewhat different, and none of the answers there apply here; however Andrew Stacey's answer which argues that infinite-dimensional constructions are usually not strictly necessary, is relevant.
Edit: Your favourite finite-dimensional result proved by infinite-dimensional means answers this question only if you can explain to me why I should not expect a finite-dimensional proof to exist or to be anywhere near as "good".
 A: Serre and Cartan wrote a Comptes Rendus note Un Théorème de finitude concernant les variétés analytiques compactes where they proved that all cohomology complex vector spaces $H^q(X,\mathcal F)$ of an arbitrary compact complex manifold $X$ are finite-dimensional. The proof is by studying complexes of Fréchet topological vector spaces $C^q(U,\mathcal F)$ constituted of   Cech cochains,  where the $U$'s are suitable Stein open subsets of $X$.The technical heart of the paper  is a theorem of Laurent Schwartz on completely continous morphisms of Fréchet spaces.
Similarly all of Hodge theory for compact Kähler manifolds consists in statements about finite dimensional cohomology vector spaces obtained through heavy recourse to functional analysis (on infinite dimensional spaces, naturally) : Sobolev spaces, pseudodifferential operators, etc.
A: There are certain results about representation spaces of surface groups that I only know how to prove using Yang-Mills theory, i.e. by studying the infinite-dimensional space of connections (or rather a Sobolev space completion thereof) on a principal bundle.  In particular, one can compute the homotopy groups of the real algebraic varieties Hom$(\pi_1 M^g, U(n))$ through a range (roughly the stable range for $\pi_* U(n)$) by identifying this space with the space of flat connections on $M\times U(n)$ modulo based gauge equivalence.  Yang-Mills theory (in particular, work of Atiyah-Bott, Uhlenbeck, Daskalopoulos, and Rade) can be used to show that the space of flat connections is highly connected. Roughly speaking, it's the minimum critical set for the Yang-Mills functional, and the other critical sets have high Morse index.  This means the the space of flat connections modulo based gauge equivalence is reasonably close to the classifying space of the gauge group.  The latter is (a component of) Map$_* (M^g, BU(n))$, whose homotopy groups are computable in a range of dimensions.  
I suppose there could be some finite-dimensional approach to these results, but I'm not aware of one.  (I should say that Hom$(\pi_1 M^g, U(n))$ is connected, and this does have a finite-dimensional proof due to Nan-Kuo Ho and C.-C. Melissa Liu, using some Lie theory and facts about quasi-Hamiltonian moment maps.)
A: I suspect that the true answer is "No", there isn't a truly finite dimensional result that can't be proved using only finite dimensional means.  One reason for thinking that is that (naturally) the first thing that springs to mind is using path spaces, but a result about path spaces can often be reduced to one about finite dimensional objects just by looking at it differently using the adjunction $C^\infty(X, P M) \cong C^\infty(X \times \mathbb{R}, M)$.
So I'm going to take the easier route and try to answer your second question (though, as I say, I don't actually know the answer to the first and would love to hear from, say, Bob Palais on that).
I've just re-read my answer in the linked text and think that actually there is a small thread there that could be the germ of an answer here.  The point I made there was that a result for a specific finite dimensional manifold many only take finite dimensions but that a result for all finite dimensional manifolds will need infinite dimensions.  Here's my offering: (as you well know) K-theory is 2-periodic.  That is, for every finite dimensional manifold (or CW complex) $\tilde{K}^\star(X) \cong \tilde{K}^{\star+2}(X)$.  Now there are lots of ways to prove this, but one that I particularly like is to show that the loop group $\Omega U$ is homotopy equivalent to $\mathbb{Z} \times B U$.  This is most definitely infinite dimensional since both of those are infinite dimensional thingies.  About the only proof of that which I feel that I actually understand a bit of is the proof given in Pressley and Segal's book where the crucial step is to show that the finite energy Grassmannian is homotopy equivalent to the smooth Grassmannian (done by a cell complex argument).  One of the lovely things about this argument is that it easily generalises to other Lie groups and shows how to relate the Grassmannia to the loop groups.
Anyway, that's the first thing that springs to mind.  As I said in the other thread, I'm probably not the right person to answer this question as I just work in infinite dimensions, I don't deal so much in the finite stuff (at least, not so much).
A: Here is a problem in convex geometry. Qualitatively it asks:  If a finite dimensional normed space has the property that an arbitrary subspace is approximately Euclidean after throwing away a small number of dimensions, must the space itself be approximately Euclidean?
Here is the question:
Fix a constant $C>1$; let's use $C=10$.  Suppose that $B$ is a convex symmetric body in $\mathbb{R}^n$ such that for every subspace $F_1$ of $\mathbb{R}^n$ there is a subspace $F$ of $F_1$ of codimension at most $\log \log \dim F_1$ in $F_1$ and a centrally symmetric ellipsoid $E$ in $F$ with $E\subset B\cap F \subset 10 E$. The question is whether there is a constant $\gamma$, independent of everything except the constant $C=10$, so that there is an ellipsoid $E \subset \mathbb{R}^n$ with $E\subset B \subset \gamma E$.
Can you answer this question using only finite dimensional considerations?  AFAIK, the only answers use infinite dimensional tools. 
A: In his famous proof of the Poincare conjecture, Perelman heuristically derived a key monotonicity formula for finite-dimensional Ricci flow, by interpreting this flow as a renormalised version of an infinite-dimensional Ricci-flat manifold.  However, he then gave a separate, and rigorous, proof of this monotonicity that avoided any infinite-dimensional analysis (though it was certainly lengthier and more tedious than the heuristic infinite-dimensional proof).  See my lecture notes at
http://terrytao.wordpress.com/2008/04/27/285g-lecture-9-comparison-geometry-the-high-dimensional-limit-and-perelman-reduced-volume/
EDIT: As noted elsewhere, it is usually the case that a finitary result that is provable by infinitary means, can also be proven by finitary means, and Perelman's monotonicity formula is no exception.  However, what I find striking about this example is that we know of no plausible route by which Perelman (or anyone else) could have discovered the formula without first using the infinite-dimensional Ricci-flat conceptual framework.  This, to me, is where the bulk of the value of infinitary mathematics resides; not necessarily in being able to prove things that weren't provable finitarily, or even to give proofs that are shorter than their finitary counterparts (though they can certainly do this), but in providing clean and powerful conceptual frameworks in order to discover what the right things to prove are in the first place.
A: Any compact Lie group admits an embedding into a large linear group $GL_n (\mathbb{C})$.
I think it is no question that this is a genuinely finite-dimensional and important statement. The proof is via the Peter-Weyl theorem; essentially one has to show that there are enough finite-dimensional representations. How is this done? There is an obvious faithful representation on the Hilbert space $L^2 (G)$. One constructs a compact, $G$-equivariant self-adjoint and injective operator $F$ on $L^2 (G)$. By the spectral theorem, the sum of the eigenspaces of $F$ is dense in $L^2 (G)$, and they are finite-dimensional, so here is a load of finite-dimensional representations! Of course the completeness of the Hilbert space is crucial. The curious thing is that the role of the Hilbert space theory is to cut down infinite dimensional things down to finite dimensions.
The appearance of infinite-dimensional spaces in complex geometry (see Georges answer), Hodge theory, elliptic PDE etc. has of course a similar flavour.
On the other hand, it seems that in algebraic topology, most infinite-dimensional spaces can be kicked out by finite-dimensional approximation, of course at the price of making arguments more cumbersome. The algebraic topologist's infinite dimensional spaces are of the $\mathbb{R}^{\infty}$-type, not of the $\ell^2$-type. Completeness does not play a big role in algebraic topology.
A: In defining his finiteness obstruction (for a finite dimensional finitely dominated CW-complex to be homotopy finite), Wall amends the given finite-dimensional complex by a homotopy equivalence so as to make it have finite skeleta, by the price of making it infinite dimensional.
If I remember it rightly, Ranicki's "instant finiteness obstruction" avoids explicit infinite-dimensional complexes by taking a more computational (hence less explanatory?) approach. EDIT: some (but not all) details can be found here.
My own impression was, however, that this whole business of finiteness obstruction is deeply rooted in the Eilenberg swindle ($1=1-1+1-1+1-...=0$) which I somehow could not appreciate as a truly infinite (let alone infinite-dimensional) construction. EDIT: indeed, 
applying each instance of $1-1=0$ is a rather finite process and then we are just running its independent identical copies.
So this "answer" ends up being a question: what is Wall's finiteness obstruction - is it a perfect application of infinite-dimensional topology to finite-dimensional topology, or on the contrary a perfect example of how such apparent applications turn out to be illusory? I'm asking this in part as an attempt to clarify the meaning of the original question, which I still don't fully understand. If the original very general question is unambiguous, then surely this very specific question has an unabmiguous answer, right?
A: This one is analogous to an Ramras' answer: Donaldson's theorem from the 80s and the corresponding Seiberg-Witten stuff.
A: Douady's prooof that there exists a space parametrizing all compact analytic subspaces
of a given analytic space uses infinite dimensional analytic spaces.
(This space is the analogue for analytic spaces of Grothendieck's Hilbert scheme,
and is now referred to as the Douady space. )
So Douady first proves that the Douady space exists as a Banach-manifold, and then shows
that this space is in fact finitely dimensional.
See: Le problème des modules pour les sous-espaces analytiques compacts d'un espace analytique donné. Annales de l'institut Fourier, 16 no. 1 (1966), p. 1-95
By the way, this paper is very famous for its first lines, whose English translation could read as:

Let $X$ be a complex analytic space.
The goal of this work is to endow his author with the title of Doctor in Mathematical sciences and the set $H(X)$ of all compact analytic subspaces of $X$ with the structure of an analytic space.
To formulate in a more precise way the second problem,...

A: Is it possible to prove the (un)stable manifold theorem for rest points of hyperbolic vector fields without using suitable (infinite dimensional) Banach spaces?
I am only aware of proofs that use certain spaces of curves or sequences which are infinite-dimensional.
