I'm reading Quantum Field Theory and Critical Phenomena, 4th ed., by Zinn-Justin and on page 154 I came across the statement that the functional integral of a functional derivative is zero, i.e. $$\int [d\phi ]\frac{\delta F[\phi]}{\delta\phi^{\alpha}(x)} = 0$$ for any functional $F[\phi ]$.
I would be most thankful if you could provide a mathematical proof for this identity.
If the functional derivative
$$\tag{1} \frac{\delta F[\phi]}{\delta\phi^{\alpha}(x)} $$
exists (wrt. to a certain choice of boundary conditions), it obeys infinitesimally
$$\tag{2}\delta F ~:=~ F[\phi+\delta\phi]- F[\phi] ~=~\int_M \!dx\sum_{\alpha\in J} \frac{\delta F[\phi]}{\delta\phi^{\alpha}(x)}\delta\phi^{\alpha}(x). $$
OP's functional integral formula
$$\tag{3} \int [d\phi ]\frac{\delta F[\phi]}{\delta\phi^{\alpha}(x)} ~=~ 0$$
is really a shorthand for infinitely many integrations
$$\tag{4} \left[\prod_{y\in M,\beta\in J} \int d\phi^{\beta}(y) \right]\frac{\delta F[\phi]}{\delta\phi^{\alpha}(x)} ~=~ 0.$$
Before we can proceed, the functional integral measure in (4) must be given a mathematical definition. The precise definition depends on context and method. Needless to say that a general mathematically rigorous definition of functional integrals is a well-known open problem in mathematics. For instance, one may try to construct the functional integral as an appropriate continuum limit of a discretized space-time $M$, as Michael Brown suggests in a comment.
Let us use DeWitt's condensed notation, where all indices (both continuous and discrete indices) are lumped together as
$$\tag{5} i~=~(\alpha,x)~\in~ I~:=~ J\times M,$$
and fields are written as
$$\tag{6} \phi^i ~:=~ \phi^{\alpha}(x)~,\qquad i~\in~ I.$$
We now discretize space-time $M$. The discretization means that we think of $I$ as a finite index-set. In other words, we now only have finitely many variables $\phi^i$, $i\in I$, in the theory. The functional derivative (1) [times$^1$ the volume $\Delta x$ of a single cell of the discretization] is replaced by a partial derivative
$$\tag{1'} \frac{\partial F[\phi]}{\partial\phi^{i}}. $$
An infinitesimally variation is given by the standard formula from calculus in several variables
$$\tag{2'}\delta F ~:=~ F[\phi+\delta\phi]- F[\phi] ~=~\sum_{i\in I} \frac{\partial F[\phi]}{\partial\phi^{i}}\delta\phi^{i}. $$
Finally, OP's functional integral formula (4) becomes
$$\tag{4'} \left[\prod_{j\in I} \int d\phi^{j} \right] \frac{\partial F[\phi]}{\partial\phi^{i}}~=~ 0.$$
Equation (4') follows from the fact that an integral of a total derivative vanishes if the boundary contributions are zero.
--
$^1$ Concerning dimensions of functional derivatives versus partial derivatives, see also this Phys.SE post.
The expression : $ [d\phi(x)] \frac{\delta F}{\delta \phi(x)}$ could be interpreted as a formal $dF(\phi)$ : $$\int [d\phi(x)] \frac{\delta F}{\delta \phi(x)} \sim \int \frac {\partial F}{\partial \phi_i} d\phi_i \sim \int dF(\phi) =F(+\infty) - F(-\infty)$$
So the left hand side of the expression is zero only for identical boudary conditions, for instance $F(-\infty) = F(+\infty)$
For instance, the function $F(\phi) = e^{- \frac{1}{2}\int dx~\phi^2(x)} =\Pi_x ~(e^{- \frac{1}{2} \phi^2(x)}$), is a valid function, because, at positive and negative infinite $\phi$, we have $F(\phi) = 0$
Your function $F = \int dx ~ C(x) \phi(x)$ is not valid because it takes different values at negative and positive infinite values of $\phi$. Moreover, the values of $F$ are infinite, for infinite $\phi$, so it is difficult to give a sense to $F(-\infty) - F(+\infty)$
I might be misinterpreting what "functional derivative" and "functional integral" here particularly mean but if I recall correctly,
Given a functional
$$ \int_{x_0}^{x_1} L(x,y(x), y'(x), y''(x) ... y^{[n]}(x)) $$
The functional derivative
$$ \frac{\delta L}{\delta y} $$
Is defined such that if $$ \frac{\delta L}{\delta y} = 0 $$
For some y, then there exists a local optima to the aforementioned functional by fitting appropriate boundary conditions on that y.
Derivation of the functional derivative itself requires substitution of
$$y = U + e k(x) $$
where U is the optimal solution, e is a variable (that we will manipulate and should be thought of as infinitesmally small) and k(x) is an arbitrary test function such that $k(x_0) = k(x_1) = 0$
then:
$$ \frac{d}{de} [\int_{x_0}^{x_1} L(x,u(x) + ek(x), ... u^{[n]}(x) + ek^{[n]}(x)) ] $$
Yields (after fidgeting with integration by parts)
$$\int_{x_0}^{x_1} [k(x) \sum_{i=0}^{n} {(-1)^{i} \frac{d^{i}}{dx^{i}}[\frac{\partial L}{\partial y^{[i]}} ]}] = 0$$
Which implies
$$\int_{x_0}^{x_1} [\sum_{i=0}^{n} {(-1)^{i} \frac{d^{i}}{dx^{i}}[\frac{\partial L}{\partial y^{[i]}} ]}] = 0$$
Whereas:
$$\sum_{i=0}^{n} {(-1)^{i} \frac{d^{i}}{dx^{i}} \frac{\partial L}{\partial y^{[i]}} } = \frac{\delta L}{\delta y} $$
The inverse of the functional derivative is a problem in partial differential equations.
Consider for example the one variable, single order derivative case: aka inverting the euler lagrange equations of
$$\frac{\partial L}{\partial y} - \frac{d}{dx}[\frac{\partial L}{\partial y'}] = H $$
for some functional H(x,y,y'). We can expand the total derivative with respect to x (Assuming our arguments are only x, y,y' to find:
$$\frac{\partial L}{\partial y} - \frac{\partial^2 L}{\partial x y'} - y'\frac{\partial^2 L}{\partial y y'} - y''\frac{\partial^2 L}{\partial (y')^2} = H$$
These can be quite challenging for general H (i'm not even sure if solutions exist for general H). But if $$\frac{\partial^2 H}{\partial (y'')^2} = 0$$ which WILL ALWAYS BE THE CASE if H = $\frac{\delta L}{\delta y} $ for any well defined $L(x,y,y')$. In this case follow the procedure below:
$$ H = u(x,y,y') + y''w(x,y,y') $$
such that
$$ \frac{\partial u}{\partial y''} = 0 $$
and
$$ \frac{\partial w}{\partial y''} = 0 $$
Then it is trivial to showL
$$L = \int \int [w] \partial y'' \partial y'' + y'a_1(x,y) + a_2(x,y)$$
Now take the truncated euler lagrange equation and substitute $\int \int [w] \partial y'' \partial y'' + y'a_1(x,y) + a_2(x,y)$ for $L$ in:
$$\frac{\partial L}{\partial y} - \frac{\partial^2 L}{\partial x y'} - y'\frac{\partial^2 L}{\partial y y'} = u$$
To ultimately derive an expression for $a_2$ in terms of $a_1$, substituting this back into your original definition we conclude that in general the inverse of the functional derivative for a functional H (ie the functional integral of H(x,y,y')) is:
$$ \int H \delta y = y' a_1(x,y) + \int{[u + \int \int [\frac{\partial w}{\partial y}] \partial (y')^2 + \frac{\partial a_1}{\partial x} - \int [\frac{\partial w}{\partial x} + \frac{\partial w}{\partial y}] \partial y'} \partial y + (1 - y')a_1(x,y) + g(x) - \int \int [w] \partial (y')^2 $$
for arbitrary functions of their arguments: $a_1(x,y)$ and $g(x)$
This is certainly not equal to 0. It is also definitely not simplified either. But I suppose if that was soo important you could manage it.
Additional notes,
This is just the case for functionals over (x,y,y') for higher order functionals ex: (x,y,y,y', y'', y''' ....) the functional integral is significantly more complex.
Good luck!
The integration variable in the functional integral is a dummy variable and can be replaced by one that differs by an infinitesimal function (epsilon). The functional measure does not change by that. Then develop the functional (F) to first order in epsilon. The non-epsilon parts cancel. The next step is to take the local epsilons outside the functional integral. And because these local epsilons are arbitrary, we are left with the result that the functional integral of the functional derivative of F is zero.
