1
$\begingroup$

I want to show That: $$ 1+a^{2017}+b^{2017} \geq a^{10}b^7+a^7b^{2000}+a^{2000}b^{10} \\ a,b\in \mathbb{R}^+_0$$ I used Simplify and then Resolve That is taking forever:

Resolve[ForAll[{a, b}, a >= 0 && b >= 0,1 + a^2017 + b^2017 >= a^7 b^7 (a^3 + a^1993 b^3 + b^1993)], Reals]

Is there a way for it that works?

$\endgroup$
  • $\begingroup$ This is a hard inequality likely proved by a trick. In my opinion, Mathematica uses standard methods to this end. That takes a lot of time. Mathematica easily proves a such type inequality with lesser powers, e.g. Resolve[ForAll[{a, b}, a >= 0 && b >= 0, 1 + a^10 + b^10 - a^2 b^7 - a^7 b - a b^2 >= 0]] and/or Minimize[{1 + a^10 + b^10 - a^2 b^7 - a^7 b - a b^2, a >= 0 && b >= 0}, {a, b}]. The former performs True and the latter produces {0, {a -> 1, b -> 1}}. $\endgroup$ – user64494 Apr 25 at 11:50
0
$\begingroup$

Well, you can try this one.

NMinimize[1 + a^2017 + b^2017 - a^10 b^7 - a^7 b^2000 - a^2000 b^10, {a, b}]
| improve this answer | |
$\endgroup$
  • 1
    $\begingroup$ This is not it: in particular, you don't take into account the condition $ a,b\in \mathbb{R}^+_0$. $\endgroup$ – user64494 Apr 25 at 5:05
0
$\begingroup$

to me, it seems to suffice to show equality for a=b=1, and further look at the behaviour for a and b close to 1:

it = a^10 b^7 + a^7 b^2000 + a^2000 b^10;
it /. {a^i_ -> 1 + i \[Alpha], b^j_ -> 1 + j \[Beta]} //Expand

giving

3 + 2017 \[Alpha] + 2017 \[Beta] + 34070 \[Alpha] \[Beta]

I notice that the last term makes the right side always bigger than the left if both a and b are >1 or both <1.

| improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.