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?
