Prove an inequality or find the global optimum solution

Question

I have an expression on $x$ as follows (from my friend).

$f(x)=x^4-2 a d x^3-2 b d x^3-2 c d x^3-2 d x^3+a^2 d^2 x^2+b^2 d^2 x^2+c^2 d^2 x^2+4 a d^2 x^2+2 a b d^2 x^2+3 b d^2 x^2+2 a c d^2 x^2+3 b c d^2 x^2+3 c d^2 x^2-a b x^2-a c x^2-b c x^2+2 a b d x^2+2 a c d x^2+2 b c d x^2+2 d x^2-x^2-2 a^2 d^3 x-b^2 d^3 x-b c^2 d^3 x-c^2 d^3 x-3 a b d^3 x-b^2 c d^3 x-3 a c d^3 x-2 a b c d^3 x-2 b c d^3 x-2 a b^2 d^2 x-2 a c^2 d^2 x-2 b c^2 d^2 x-4 a d^2 x-2 a^2 b d^2 x-2 a b d^2 x-2 b d^2 x-2 a^2 c d^2 x-2 b^2 c d^2 x-2 a c d^2 x-4 a b c d^2 x-4 b c d^2 x-2 c d^2 x+a b^2 d x+a c^2 d x+b c^2 d x+2 a d x+a^2 b d x+a b d x+b d x+a^2 c d x+b^2 c d x+a c d x+2 a b c d x+2 b c d x+c d x+2 a^2 d^3+2 a b^2 d^3+2 b^2 c^2 d^3+2 a c^2 d^3+2 a b c^2 d^3+2 b c^2 d^3+2 a^2 b d^3+2 a b d^3+2 a^2 c d^3+2 a b^2 c d^3+2 b^2 c d^3+2 a c d^3+8 a b c d^3-a^2 d^2-a b^2 d^2-b^2 c^2 d^2-a c^2 d^2-a b c^2 d^2-b c^2 d^2-a^2 b d^2-a b d^2-a^2 c d^2-a b^2 c d^2-b^2 c d^2-a c d^2+4 a^2 b c d^2-12 a b c d^2+4 b c d^2+a^2 b c-2 a b c+b c-4 a^2 b c d+8 a b c d-4 b c d$

where $a\geqslant b+1, b\geqslant c, b\geqslant1, c\geqslant0, 0\leqslant d \leqslant1$ and $a,b,c$ are integers.

I would like to prove that $f(x)>0$ or $\min f(x)>0$ when $$x\geqslant \frac{1}{2}\left(d(2a+b+c)+\sqrt{d^2(2a+b+c)^2+8a(b+c)(1-2d)}\right),$$

When I used Lingo, it only found a local minimum (3.6..) instead of the global minimum (even though I chose the option Global Solve).

min=(-a^2)*d^2+2*a^2*d^3-a*d^2*b-a^2*d^2*b+2*a*d^3*b+2*a^2*d^3*b-a*d^2*b^2+2*a*d^3*b^2-a*d^2*c-
a^2*d^2*c+2*a*d^3*c+2*a^2*d^3*c+b*c-2*a*b*c+a^2*b*c-4*d*b*c+8*a*d*b*c-4*a^2*d*b*c+
4*d^2*b*c-12*a*d^2*b*c+4*a^2*d^2*b*c+8*a*d^3*b*c-d^2*b^2*c-a*d^2*b^2*c+2*d^3*b^2*c+
2*a*d^3*b^2*c-a*d^2*c^2+2*a*d^3*c^2-d^2*b*c^2-a*d^2*b*c^2+2*d^3*b*c^2+2*a*d^3*b*c^2-
d^2*b^2*c^2+2*d^3*b^2*c^2+2*a*d*x-4*a*d^2*x-2*a^2*d^3*x+d*b*x+a*d*b*x+a^2*d*b*x-2*d^2*b*x-
2*a*d^2*b*x-2*a^2*d^2*b*x-3*a*d^3*b*x+a*d*b^2*x-2*a*d^2*b^2*x-d^3*b^2*x+d*c*x+a*d*c*x+
a^2*d*c*x-2*d^2*c*x-2*a*d^2*c*x-2*a^2*d^2*c*x-3*a*d^3*c*x+2*d*b*c*x+2*a*d*b*c*x-4*d^2*b*c*x-
4*a*d^2*b*c*x-2*d^3*b*c*x-2*a*d^3*b*c*x+d*b^2*c*x-2*d^2*b^2*c*x-d^3*b^2*c*x+a*d*c^2*x-
2*a*d^2*c^2*x-d^3*c^2*x+d*b*c^2*x-2*d^2*b*c^2*x-d^3*b*c^2*x-x^2+2*d*x^2+4*a*d^2*x^2+
a^2*d^2*x^2-a*b*x^2+2*a*d*b*x^2+3*d^2*b*x^2+2*a*d^2*b*x^2+d^2*b^2*x^2-a*c*x^2+2*a*d*c*x^2+
3*d^2*c*x^2+2*a*d^2*c*x^2-b*c*x^2+2*d*b*c*x^2+3*d^2*b*c*x^2+d^2*c^2*x^2-2*d*x^3-2*a*d*x^3-
2*d*b*x^3-2*d*c*x^3+x^4;
x >= 1/2*(d*(2*a + b + c) + @SQRT((d)^2*(2*a + b + c)^2 + 8*a*(b + c)*(1 - 2*d))); 
a >= b + 1;
b >= c;
b >= 1;
c >= 0;
d >= 0;
d <= 1;
@GIN(a);
@GIN(b);
@GIN(c);

  Local optimal solution found.
  Objective value:                              3.646110
  Objective bound:                              3.646110
  Infeasibilities:                              0.000000
  Extended solver steps:                               0
  Total solver iterations:                            21
  Elapsed runtime seconds:                          0.14

  Model Class:                                     MINLP

  Total variables:                      5
  Nonlinear variables:                  5
  Integer variables:                    3

  Total constraints:                    8
  Nonlinear constraints:                2

  Total nonzeros:                      18
  Nonlinear nonzeros:                   9



                                Variable           Value        Reduced Cost
                                       A        2.000000            0.000000
                                       D       0.1741100            0.000000
                                       B        1.000000            0.000000
                                       C        0.000000            0.000000
                                       X        2.107574            0.000000

                                     Row    Slack or Surplus      Dual Price
                                       1        3.646110           -1.000000
                                       2        0.000000           -14.59492
                                       3        0.000000           -5.918372
                                       4        1.000000            0.000000
                                       5        0.000000           -13.40245
                                       6        0.000000           -5.672014
                                       7       0.1741100            0.000000
                                       8       0.8258900            0.000000

Can I assert that the local optimum solution $3.646110$ is the global optimum solution? Or is their difference so small that it is enough to demonstrate $f > 0$? Or is it possible that this expression does not have a global minimum value? I originally intended to use Mathematica for calculations, but unfortunately, there are no corresponding results. Please see the link below.

• How to estimate whether the objective expression has a global minimum value?

---

In the original problem, $f(x)$ is the characteristic polynomial of $A$.

$$A:=\left( \begin{array}{cccc} d(b+1) & 0 & (1-d)b & 1-d \\ 0 & d(a+b) & (1-d)b & (1-d)a \\ (1-d)a & (1-d)c & d(a+c) & 0 \\ 1-d& (1-d)c & 0 & d(c+1) \\ \end{array} \right).$$

Answer 1

In Mathematica, after reducing the constraints:

Reduce[{a >= b + 1, b >= c, b >= 1, c >= 0, d >= 0, d <= 1}, c]

(a == 2 && b == 1 && 0 <= d <= 1 && 0 <= c <= 1) ||
(a > 2 && 1 <= b <= -1 + a && 0 <= d <= 1 && 0 <= c <= b)

and after verifying that:

emin = ((2 a + b + c) d + Sqrt[(2 a + b + c)^2 d^2 + 8 a (b + c) (1 - 2 d)]) / 2;
cons = {a >= 2, 1 <= b <= a - 1, 0 <= c <= b, 0 <= d <= 1};
NMinimize[{emin, cons}, {a, b, c, d}]

{2., {a -> 2., b -> 1., c -> 6.10647 * 10^-8, d -> 1.22195 * 10^-7}}

it's possible to write:

A = {{d (b + 1), 0, (1 - d) b, 1 - d},
     {0, d (a + b), (1 - d) b, (1 - d) a},
     {(1 - d) a, (1 - d) c, d (a + c), 0},
     {1 - d, (1 - d) c, 0, d (c + 1)}};

f = Det[A - e IdentityMatrix[4]];

cons = {a >= 2, 1 <= b <= a - 1, 0 <= c <= b, 0 <= d <= 1, e >= 2, e >= emin};

NMinimize[{f, cons}, {a, b, c, d, e}]

{2.59802, {a -> 2., b -> 1., c -> 1., d -> 0.795932, e -> 3.37098}}

that is, f is positive in cons, as we wanted to prove.