How to prove an inequality or read Mathematica's proof

Question

Given $0 < \alpha_1, \alpha_2 <1$ and $1/2 < p <1$, how to prove that the following expression is always non-negative? \begin{align*} (1 - \alpha_2)^2 p^2 (2 p -1) + \alpha_1^2 \, p\, \left(2 \alpha_2^2 \,(1 - p)^2 + p (2 p - 1) + \alpha_2 (-1 + 5 p - 4 p^2) \right) + \alpha_1 \left(-2 p^2\, (2 p - 1) + \alpha_2^2\, p \,(-1 + 5 p - 4 p^2) + \alpha_2 (1 - 7 p^2 + 8 p^3) \right) \geq 0 \end{align*}

It's easy to see that there is only one term, $-2 p^2 \alpha_1 (2p-1) $, that will be negative in this expression. I have tested this inequality using Mathematica's Reduce function and also by brute forcing using a small Java program. However, I still don't know of a rigorous proof. The inequality arose when I was trying to design a primal-dual approximation algorithm for a graph matching problem.

Also, is there a way I can get Mathematica's proof (that uses the Reduce function) for this inequality in a human understandable format?

Answer 1

First, we determine whether the function has a minimum in the allowed region via the first derivative.

Simplify[
  D[(1 - α2)^2 p^2 (2 p - 1) + 
          α1^2 p (2 α2^2 (1 - p)^2 + p (2 p - 1) + α2 (-1 + 5 p - 4 p^2)) +
          α1 (-2 p^2 (2 p - 1) + α2^2 p (-1 + 5 p - 4 p^2) + α2 (1 - 7 p^2 + 8 p^3)), 
  #] & /@ {α1, α2, p}
]

(*  {4 p^3 (-1 + α1) (-1 + α2)^2 + α2 + p α2 (-α2 + α1 (-2 + 4 α2)) - p^2 (-1 + α2) (2 - 5 α2 + α1 (-2 + 8 α2)), 
 α1 + 4 p^3 (-1 + α1)^2 (-1 + α2) + p α1 (-2 α2 + α1 (-1 + 4 α2)) - p^2 (-1 + α1) (2 - 2 α2 + α1 (-5 + 8 α2)), 
 6 p^2 (-1 + α1)^2 (-1 + α2)^2 + α1 α2 (-α2 + α1 (-1 + 2 α2)) - 2 p (-1 + α1) (-1 + α2) (1 - α2 + α1 (-1 + 4 α2))}  *)

Simplify[ 
  Reduce[{
    f == (1 - α2)^2 p^2 (2 p - 1) + 
          α1^2 p (2 α2^2 (1 - p)^2 + p (2 p - 1) + α2 (-1 + 5 p - 4 p^2)) +
          α1 (-2 p^2 (2 p - 1) + α2^2 p (-1 + 5 p - 4 p^2) + α2 (1 - 7 p^2 + 8 p^3)),
    Simplify[
      D[(1 - α2)^2 p^2 (2 p - 1) + 
          α1^2 p (2 α2^2 (1 - p)^2 + p (2 p - 1) + α2 (-1 + 5 p - 4 p^2)) +
          α1 (-2 p^2 (2 p - 1) + α2^2 p (-1 + 5 p - 4 p^2) + α2 (1 - 7 p^2 + 8 p^3)), 
        #] & /@ {α1, α2, p}
    ] == 0,
    0 < α1 < 1, 
    0 < α2 < 1, 
    1/2 < p < 1}, 
    {f}, 
    Reals, 
    Backsubstitution -> True],
  TransformationFunctions -> {Automatic, RootReduce}]

(*  α2 == Root[2 + 4 #1 - 28 #1^2 + 6 #1^3 - 15 #1^4 + 8 #1^5 &, 2] && 
    p + Root[1 + 7 #1 + 34 #1^2 + 94 #1^3 + 97 #1^4 + 23 #1^5 &, 2] == 0 && 
    α1 == Root[2 + 4 #1 - 28 #1^2 + 6 #1^3 - 15 #1^4 + 8 #1^5 &, 2] && 
    f == Root[-11 + 20 #1 + 5182 #1^2 + 10580 #1^3 + 7605 #1^4 + 
 512 #1^5 &, 3]
*)

N[%]

(*  α2 == 0.352859 && -0.707063 + p == 0. && α1 == 0.352859 && f == 0.0424094
*)

So the function has exactly one local minimum in the allowed region, but that minimum is positive. There may yet be a minimum on the boundary of the region. (The derivatives of the function don't know anything about our region...) There are two ways forward:

Minimize[{
  (1 - α2)^2 p^2 (2 p - 1) + 
   α1^2 p (2 α2^2 (1 - p)^2 + p (2 p - 1) + α2 (-1 + 5 p - 4 p^2)) +
   α1 (-2 p^2 (2 p - 1) + α2^2 p (-1 + 5 p - 4 p^2) + α2 (1 - 7 p^2 + 8 p^3)), 
   0 < α1 < 1, 0 < α2 < 1, 1/2 < p < 1}, 
  {α1, α2, p}]

Minimize::wksol: Warning: there is no minimum in the region in which the objective function is defined and the constraints are satisfied; returning a result on the boundary.

{0, {α1 -> 0, α2 -> 0, p -> 1/2}}

and explicitly finding the minima on each chunk of the boundary, finding that most chunks don't have a stationary point.

Outer[{#1,#2,#3,
  Simplify[ 
  Reduce[{
    f == (1 - α2)^2 p^2 (2 p - 1) + 
          α1^2 p (2 α2^2 (1 - p)^2 + p (2 p - 1) + α2 (-1 + 5 p - 4 p^2)) +
          α1 (-2 p^2 (2 p - 1) + α2^2 p (-1 + 5 p - 4 p^2) + α2 (1 - 7 p^2 + 8 p^3)),
    Simplify[
      D[Assuming[{#1,#2,#3},Simplify[
        (1 - α2)^2 p^2 (2 p - 1) + 
          α1^2 p (2 α2^2 (1 - p)^2 + p (2 p - 1) + α2 (-1 + 5 p - 4 p^2)) +
          α1 (-2 p^2 (2 p - 1) + α2^2 p (-1 + 5 p - 4 p^2) + α2 (1 - 7 p^2 + 8 p^3))]], 
        #] & /@ {α1, α2, p}
    ] == 0,
    #1, 
    #2, 
    #3}, 
    {f}, 
    Reals, 
    Backsubstitution -> True],
  TransformationFunctions -> {Automatic, RootReduce}]} &,
  {0 == α1, 0 < α1 < 1, α1 == 1}, 
  {0 == α2, 0 < α2 < 1, α2 == 1}, 
  {1/2 == p, 1/2 < p < 1, p == 1}
]

(*  {{{{0 == α1, 0 == α2, 1/2 == p, α2 == 0 && α1 == 0 && 2 p == 1 && f == 0}, 
       {0 == α1, 0 == α2, 1/2 < p < 1, α1 == 0 && α2 == 0 && ((864 f == 49 && 12 p == 7) || (f + p^2 == 2 p^3 && (1/2 < p < 7/12 || 7/12 < p < 1)))}, 
       {0 == α1, 0 == α2, p == 1, α2 == 0 && α1 == 0 && p == 1 && f == 1}}, 
      {{0 == α1, 0 < α2 < 1, 1/2 == p, 0 < α2 < 1 && α1 == 0 && 2 p == 1 && f == 0}, 
       {0 == α1, 0 < α2 < 1, 1/2 < p < 1, α1 == 0 && 0 < α2 < 1 && ((864 f == 49 (-1 + α2)^2 && 12 p == 7) || (f == p^2 (-1 + 2 p) (-1 + α2)^2 && (1/2 < p < 7/12 || 7/12 < p < 1)))}, 
       {0 == α1, 0 < α2 < 1, p == 1, 0 < α2 < 1 && α1 == 0 && p == 1 && f == (-1 + α2)^2}}, 
      {{0 == α1, α2 == 1, 1/2 == p, α2 == 1 && α1 == 0 && 2 p == 1 && f == 0}, 
       {0 == α1, α2 == 1, 1/2 < p < 1, f == 0 && 1/2 < p < 1 && α1 == 0 && α2 == 1}, 
       {0 == α1, α2 == 1, p == 1, α2 == 1 && α1 == 0 && p == 1 && f == 0}}}, 
     {{{0 < α1 < 1, 0 == α2, 1/2 == p, 0 < α1 < 1 && α2 == 0 && 2 p == 1 && f == 0}, 
       {0 < α1 < 1, 0 == α2, 1/2 < p < 1, α2 == 0 && 0 < α1 < 1 && ((864 f == 49 (-1 + α1)^2 && 12 p == 7) || (f == p^2 (-1 + 2 p) (-1 + α1)^2 && (1/2 < p < 7/12 || 7/12 < p < 1)))}, 
       {0 < α1 < 1, 0 == α2, p == 1, 0 < α1 < 1 && α2 == 0 && p == 1 && f == (-1 + α1)^2}}, 
      {{0 < α1 < 1, 0 < α2 < 1, 1/2 == p, False}, 
       {0 < α1 < 1, 0 < α2 < 1, 1/2 < p < 1, 0 < α2 < 1 && 0 < α1 < 1 && 12 p == 7 && 864 f == 49 (-1 + α2)^2 + 7 α1^2 (7 + 40 α2 + 25 α2^2) + 2 α1 (-49 + 89 α2 + 140 α2^2)}, 
       {0 < α1 < 1, 0 < α2 < 1, p == 1, False}}, 
      {{0 < α1 < 1, α2 == 1, 1/2 == p, False}, 
       {0 < α1 < 1, α2 == 1, 1/2 < p < 1, 0 < α1 < 1 && 12 p == 7 && α2 == 1 && 12 f == α1 (5 + 7 α1)}, 
       {0 < α1 < 1, α2 == 1, p == 1, False}}}, 
     {{{α1 == 1, 0 == α2, 1/2 == p, α2 == 0 && α1 == 1 && 2 p == 1 && f == 0}, 
       {α1 == 1, 0 == α2, 1/2 < p < 1, f == 0 && 1/2 < p < 1 && α1 == 1 && α2 == 0}, 
       {α1 == 1, 0 == α2, p == 1, α2 == 0 && α1 == 1 && p == 1 && f == 0}}, 
      {{α1 == 1, 0 < α2 < 1, 1/2 == p, False}, 
       {α1 == 1, 0 < α2 < 1, 1/2 < p < 1, 0 < α2 < 1 && 12 p == 7 && α1 == 1 && 12 f == α2 (5 + 7 α2)}, 
       {α1 == 1, 0 < α2 < 1, p == 1, False}}, 
      {{α1 == 1, α2 == 1, 1/2 == p, False}, 
       {α1 == 1, α2 == 1, 1/2 < p < 1, 12 p == 7 && α2 == 1 && α1 == 1 && f == 1}, 
       {α1 == 1, α2 == 1, p == 1, False}}}}  *)

and we can, if we choose manually verify that all of these minima (for the regions that contain local minima) are nonnegative. We also see that $p=7/12$ is somewhat interesting.

This is not Mathematica providing a proof that the minimum of your expression in your region is positive. (Mathematica is not designed to provide proofs.) However, all the ingredients you need are here.