This is more an extended comment to the answer of @MichaelRozenberg than an answer by its own.
I used a short Maxima to confirm the equation derived by @MichaelRozenberg.
I used Maxima because it is open source.
Here is the Maxima script (statements are terminated by $ or by ;):
"I use string to comment this file"$
"the flag `display2d` controls
the display of the output. You can unset it (display2d:false), that makes it easy to copy
the maxima output to math.stackexchange"$
"to make it easier to input the problem data
we define to function g and f:"$
g(r,s):=(8*r^3+5*s^3);
f(r,s):=r^4/g(r,s);
"
the initial problem has the form
L(x,y,t)>=R(x,y,z)
but we subtract R(x,y,z) from this equation and
we state the problem in the form
term0>=0
where term0 is L(x,y,z)-R(x,y,z)
this is term0:
"$
term0:f(x,y)+f(y,z)+f(z,x)-(x+y+z)/13;
"
Now we multiply the term0 by a positive fraction of the (positive) common denominator
and get term1 that satisfies
term1>=0
`ratsimp` does some simplification like cancelling
"$
term1:13/5*g(x,y)*g(y,z)*g(z,x)*term0,ratsimp;
"
now we assume x=0 and v>=0
`,y=x+u` and `,z=x+v` do these substitutions
"$
term2:term1,y=x+u,z=x+v;
"
ratsimp(.,x) does some simplification and displays the term as polynomial of x
"$
term3:ratsimp(term2,x);
for p:0 thru hipow(term3,x) do print (coeff(term3,x,p)*x^p);
"the lowerbound polynomial is given by @Michael Rozenberg";
lowerbound:u^5*v^5*(156*t^8+531*t^7+2*t^6-632*t^5-152*t^4+867*t^3+834*t^2+299*t+40);
"we use the expanded version of the lowerbound polynomial";
lb:lowerbound,expand;
"we want to avoid squareroots and therefore substitute u bei `q^2` and v by `w^2`.
The expression `sqrt(u*v)` (see thhe proof of Michael Rozenberg) then can be replaced by q*w";
"We want to avoid squareroots and therefore substitute u bei `q^2` and v by `w^2`.
The expression `sqrt(u*v)` (see thhe proof of Michael Rozenberg) then can be replaced by q*w.
The following loop checks for each exponent k, that the coefficient of the original polynomial
in x (adjusted by sqrt(u*v)^k) is larger than the coeffiecient of the lowerbound polynomial.
This value is called wdiff in the following.
We already mentioned that we do not use the original variable u and v but first transform
to q and w as described above and therefor the adjustment is (q*w)^k instead of sqrt(u*v)^k.
`wdiff` is a homogenous polynom of degree 20. We devide by `w`and replace `q/w` by `s`
and get the polynomial `poly` with vrailbe `s`. For these polynomials we calculate the number
of roots greater than 0. This can be done bei the `nroot` function that uses 'sturm's theorem'
Then we calculate the value of poly at 2. If this value is greate 0 and there are
no zeros greater 0 then wdiff is greater or equal 0 for all nonnegative q and w and therefore
for all nonegative u and v. This was what we wanted to proof.
We see that all polynomails are positive at 2 and also for all except for k=8 there are no zeros
greater than 0. For k=8 we have a zero with even multiplicity.
";
for k:0 thru 8 do (
coff_x:coeff(term3,x,k),
coeff_t:coeff(lb,t,k),
wdiff:ev(coff_x*(q*w)^k-coeff_t,u=q^2,v=w^2),
poly:ratsubst(s,q/w,expand(wdiff/w^20)),
nr:nroots(poly,0,inf),
print("==="),
print("k=",k),
print("coeff(term3, x,",k,")=",coff_x),
print("coeff(lb, t,",k,")=",coeff_t),
print("wdiff=",wdiff),
print("polynomial:",poly),
print("factors=",factor(poly)),
print("number of roots >0:",nr),
print("poly(2)=",ev(poly,s=2))
);
"finally we proof that the lowerbbound polynomial has no positive root and that
it is greater than 0 for t=1. Therefor it is greater or equal than 0 for all admissible values";
poly:ratcoeff(lowerbound,u^5*v^5);
poly,t=1;
nroots(poly,0,inf);
I ran the scrip on the Xmaxima console and get the following output.
I use this console with this rather ugly kind of output because it
can be simply copied and pasted to math.stackecchange.
A prettier output can be found here at an online version of Maxima
(%i1) display2d:false;
(%o1) false
(%i2)
read and interpret file: #pD:/maxima/ineq1775572.mac
(%i3) "I use string to comment this file"
(%i4) "the flag `display2d` controls
the display of the output. You can unset it (display2d:false), that makes it easy to copy
the maxima output to math.stackexchange"
(%i5) "to make it easier to input the problem data
we define to function g and f:"
(%i6) g(r,s):=8*r^3+5*s^3
(%o6) g(r,s):=8*r^3+5*s^3
(%i7) f(r,s):=r^4/g(r,s)
(%o7) f(r,s):=r^4/g(r,s)
(%i8) "
the initial problem has the form
L(x,y,t)>=R(x,y,z)
but we subtract R(x,y,z) from this equation and
we state the problem in the form
term0>=0
where term0 is L(x,y,z)-R(x,y,z)
this is term0:
"
(%i9) term0:f(x,y)+f(y,z)+f(z,x)+(-(x+y+z))/13
(%o9) z^4/(8*z^3+5*x^3)+y^4/(5*z^3+8*y^3)+((-z)-y-x)/13+x^4/(5*y^3+8*x^3)
(%i10) "
Now we multiply the term0 by a positive fraction of the (positive) common denominator
and get term1 that satisfies
term1>=0
`ratsimp` does some simplification like cancelling
"
(%i11) ev(term1:(13*g(x,y)*g(y,z)*g(z,x)*term0)/5,ratsimp)
(%o11) (25*y^3+40*x^3)*z^7+((-40*y^4)-40*x*y^3-64*x^3*y+40*x^4)*z^6
+(40*y^6+39*x^3*y^3-40*x^6)*z^4
+(40*y^7-64*x*y^6+39*x^3*y^4+39*x^4*y^3-40*x^6*y
+25*x^7)
*z^3+((-40*x^3*y^6)-64*x^6*y^3)*z+25*x^3*y^7
-40*x^4*y^6+40*x^6*y^4+40*x^7*y^3
(%i12) "
now we assume x=0 and v>=0
`,y=x+u` and `,z=x+v` do these substitutions
"
(%i13) ev(term2:term1,y = x+u,z = x+v)
(%o13) (x+v)^3*(40*(x+u)^7-64*x*(x+u)^6+39*x^3*(x+u)^4+39*x^4*(x+u)^3+25*x^7
-40*x^6*(x+u))
+25*x^3*(x+u)^7+(x+v)*((-40*x^3*(x+u)^6)-64*x^6*(x+u)^3)
+(x+v)^4*(40*(x+u)^6+39*x^3*(x+u)^3-40*x^6)-40*x^4*(x+u)^6+40*x^6*(x+u)^4
+(x+v)^6*((-40*(x+u)^4)-40*x*(x+u)^3+40*x^4-64*x^3*(x+u))
+(x+v)^7*(25*(x+u)^3+40*x^3)+40*x^7*(x+u)^3
(%i14) "
ratsimp(.,x) does some simplification and displays the term as polynomial of x
"
(%i15) term3:ratsimp(term2,x)
(%o15) (156*v^2-156*u*v+156*u^2)*x^8+(390*v^3-1056*u*v^2+1134*u^2*v+390*u^3)
*x^7
+(754*v^4-2698*u*v^3+1170*u^2*v^2
+2412*u^3*v+754*u^4)
*x^6
+(741*v^5-2178*u*v^4-1476*u^2*v^3
+3504*u^3*v^2+2997*u^4*v+741*u^5)
*x^5
+(351*v^6-489*u*v^5-2058*u^2*v^4
+546*u^3*v^3+4437*u^4*v^2
+2088*u^5*v+351*u^6)
*x^4
+(65*v^7+181*u*v^6-585*u^2*v^5
-1286*u^3*v^4+2079*u^4*v^3
+2808*u^5*v^2+768*u^6*v+65*u^7)
*x^3
+(75*u*v^7+165*u^2*v^6-675*u^3*v^5
+1416*u^5*v^3+888*u^6*v^2
+120*u^7*v)
*x^2
+(75*u^2*v^7-25*u^3*v^6-240*u^4*v^5
+240*u^5*v^4+376*u^6*v^3
+120*u^7*v^2)
*x+25*u^3*v^7-40*u^4*v^6+40*u^6*v^4
+40*u^7*v^3
(%i16) for p from 0 thru hipow(term3,x) do print(coeff(term3,x,p)*x^p)
25*u^3*v^7-40*u^4*v^6+40*u^6*v^4+40*u^7*v^3
(75*u^2*v^7-25*u^3*v^6-240*u^4*v^5+240*u^5*v^4+376*u^6*v^3+120*u^7*v^2)*x
(75*u*v^7+165*u^2*v^6-675*u^3*v^5+1416*u^5*v^3+888*u^6*v^2+120*u^7*v)*x^2
(65*v^7+181*u*v^6-585*u^2*v^5-1286*u^3*v^4+2079*u^4*v^3+2808*u^5*v^2+768*u^6*v
+65*u^7)
*x^3
(351*v^6-489*u*v^5-2058*u^2*v^4+546*u^3*v^3+4437*u^4*v^2+2088*u^5*v+351*u^6)
*x^4
(741*v^5-2178*u*v^4-1476*u^2*v^3+3504*u^3*v^2+2997*u^4*v+741*u^5)*x^5
(754*v^4-2698*u*v^3+1170*u^2*v^2+2412*u^3*v+754*u^4)*x^6
(390*v^3-1056*u*v^2+1134*u^2*v+390*u^3)*x^7
(156*v^2-156*u*v+156*u^2)*x^8
(%o16) done
(%i17) "the lowerbound polynomial is given by @Michael Rozenberg"
(%o17) "the lowerbound polynomial is given by @Michael Rozenberg"
(%i18) lowerbound:u^5*v^5
*(156*t^8+531*t^7+2*t^6-632*t^5-152*t^4+867*t^3+834*t^2
+299*t+40)
(%o18) (156*t^8+531*t^7+2*t^6-632*t^5-152*t^4+867*t^3+834*t^2+299*t+40)*u^5*v
^5
(%i19) "we use the expanded version of the lowerbound polynomial"
(%o19) "we use the expanded version of the lowerbound polynomial"
(%i20) ev(lb:lowerbound,expand)
(%o20) 156*t^8*u^5*v^5+531*t^7*u^5*v^5+2*t^6*u^5*v^5-632*t^5*u^5*v^5
-152*t^4*u^5*v^5+867*t^3*u^5*v^5+834*t^2*u^5*v^5
+299*t*u^5*v^5+40*u^5*v^5
(%i21) "we want to avoid suareroots and therefore substitute u bei `q^2` and v by `w^2`.
The expression `sqrt(u*v)` (see thhe proof of Michael Rozenberg) then can be replaced by q*w"
(%o21) "we want to avoid suareroots and therefore substitute u bei `q^2` and v by `w^2`.
The expression `sqrt(u*v)` (see thhe proof of Michael Rozenberg) then can be replaced by q*w"
(%i22) "We want to avoid suareroots and therefore substitute u bei `q^2` and v by `w^2`.
The expression `sqrt(u*v)` (see thhe proof of Michael Rozenberg) then can be replaced by q*w.
The following loop checks for each exponent k, that the coefficient of the original polynomial
in x (adjusted by sqrt(u*v)^k) is larger than the coeffiecient of the lowerbound polynomial.
This value is called wdiff in the following.
We already mentioned that we do not use the original variable u and v but first transform
to q and w as described above and therefor the adjustment is (q*w)^k instead of sqrt(u*v)^k.
`wdiff` is a homogenous polynom of degree 20. We devide by `w`and replace `q/w` by `s`
and get the polynomial `poly` with vrailbe `s`. For these polynomials we calculate the number
of roots greater than 0. This can be done bei the `nroot` function that uses 'sturm's theorem'
Then we calculate the value of poly at 2. If this value is greate 0 and there are
no zeros greater 0 then wdiff is greater or equal 0 for all nonnegative q and w and therefore
for all nonegative u and v. This was what we wanted to proof.
We see that all polynomails are positive at 2 and also for all except for k=8 there are no zeros
greater than 0. For k=8 we have a zero with even multiplicity.
"
(%o22) "We want to avoid suareroots and therefore substitute u bei `q^2` and v by `w^2`.
The expression `sqrt(u*v)` (see thhe proof of Michael Rozenberg) then can be replaced by q*w.
The following loop checks for each exponent k, that the coefficient of the original polynomial
in x (adjusted by sqrt(u*v)^k) is larger than the coeffiecient of the lowerbound polynomial.
This value is called wdiff in the following.
We already mentioned that we do not use the original variable u and v but first transform
to q and w as described above and therefor the adjustment is (q*w)^k instead of sqrt(u*v)^k.
`wdiff` is a homogenous polynom of degree 20. We devide by `w`and replace `q/w` by `s`
and get the polynomial `poly` with vrailbe `s`. For these polynomials we calculate the number
of roots greater than 0. This can be done bei the `nroot` function that uses 'sturm's theorem'
Then we calculate the value of poly at 2. If this value is greate 0 and there are
no zeros greater 0 then wdiff is greater or equal 0 for all nonnegative q and w and therefore
for all nonegative u and v. This was what we wanted to proof.
We see that all polynomails are positive at 2 and also for all except for k=8 there are no zeros
greater than 0. For k=8 we have a zero with even multiplicity.
"
(%i23) for k from 0 thru 8 do
(coff_x:coeff(term3,x,k),coeff_t:coeff(lb,t,k),
wdiff:ev(coff_x*(q*w)^k-coeff_t,u = q^2,v = w^2),
poly:ratsubst(s,q/w,expand(wdiff/w^20)),nr:nroots(poly,0,inf),
print("==="),print("k=",k),print("coeff(term3, x,",k,")=",coff_x),
print("coeff(lb, t,",k,")=",coeff_t),print("wdiff=",wdiff),
print("polynomial:",poly),print("factors=",factor(poly)),
print("number of roots >0:",nr),print("poly(2)=",ev(poly,s = 2)))
===
k= 0
coeff(term3, x, 0 )= 25*u^3*v^7-40*u^4*v^6+40*u^6*v^4+40*u^7*v^3
coeff(lb, t, 0 )= 40*u^5*v^5
wdiff= 25*q^6*w^14-40*q^8*w^12-40*q^10*w^10+40*q^12*w^8+40*q^14*w^6
polynomial: 40*s^14+40*s^12-40*s^10-40*s^8+25*s^6
factors= 5*s^6*(8*s^8+8*s^6-8*s^4-8*s^2+5)
number of roots >0: 0
poly(2)= 769600
===
k= 1
coeff(term3, x, 1 )=
75*u^2*v^7-25*u^3*v^6-240*u^4*v^5+240*u^5*v^4+376*u^6*v^3
+120*u^7*v^2
coeff(lb, t, 1 )= 299*u^5*v^5
wdiff=
q*w
*(75*q^4*w^14-25*q^6*w^12-240*q^8*w^10+240*q^10*w^8+376*q^12*w^6
+120*q^14*w^4)
-299*q^10*w^10
polynomial: 120*s^15+376*s^13+240*s^11-299*s^10-240*s^9-25*s^7+75*s^5
factors= s^5*(120*s^10+376*s^8+240*s^6-299*s^5-240*s^4-25*s^2+75)
number of roots >0: 0
poly(2)= 7074016
===
k= 2
coeff(term3, x, 2 )=
75*u*v^7+165*u^2*v^6-675*u^3*v^5+1416*u^5*v^3+888*u^6*v^2
+120*u^7*v
coeff(lb, t, 2 )= 834*u^5*v^5
wdiff=
q^2*w^2
*(75*q^2*w^14+165*q^4*w^12-675*q^6*w^10+1416*q^10*w^6+888*q^12*w^4
+120*q^14*w^2)
-834*q^10*w^10
polynomial: 120*s^16+888*s^14+1416*s^12-834*s^10-675*s^8+165*s^6+75*s^4
factors= 3*s^4*(40*s^12+296*s^10+472*s^8-278*s^6-225*s^4+55*s^2+25)
number of roots >0: 0
poly(2)= 27198192
===
k= 3
coeff(term3, x, 3 )=
65*v^7+181*u*v^6-585*u^2*v^5-1286*u^3*v^4+2079*u^4*v^3
+2808*u^5*v^2+768*u^6*v+65*u^7
coeff(lb, t, 3 )= 867*u^5*v^5
wdiff=
q^3*w^3
*(65*w^14+181*q^2*w^12-585*q^4*w^10-1286*q^6*w^8+2079*q^8*w^6
+2808*q^10*w^4+768*q^12*w^2+65*q^14)
-867*q^10*w^10
polynomial:
65*s^17+768*s^15+2808*s^13+2079*s^11-867*s^10-1286*s^9-585*s^7
+181*s^5+65*s^3
factors=
s^3*(65*s^14+768*s^12+2808*s^10+2079*s^8-867*s^7-1286*s^6-585*s^4
+181*s^2+65)
number of roots >0: 0
poly(2)= 59331624
===
k= 4
coeff(term3, x, 4 )=
351*v^6-489*u*v^5-2058*u^2*v^4+546*u^3*v^3+4437*u^4*v^2
+2088*u^5*v+351*u^6
coeff(lb, t, 4 )= -152*u^5*v^5
wdiff=
q^4*w^4
*(351*w^12-489*q^2*w^10-2058*q^4*w^8+546*q^6*w^6+4437*q^8*w^4
+2088*q^10*w^2+351*q^12)
+152*q^10*w^10
polynomial: 351*s^16+2088*s^14+4437*s^12+698*s^10-2058*s^8-489*s^6+351*s^4
factors= s^4*(351*s^12+2088*s^10+4437*s^8+698*s^6-2058*s^4-489*s^2+351)
number of roots >0: 0
poly(2)= 75549104
===
k= 5
coeff(term3, x, 5 )=
741*v^5-2178*u*v^4-1476*u^2*v^3+3504*u^3*v^2+2997*u^4*v+741*u^5
coeff(lb, t, 5 )= -632*u^5*v^5
wdiff=
q^5*w^5
*(741*w^10-2178*q^2*w^8-1476*q^4*w^6+3504*q^6*w^4+2997*q^8*w^2
+741*q^10)
+632*q^10*w^10
polynomial: 741*s^15+2997*s^13+3504*s^11+632*s^10-1476*s^9-2178*s^7+741*s^5
factors= s^5*(741*s^10+2997*s^8+3504*s^6+632*s^5-1476*s^4-2178*s^2+741)
number of roots >0: 0
poly(2)= 55645088
===
k= 6
coeff(term3, x, 6 )= 754*v^4-2698*u*v^3+1170*u^2*v^2+2412*u^3*v+754*u^4
coeff(lb, t, 6 )= 2*u^5*v^5
wdiff=
q^6*w^6*(754*w^8-2698*q^2*w^6+1170*q^4*w^4+2412*q^6*w^2+754*q^8)
-2*q^10*w^10
polynomial: 754*s^14+2412*s^12+1168*s^10-2698*s^8+754*s^6
factors= 2*s^6*(377*s^8+1206*s^6+584*s^4-1349*s^2+377)
number of roots >0: 0
poly(2)= 22786688
===
k= 7
coeff(term3, x, 7 )= 390*v^3-1056*u*v^2+1134*u^2*v+390*u^3
coeff(lb, t, 7 )= 531*u^5*v^5
wdiff= q^7*w^7*(390*w^6-1056*q^2*w^4+1134*q^4*w^2+390*q^6)-531*q^10*w^10
polynomial: 390*s^13+1134*s^11-531*s^10-1056*s^9+390*s^7
factors= 3*s^7*(130*s^6+378*s^4-177*s^3-352*s^2+130)
number of roots >0: 0
poly(2)= 4482816
===
k= 8
coeff(term3, x, 8 )= 156*v^2-156*u*v+156*u^2
coeff(lb, t, 8 )= 156*u^5*v^5
wdiff= q^8*w^8*(156*w^4-156*q^2*w^2+156*q^4)-156*q^10*w^10
polynomial: 156*s^12-312*s^10+156*s^8
factors= 156*(s-1)^2*s^8*(s+1)^2
number of roots >0: 2
poly(2)= 359424
(%o23) done
(%i24) "finally we proof that the lowerbbound polynomial has no positive root and that
it is greater than 0 for t=1. Therefor it is greater or equal than 0 for all admissible values"
(%o24) "finally we proof that the lowerbbound polynomial has no positive root and that
it is greater than 0 for t=1. Therefor it is greater or equal than 0 for all admissible values"
(%i25) poly:ratcoef(lowerbound,u^5*v^5)
(%o25) 156*t^8+531*t^7+2*t^6-632*t^5-152*t^4+867*t^3+834*t^2+299*t+40
(%i26) ev(poly,t = 1)
(%o26) 1945
(%i27) nroots(poly,0,inf)
(%o27) 0
(%i28)
Here we list the coefficient functions so we can compare them to @MichaelRozenbergs function to see they are the same.
$$\begin{array}{r} \tag{1}
\left(25\,u^3\,v^7-40\,u^4\,v^6+40\,u^6\,v^4+40\,u^7\,v^3\right)\,x^0 \\
\left(75\,u^2\,v^7-25\,u^3\,v^6-240\,u^4\,v^5+240\,u^5\,v^4+376\,u^
6\,v^3+120\,u^7\,v^2\right)\,x^1 \\
\left(75\,u\,v^7+165\,u^2\,v^6-675\,u^3\,v^5+1416\,u^5\,v^3+888\,u^
6\,v^2+120\,u^7\,v\right)\,x^2 \\
\left(65\,v^7+181\,u\,v^6-585\,u^2\,v^5-1286\,u^3\,v^4+2079\,u^4\,v
^3+2808\,u^5\,v^2+768\,u^6\,v+65\,u^7\right)\,x^3 \\
\left(351\,v^6-489\,u\,v^5-2058\,u^2\,v^4+546\,u^3\,v^3+4437\,u^4\,
v^2+2088\,u^5\,v+351\,u^6\right)\,x^4 \\
\left(741\,v^5-2178\,u\,v^4-1476\,u^2\,v^3+3504\,u^3\,v^2+2997\,u^4
\,v+741\,u^5\right)\,x^5 \\
\left(754\,v^4-2698\,u\,v^3+1170\,u^2\,v^2+2412\,u^3\,v+754\,u^4
\right)\,x^6 \\
\left(390\,v^3-1056\,u\,v^2+1134\,u^2\,v+390\,u^3\right)\,x^7 \\
\left(156\,v^2-156\,u\,v+156\,u^2\right)\,x^8
\end{array}$$
To proof that this function is larger than
$$\left(156\,t^8+531\,t^7+2\,t^6-632\,t^5-152\,t^4+867\,t^3+834\,t^2+
299\,t+40\right)\,u^5\,v^5 \tag{2}$$
Rozenbergs's lower bound when we substitute $x$ by $t\sqrt(uv)$ we show that each coefficient of the polynomial $(1)$ is larger than the corresponding coefficient of the lower bound polynomial $(2)$.
Then we show that the polynomial $(2)$ is larger than $0$ for all nonnegative $u$, $v$ and $t$. Details can be found in the Maxima script.
Instead of the Maxima nroots
function, which is based on Sturm sequences, one could solve the equations by some numeric functions to see if there are zeros greater than zeros, e.g. calculating the roots of poly
for k=7
gives the following:
(%i29) allroots(390*s^13+1134*s^11-531*s^10-1056*s^9+390*s^7 ,s);
(%o29) [s = 0.0,s = 0.0,s = 0.0,s = 0.0,s = 0.0,s = 0.0,s = 0.0,
s = 0.007444635413686057*%i+0.7516683014652126,
s = 0.7516683014652126-0.007444635413686057*%i,
s = 0.3202741285237583*%i-0.6047586795035632,
s = (-0.3202741285237583*%i)-0.6047586795035632,
s = 1.93839678615644*%i-0.1469096219616494,
s = (-1.93839678615644*%i)-0.1469096219616494]
So we can also conclude are no real roots greater than 0. But this method is not really acceptable if one does not analyze the impact of the rounding errors. And this can be very complicated. The nroots
function works with integers (for integer polynomials) and so there are no rounding errors.