Note: I am asking this here over math.se or mathoverflow because functional derivatives are very much a physics-only thing.
It seems to be a common assumption that second functional derivatives commute (see for example https://physics.stackexchange.com/a/82247/68410).
Indeed, part of the reason why I am asking this question is because the functional derivative miraculously corresponds to a sequence of differentials on the variational bicomplex that are otherwise fairly complicated algebraically to construct and the commutativity of functional derivatives is crucial in this.
To give an example, if $S[\phi]=\int L(x,\phi(x),...,\phi^{(r)}(x))d^nx$ is an action functional, then $$ \frac{\delta S}{\delta\phi^\kappa(x)}[\phi]=E_\kappa(L)[\phi](x) $$ is the Euler-Lagrange operator, and while to explicitly calculate the functional derivative one must still go through the pains of doing a bunch of integrations by parts, but nontheless this operation formally constructs the Euler-Lagrange form.
To go further, if $\varepsilon_\kappa[\phi](x)$ is a "source form" (using terminology common in the variational geometry literature), then the bivariate "expression" (which in the ordinary case is can be interpreted as a bivariate distribution at best) $$ H_{\kappa\lambda}(\varepsilon)[\phi](x,x^\prime)=\frac{\delta \varepsilon_\kappa[\phi](x)}{\delta\phi^\lambda(x^\prime)}-\frac{\delta\varepsilon_\lambda[\phi](x^\prime)}{\delta\phi^\kappa(x)} $$is essentially equivalent to the standard "Helmholtz expressions" $$ H^I_{\kappa\lambda}(\varepsilon)[\phi]=\frac{\partial\varepsilon_\kappa}{\partial\phi^\lambda_I}[\phi]-(-1)^{|I|}E^I_\kappa(\varepsilon_\lambda)[\phi], $$ where $I=(i_1,...,i_s)$ ($0\le s\le r$) is a multiindex and $E^I_\kappa$ are the "higher Euler operators" $$ E^I_\kappa(f)=\sum_{|J|=0}^{r-|I|}\left(\begin{matrix} |I|+J| \\ |I|\end{matrix}\right)(-1)^{|J|}D_J\frac{\partial^Sf}{\partial y^\kappa_{IJ}}, $$ with $D_J=D_{j_1}...D_{j_s}$ being repeated total differentiation and $\partial^S/\partial y^\kappa_{I}$ is an appropriately normalized derivative.
That is, the expression $H_{\kappa\lambda}(\varepsilon)(x,x^\prime)$ vanishes if and only if the $\varepsilon_\kappa$ are the Euler-Lagrange expressions of some Lagrangian, with the if part following from the symmetry of the functional derivatives and the only if part from adapting the usual proof of Poincaré's lemma to the functional case and producing the Vainberg-Tonti Lagrangian/action $$ S_\varepsilon[\phi]=\int d^n x\int_0^1\varepsilon_\kappa[s\phi]\phi^\kappa ds $$basically for free, while otherwise one would either need considerable algebraic intuition, studying the total divergence equation or developing the formal properties of the variational bicomplex to get this result.
Which basically brings me to my question. All these results rely crucially on the commutativity of functional derivatives. Now on the special cases of
- "action" functionals that arise as the integral of a finite order Lagrangian;
- formal multivariate distributions whose coefficients are finite order local functionals (like $E_\kappa(L)[\phi](x)$ or $H_{\kappa\lambda}(\varepsilon)[\phi](x,x^\prime)$);
the functional derivative can be interpreted sensibly, however then commutativity is not a natural property but one may establish commutativity by for example manually checking that for any "action" functional $S[\phi]=\int d^nx L(x,\phi(x),...)$ it is true that $$ \frac{\delta^2 S}{\delta\phi^\kappa(x)\delta\phi^\lambda(x^\prime)}=\{(\kappa,x)\leftrightarrow (\lambda,x^\prime)\}, $$but checking this manually is essentially equivalent to the same set of rather complicated algebraic manipulations that would give for example the explicit form of the Helmholtz expressions $ H^I_{\kappa\lambda} $, and in the higher order case it would be even more complicated.
Otherwise the functional derivative doesn't really have a proper mathematical definition, because $$ \frac{\delta F[\phi]}{\delta\phi^\kappa(x)}=\frac{d}{ds}F[\phi+e_\kappa\delta_x]|_{s=0} $$ is not really a definition. It is at best a heuristic rule that defines the functional derivative in the sense that the functional derivative is this expression whenever it is possible to make some sense of the resulting expression.
The other definition $$ \delta F[\phi]=\int d^n x \frac{\delta F[\phi]}{\delta\phi^\kappa(x)}\delta\phi^\kappa(x) $$ for all variations with compact support isn't exactly helpful either, at least I don't see how commutativity of functional derivatives follow from this (any more than Clairut's theorme directly following from $df=\sum_i\frac{\partial f}{\partial i}dx^i$, which it does not).
And as far as I know, Clairaut's theorem (the corresponding symmetry result for ordinary partial derivatives) has a rather nontrivial proof that relies crucially on the continuity of certain derivatives, but since the functional derivative is not really well-defined, I don't how to say whether a functional is "functionally $C^2$ or whatever.
So collecting:
Assuming commutativity of functional derivatives, it reproduces all the vertical differentials in the Euler-Lagrange complex.
Knowing the vertical part of the Euler-Lagrange complex essentially implies that the functional derivative is symmetric when applied to finite order functionals.
On the other hand as far as I am aware, in physics-based texts the functional derivative is heavily applied in a "nonlocal" context as well, for example in the covariant phase space formalism or generally to construct algebras of observers in filed theory ("action" type functionals do not form an algebra), and the commutativity of functional derivatives is assumed in this case.
Question: What is a/the justification for saying "functional derivatives commute" in a general - including nonlocal - context? Is there any way to at least formally prove a Clairaut-type result which does not suppose that the functional we are differentiating is somewhat special, like finite order? I do not expect a rigorous proof because the functional derivative itself is not rigorous, but I would assume there is at least some highly formal way to justify this.
