Noether second theorem calculus of variation formalization Noether's first theorem as a statement about the action of a finite dimensional lie group $ G_{\rho} $ dependent upon $\rho $ parameters $  \varepsilon_{i}$ with $i = 1, \dots, \rho $; can be formalized in a proper functional space with the Gateaux Derivative formalism as the action of the lie group/lie algebra can be represented by a set of parameters:
$$\tag{1} \phi^{'\alpha}_{\varepsilon}~=~ F^{\alpha}(\varepsilon , \phi^{\alpha})
\approx \phi^{\alpha} + F^{\alpha,\mu} \varepsilon $$
Where I omitted the index $ i$ on the parameters. Now the invariance of an action functional $S$ implies the invariance of its variation. My concern is in formalizing the concept of variation $\delta S $. I only know that in some functional space, the Gateaux Derivative is well defined and so I can put:
$$\tag{2} \delta S = \frac{d}{d \varepsilon}|_{\varepsilon = 0} ~~S[ \phi^{'\alpha}_{\varepsilon}] $$
where the variation is to be done with respect to each parameter if I have more than one.
Now in Noether's second theorem if I have an infinite dimensional Lie Group/Algebra $ G^{\infty}_{\rho} $ dependent upon $\rho $ functions $  p_{i}(x)$ with $i = 1, \dots, \rho $  I have the following transformation:
$$\tag{3} \phi^{'\alpha}_{p}~=~ F^{\alpha}(\phi^{\alpha}(x) , p_{i}(x), p^{(1)}_{i}(x), \dots, p^{(N)}_{i}(x) ) $$
where we can have the dependence on the parameters and their derivatives up to order $N$.
For simplicity we can consider no dependence upon the derivatives of the parameters.
My question is how can I use a similar formalism such as Gateaux derivative to formalize the notion of variation of the action $ \delta S $ ? Where can I find some reference where the proof of the theorems are formalized in the language of functional analysis?
 A: There are a number of different approaches one can find to the calculus of variations, so here I will only mention the approach which make the most sense to me, which goes by the name "covariant phase space." The idea is to call the space of classical solutions to the equations of motion the phase space (up to subtleties involving gauge transformations and a symplectic quotient) and assume that this space has a manifold structure. I know that sounds a little strange, but it works out really well. Essentially, one can formalize things in terms of jet bundles, but the end result insofar as I have ever found is that the end result of the jet bundle formalism is to tell us that it's okay to think about the space of solutions as having a manifold structure.
Describing this approach would, I think, be too much for a post here, but let me share some references which I found particularly helpful thinking about these things.

*

*First and foremost, though it has nothing to do with the formalism I am thinking about here, I absolutely suggest going and reading Emmy Noether's original paper. It's not too long (about ~20 pages) and an absolute pleasure to read. Her writing was exceptionally clear and extremely general. There's an English translation on the arXiv as well.


*This paper (the pdf is there too) by Crnkovic and Witten in 1986 contains a very nice description of this formalism along with some worked examples, though the language is not as modern as one might want these days.


*These lecture notes by Compere and Fiorucci can also be helpful. They give some light reference to the jet space formalism that I mentioned and also explicitly discuss the consequences of Noether's second theorem as it pertains to gauge transformations in this formalism. Their focus is mostly on diffeomorphisms, but that's to be expected in some GR lectures.


*This paper by Harlow and Wu again focuses mainly upon diffeomorphisms, but has a chapter at the end on more general symmetries. I think the notation in this paper is the easiest to follow if you're comfortable working with differentials and Lie derivatives in coordinate-independent notation. They also work a number of examples and have a fairly nice description of the symplectic quotienting procedure I mentioned earlier.


*If you want something more formal on this last point in particular, there is this paper (pdf not freely available as far as I know) by Lee and Wald. It discusses a number of points a little more formally than some of the other sources I've listed (the notation is also heavier) and also does some examples. The thing I remember most from it though is the description of how we mod out the gauge transformations. They are much more careful about how they describe this than Harlow and Wu are (it wasn't a main focus there, so it's understandable).
Anyway, these are things I found helpful, and hopefully you will find them helpful as well.
