Context: I am a PhD student in theoretical physics with higher-than-average education on differential geometry. I am trying to understand Lagrangian and Hamiltonian field theories and related concepts like Noether's theorem etc. in a mathematically rigorous way since the standard physics literature is sorely lacking for someone who values precision and generality, in my opinion.
I am currently studying various text by Anderson, Olver, Krupka, Sardanashvili etc. on the variational bicomplex and on the formulation of Lagrangian systems on jet bundles. I do not rule the formalism yet, but made significant steps towards understanding.
On the other hand, most physics literature employs the functional formalism, where rather than calculus on variations taking place on finite dimensional jet bundles (or the "mildly infinite dimensional" $\infty$-jet bundle), it takes place on the suitably chosen (and usually not actually explicitly chosen) infinite dimensional space of smooth sections (of the given configuration bundle).
Even relatively precise physics authors like Wald, DeWitt or Witten (lots of 'W's here) seems to prefer this approach (I am referring to various papers on the so-called "covariant phase space formulation", which is a functional and infinite dimensional but manifestly "covariant" approach to Hamiltonian dynamics, which also seems to be a focus of DeWitts "The Global Approach to Quantum Field Theory", which is a book I'd like to read through but I find it impenetrable yet).
I find it difficult to arrive at a common ground between the functional formalism and the jet-based formalism. I also do not know if the functional approach had been developed to any modern standard of mathematical rigour, or the variational bicomplex-based approach has been developed precisely to avoid the usual infinite dimensional troubles.
Example:
Here is an image from Anderson's "The Variational Bicomplex", which shows the so-called augmented variational bicomplex. Here $I$ is the so-called interior Euler operator, which seems to be a substitute for integration by parts in he functional approach.
Later on, Anderson proves that the vertical columns are locally exact, and the augmented horizontal rows (sorry for picture linking, xypic doesn't seem to be working here, don't know how to draw complices)
are locally exact as well. In fact for the homotopy operator $\mathcal H^1:\mathcal F^1\rightarrow\Omega^{n,0}$ that reconstructs Lagrangians from "source forms" (equations of motion) he gives (for source form $\Delta=P_a[x,y]\theta^a\wedge\mathrm d^nx$) $$ \mathcal H^1(\Delta)=\int_0^1 P_a[x,tu]u^a\mathrm dt\ \mathrm d^nx. $$
On the other hand, if we use the functional formalism in an unrigorous manner, the functional derivative $$ S\mapsto\frac{\delta S[\phi]}{\delta \phi^a(x)} $$ behaves like the infinite dimensional analogue of the ordinary partial derivative, so using the local form of the homotopy operator for the de Rham complex (which for the lowest degree is $f:=H(\omega)=\int_0^1\omega_\mu(tx)x^\mu\mathrm dt$) and extending it "functionally", one can arrive at the fact that if an "equation of motion" $E_a(x)[\phi]$ satisfies $\frac{\delta E_a(x)}{\delta\phi^b(y)}-\frac{\delta E_b(y)}{\delta\phi^a(x)}=0$, then $E_a(x)[\phi]$ will be the functional derivative of the action functional $$ S[\phi]=\int_0^1\mathrm dt\int\mathrm d^nx\ E_a(x)[t\phi]\phi^a(x). $$
I have (re)discovered this formula on my own by simply abusing the finite dimensional analogy and was actually surprised that this works, but it does agree (up to evaluation on a secton and integration) with the homotopy formula given in Anderson.
This makes me think that the "variation" $\delta$ can be considered to be a kind of exterior derivative on the formal infinite dimensional space $\mathcal F$ of all (suitable) field configurations, and the Lagrangian inverse problem can be stated in terms of the de Rham cohomology of this infinite dimensional field space.
This approach however fails to take into account boundary terms, since it works only if integration by parts can be performed with reckless abandon and all resulting boundary terms can be thrown away. This can be also seen that if we consider the variational bicomplex above, the $\delta$ variation in the functional formalism corresponds to the $\mathrm d_V$ vertical differential, but in the augmented horizontal complex, the $\delta_V=I\circ\mathrm d_V$ appears, which has the effect of performing integrations by parts, and the first variation formula is actually $$ \mathrm d_V L=E(L)-\mathrm d_H\Theta, $$ where the boundary term appears explicitly in the form of the horizontally exact term.
The functional formalism on the other hand requires integrals everywhere and boundary terms to be thrown aside for $\delta$ to behave as an exterior derivative. Moreover, integrals of different dimensionalities (eg. integrals over spacetime and integrals over a hypersurface etc.) tend to appear sometimes in the functional formalism, which can only be treated using the same concept of functional derivative if various delta functions are introduced, which makes me think that de Rham currents (I am mostly unfamiliar with this area of mathematics) are also involved here.
Question: I would like to ask for references to papers/and or textbooks that develop the functional formalism in a general and mathematically precise manner (if any such exist) and also (hopefully) that compare meaningfully the functional formalism to the jet-based formalism.