:

## Inequality proved with Maple

Maple

How to prove the inequality provided , ? That problem was posed  by Israeli mathematician nicked by himself as arqady in Russian math forum and was not answered there.I know how to prove that with Maple and don't know how to prove that without Maple. Neither nor work here. The difficulty consists in the nonlinearity both the target function and the main constraint. The first step is to linearize the main constraint and the second step is to reduce the number of variables to one.

restart; A := eval(x^(4*y)+y^(4*x), [x = sqrt(u), y = sqrt(v)]); (1)

B := expand(A); (2)

C := eval(B, u = 2-v); (3)

It is more or less clear that the plot of F is symmetric wrt  the straight line v=1. This motivates the following change of variable  to obtain an even function.

F := simplify(expand(eval(C, v = z+1)), symbolic, power); (4) The plots suggest the only maximim of F at z=0 and its concavity.

Student[Calculus1]:-FunctionPlot(F, z = -1 .. 1); Student[Calculus1]:-FunctionPlot(diff(F, z, z), z = -1 .. 1); As usually, numeric global solvers cannot prove certain inequalities. However, the GlobalSearch command of the DirectSearch package indicates the only local maximum of  F and F''. Digits := 25; DirectSearch:-GlobalSearch(F, {z = -1 .. 1}, maximize, solutions = 3, tolerances = 10^(-15)); DirectSearch:-GlobalSearch(diff(F, z, z), {z = -1 .. 1}, maximize, solutions = 3, tolerances = 10^(-15)); (5)

The series command confirms a local maximum of F at z=0.

series(F, z, 6); (6)

The extrema command indicates only the value of F at a critical point, not outputting its position.

extrema(F, z); extrema(F, z, 's'); (7)

solve(F = 2); (8)

DirectSearch:-SolveEquations(F = 2, {z = -1 .. 1}, AllSolutions, solutions = 3); (9)

DirectSearch:-SolveEquations(F = 2, {z = -1 .. 1}, AllSolutions, solutions = 3, assume = integer); (10) PS. I see my proof needs an additional explanation. The DirectSearch command establishes the only both local and global  maximum of F is located at z= -1.98*10^(-13) up to default error 10^(-9). After that  the series command confirms a local maximum at z=0. Combining these, one draws the conclusion that the global maximum is placed exactly at z=0 and equals 2. In order to confirm that the only real root of F=2 at z=0  is found approximately and exactly by the DirectSearch. 