I came across an inequality the other day, and I assume that it is either a special case of something well known or else something from a math contest. In an effort to write out this post, I came up with a proof, but I would ideally like something cleaner (that doesn't involve operators on Hilbert spaces to come up with), or which follows from standard inequalities.
Let $f(x,y)$ be a continuous, real valued function on $[0,1]^2$. Prove
$$\int_0^1\int_0^1 \left(f(x,y)\right)^2 dxdy + \left(\int_0^1\int_0^1 f(x,y) dxdy\right)^2\geq \int_0^1\left(\int_0^1 f(x,y) dx)\right)^2 dy+\int_0^1\left(\int_0^1 f(x,y) dy)\right)^2 dx.$$
My first thought was that this could be handled by iterated Cauchy-Schwarz, but I was unable to make things work directly. In an effort to provide structure to the problem, I defined the standard inner product $\langle f,g\rangle = \int_{[0,1]^2} fg\, dxdy$, and I defined projection operators $E_x$ and $E_y$ defined by $E_x(f)(t,y)=\int_0^1 f(x,y) dx$ (and similarly for $E_y$), and verified that the operators are self adjoint, idempotent, and commute (which is just Fubini's theorem).
One can then rewrite the inequality in the following form:
$$\langle f,f \rangle + \langle E_x(f),E_y(f) \rangle \geq \langle E_x(f), E_x(f) \rangle +\langle E_y(f), E_y(f) \rangle,$$
which can be further rewritten as
$$\langle f-E_x(f),f-E_y(f) \rangle \geq 0$$.
Let $S=I-E_x, T=I-E_y$. Because $E_x$ and $E_y$ are commutative, self adjoint, and idempotent, so are $S$ and $T$. Then
$$\langle Sf, Tf \rangle = \langle S^2 f, T^2 f \rangle = \langle Sf, ST^2f \rangle = \langle Sf, T(ST)f \rangle = \langle (ST)f, (ST)f \rangle.$$
Translating all this back into functions and integrals, this suggests the simple but unmotivated proof of simplifying $$\iint_{[0,1]^2}\left(f-\int_0^1 fdx-\int_0^1 fdy+\iint_{[0,1]^2} fdxdy\right)^2\geq 0.$$
Is there a proof that is either simpler than talking about commuting orthogonal projections or less mysterious than saying "If you square and integrate this auxiliary function, it simplifies to what you want"? Also, is the result that $\langle Pv,Qv \rangle \geq 0$ when $P,Q$ are commuting orthogonal projections well known? It's trivial to prove, but I've never seen it before.