Want to prove an inequality

Iosif's answer is very interesting and if anyone knows how to do the same thing in Maple I'd like to know.

However I disagree with Iosif about the difficulty. Mathematica will use a systematic procedure that is guaranteed to work in a wide variety of cases, and that may take many more steps than an ad hoc method devised by a human.

So here is a quick proof. Remove the upper bounds on $q$, $x$, $y$ by substituting $x=(1-q)X/(1+X)$, $y=qY/(1+Y)$, $q=Q/(1+Q)$. After clearing demoninators that are obviously positive, we have to prove $\Phi\ge 0$ subject to $Q,X,Y\ge 0$ and conditions $C_1$ and $C_2$, where $$\begin{align}\Phi &= -Y^2(1+X)^3 Q^4 + XY(1+X)^2(Y+2)Q^3\\ &{\quad}+ 2XY(1+Y)(1+X)(X+Y+3)Q^2 + XY(1+Y)^2(X+2)Q - X^2(1+Y)^3\end{align}$$ and $C_1$, $C_2$ come from the OP's last condition. They can be arranged like this: \begin{align*} C_1:\qquad & YQ \ge \frac{(1+Y)X}{(X+2)}-\frac{Y(2Y+3)(1+X)}{(1+Y)(X+2)}Q^2. \\ C_2:\qquad & YQ^2 \le \frac{X(1+Y)(2X+3)}{(1+X)^2}+\frac{(Y+2)X}{(1+X)}Q. \end{align*}

Now apply $C_1$ to the linear term of $\Phi$ and apply $C_2$ to the quartic term in the manner $YQ^4 \le \operatorname{rhs}(C_2)\,Q^2$. The result is exactly 0.

To show that $\Phi\gt 0$ strictly when $x,y,q\gt 0$, note that zero can only happen if $C_1,C_2$ hold with equality at the same time. But $Q\operatorname{rhs}(C_1)-\operatorname{rhs}(C_2)$ is manifestly negative.


Welcome to MO! However, your conjecture is false e.g. for $q = 1/2$, $x= 3/8$, $y = 1/4$, $t= 0$.

Added: The OP later stated that the additional condition $t=3$ was initially omitted in the OP's post. Anyhow, the problem is one of real algebraic geometry and, as such, admits a completely algorithmic solution. In Mathematica, such algorithms are represented by Reduce[] and related commands. Using Reduce[] indeed, we get

enter image description here

This proves the conjecture. We see that it took Mathematica about 2 sec to obtain this result; so, a manual proof might be quite long and laborious, and most likely less reliable than Mathematica's.

Tags:

Inequalities