The following "piecewise-quadratic" inequality emerged in a joint work of Rom Pinchasi and myself. The inequality is surprisingly delicate, and all our attempts to simplify it made it false. By the end of the day, we were able to prove the inequality, but the proof is unreasonably sophisticated, totalling to about 15 pages. We would be happy to have a shorter proof.

The inequality involves the function $G$ of three real variables, defined as
follows: if $(\xi,\eta,\zeta)$ is a non-decreasing rearrangement of
$(x,y,z)$, then we let
$$ G(x,y,z) := \begin{cases}
\xi\eta &\ \text{if}\ \zeta\ge \xi+\eta, \\
\xi\eta-\frac14\,(\xi+\eta-\zeta)^2 &\ \text{if}\ \zeta\le \xi+\eta.
\end{cases} $$
Thus, for instance, we have $G(9,6,7)=38$, whereas $G(7,14,6)=42$. Now
consider the function $f$ of four variables defined by
$$\begin{align*}
f(x_0,x_1,y_0,y_1)
&:= \min \{ 0.15s^2, x_0y_0+x_1y_1 \} \\
&\qquad + G(x_0,y_1,1-s) + G(x_1,y_0,1-s) \\
&\qquad + 0.25(1-s)^2,
\end{align*}$$
where for brevity I write $s=x_0+x_1+y_0+y_1$, and let
$$ \Omega := \{ (x_0,x_1,y_0,y_1)\in{\mathbb R}_{\ge 0}^4\colon 1/2 \le s \le 1. \}. $$
All we want to show is that
$$ \max_\Omega f \le 0.15. $$
(Indeed, the maximum is actually *equal* to $0.15$: say, we have
$f(0.5,0,0.5,0)=0.15$.)

At Pat Devlin's suggestion, here is the graph of the maximum as a function of the sum $s=x_0+x_1+y_0+y_1$.

It looks nice, but does not seem to be a graph of some "simple" function; and so, there is probably no simple analytic expression for $\max f$ over all quadruples $(x_0,x_1,y_0,y_1)$ adding up to $s$.

anyinequality there is always a stronger inequality (as for any non-negative functions there is a smaller non-negative function); the problem is to find a stronger inequality whichiseasier to prove. In our case, replacing $0.25(1-s)^2$ with $(s/4)(1-s)^2$ actually leads to aweakerinequality. – Seva Oct 1 '12 at 20:32