In this notebook there are presented examples of usage of shiroin, a python library for proving inequalities of multivariate polynomials.

At the beginning we need to load the packages.


```python
from sympy import *
from shiroin import *
from IPython.display import Latex
shiro.seed=1
shiro.display=lambda x:display(Latex(x))
```

`shiro.seed=1` sets a seed for proving functions. If you don't write it, you can get a slightly different proof each time you run a function. This line is here only for the sake of reproducibility. 

The next line provides a nicer display of proofs, i.e. formulas will be shown instead of LaTeX code of these formulas. Note that this works on Jupyter, but not on the git page.

Now let's make some proofs. We will use problems from https://www.imomath.com/index.php?options=593&lmm=0.

#### Problem 1
Prove the inequality $a^2+b^2+c^2\ge ab+bc+ca$, if $a,b,c$ are real numbers.

Function `prove` tries to prove that given formula is nonnegative, **assuming all variables are nonnegative**. In this case the nonnegativity assumption is not a problem, since all powers on the left side are even, so if $|a|^2+|b|^2+|c|^2 \ge |ab|+|ac|+|bc|,$ then $a^2+b^2+c^2= |a|^2+|b|^2+|c|^2 \ge |ab|+|ac|+|bc| \ge ab+ac+bc$.


```python
prove('(a^2+b^2+c^2-a*b-a*c-b*c)')
```


numerator: $a^{2} - a b - a c + b^{2} - b c + c^{2}$



denominator: $1$



status: 0



From weighted AM-GM inequality:



Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again.



$$ a b+a c+b c \le a^{2}+b^{2}+c^{2} $$





    -1



Function prove prints several things. The first two gives us a formula after expanding it. The next one is status, which is the return status of the first use of ```scipy.optimize.linprog```. Possible outputs and explanations are

* 0 - found a proof with real coefficients,
* 1 - need more time, 
* 2 - function didn't find a proof,
* 3,4 - loss of precision (which may happen if it has to work with big numbers).

Then we've got a hint. So let's use it!


```python
prove('(a^2+b^2+c^2-a*b-a*c-b*c)*2')
```


numerator: $2 a^{2} - 2 a b - 2 a c + 2 b^{2} - 2 b c + 2 c^{2}$



denominator: $1$



status: 0



From weighted AM-GM inequality:



$$2 a b \le a^{2}+b^{2}$$



$$2 a c \le a^{2}+c^{2}$$



$$2 b c \le b^{2}+c^{2}$$



$$ 0 \le 0 $$



The sum of all inequalities gives us a proof of the inequality.





    0



#### Problem 2
Find all real numbers such that $a^2+b^2+c^2+d^2=a(b+c+d)$. 

At first glance it doesn't look like an inequality problem, but actually it is one. If you try to calculate both sides for different values, you can see that the left side of the equation is never less than the right one. So let's try


```python
prove('a^2+b^2+c^2+d^2-a*(b+c+d)')
```


numerator: $a^{2} - a b - a c - a d + b^{2} + c^{2} + d^{2}$



denominator: $1$



status: 2



Program couldn't find any proof.



$$ a b+a c+a d \le a^{2}+b^{2}+c^{2}+d^{2} $$





    2



This time `prove` didn't found the proof. But it doesn't mean that the inequality is not true! `prove` uses a list of $n$ positive values, where $n$ is a number of variables in the formula. List of values should correspond to the list of variables in alphabetical order. Here are a few tips how to choose the right values.

1. Consider a function $pos(values)$ which is the sum of the positive addends in the formula after substitution of values to variables. Analogically, let $neg(values)$ be the sum of the negative addends. We should choose such values for which $quotient=pos(values)/|neg(values)|$ is small. 
2. The symmetry group of the formula splits set of variables into orbits. Using the same values for variables in one orbit is recommended. In particular, if the symmetry group of the formula is transitive (for example, when the formula is cyclic), then all values (probably) should be the same.
3. If the formula is homogeneous, then $values=(a_1,a_2,...,a_n)$ provide a proof iff $values=(ka_1,ka_2,...,ka_n)$ provides a proof for any $k\in Q_+$ (as long as you don't run into overflow error).

In the formula above $b,c,d$ are in one orbit and the formula is homogenous, so let's try $a=2$ and $b=c=d=1$.


```python
prove('a^2+b^2+c^2+d^2-a*(b+c+d)','2,1,1,1')
```


Substitute $a\to 2 e$



numerator: $b^{2} - 2 b e + c^{2} - 2 c e + d^{2} - 2 d e + 4 e^{2}$



denominator: $1$



status: 0



From weighted AM-GM inequality:



$$2 b e \le b^{2}+e^{2}$$



$$2 c e \le c^{2}+e^{2}$$



$$2 d e \le d^{2}+e^{2}$$



$$ 0 \le e^{2} $$



The sum of all inequalities gives us a proof of the inequality.





    0



Function makes a substitution $a\to 2e$ and try to prove new inequality. This time it succeeded. Moreover, if starting formula is equal to 0, then all these inequalities have to be equalities, so $e^2=0$ and eventually $a=0$. We can also try a little bit lower value for $a$.


```python
prove('a^2+b^2+c^2+d^2-a*(b+c+d)','7/4,1,1,1')
```


Substitute $a\to \frac{7 f}{4}$



numerator: $16 b^{2} - 28 b f + 16 c^{2} - 28 c f + 16 d^{2} - 28 d f + 49 f^{2}$



denominator: $16$



status: 0



From weighted AM-GM inequality:



$$28 b f \le 14 b^{2}+14 f^{2}$$



$$28 c f \le 14 c^{2}+14 f^{2}$$



$$28 d f \le 14 d^{2}+14 f^{2}$$



$$ 0 \le 2 b^{2}+2 c^{2}+2 d^{2}+7 f^{2} $$



The sum of all inequalities gives us a proof of the inequality.





    0



Now we can see that if $a^2+b^2+c^2+d^2-a(b+c+d)=0$, then $7f^2+2b^2+2c^2+2d^2=0$ and eventually $a=b=c=d=0$. Note that inequality is proved only for positive numbers (which, by continuity, can be expanded to nonnegative numbers). But using similar argumentation to the one in previous problem, if $(a,b,c,d)=(x,y,z,t)$ is the solution of $a^2+b^2+c^2+d^2-a(b+c+d)=0$, then $(a,b,c,d)=(|x|,|y|,|z|,|t|)$ is a solution, too. Since the only nonnegative solution is $(0,0,0,0)$, it means that it is the only solution.

It is worth noting that this time function `prove` used $f$ as a new variable instead of $e$. If you want to start a new proof and you don't care about the collision of variables from previous proofs, you can use `newproof` function, which clears the set of used variables.

We can also use the `findvalues` function to find values for the proof more automatically. It looks for (local) minimum of the $quotient$ value defined above.


```python
formula=S('a^2+b^2+c^2+d^2-a*(b+c+d)')
numvalues=findvalues(formula)
numvalues
```

    Optimization terminated successfully.
             Current function value: 1.154701
             Iterations: 68
             Function evaluations: 127





    (1.4339109663193974,
     0.8278441585048405,
     0.8279027492686561,
     0.8278930696996669)



If the $quotient$ value were less than 1, that would mean that the formula is negative for given values. If $quotient$ were equal to 1, then we have to choose exactly these values (or other values for which the $quotient$ is equal to 1. But here $quotient$ is greater than 1, so we can take a point near it and (probably) still have a proof. The values given to the `prove` function must not be floating point numbers, so we can rationalize them.


```python
values=nsimplify(numvalues,tolerance=0.1,rational=True)
values
```




$\displaystyle \left( \frac{10}{7}, \  \frac{5}{6}, \  \frac{5}{6}, \  \frac{5}{6}\right)$




```python
newproof()
prove(formula,values)
```


Substitute $a\to \frac{10 e}{7}$



Substitute $b\to \frac{5 f}{6}$



Substitute $c\to \frac{5 g}{6}$



Substitute $d\to \frac{5 h}{6}$



numerator: $3600 e^{2} - 2100 e f - 2100 e g - 2100 e h + 1225 f^{2} + 1225 g^{2} + 1225 h^{2}$



denominator: $1764$



status: 0



From weighted AM-GM inequality:



$$2100 e f \le 1050 e^{2}+1050 f^{2}$$



$$2100 e g \le 1050 e^{2}+1050 g^{2}$$



$$2100 e h \le 1050 e^{2}+1050 h^{2}$$



$$ 0 \le 450 e^{2}+175 f^{2}+175 g^{2}+175 h^{2} $$



The sum of all inequalities gives us a proof of the inequality.





    0



If you set the tolerance bigger, then the values will have smaller numerators and denominators, so coefficients in the proof will be smaller, too. But if the tolerance is too big, then proof will not be found.

Let's skip the problem 3 and look solve the problem 4 instead.

#### Problem 4
If $x$ and $y$ are two positive numbers less than 1, prove that
$$\frac{1}{1-x^2}+\frac{1}{1-y^2}\ge \frac{2}{1-xy}.$$


```python
prove('1/(1-x^2)+1/(1-y^2)-2/(1-x*y)')
```


numerator: $- x^{3} y + 2 x^{2} y^{2} - x^{2} - x y^{3} + 2 x y - y^{2}$



denominator: $x^{3} y^{3} - x^{3} y - x^{2} y^{2} + x^{2} - x y^{3} + x y + y^{2} - 1$



status: 2



Program couldn't find any proof.



$$ x^{3} y+x^{2}+x y^{3}+y^{2} \le 2 x^{2} y^{2}+2 x y $$



It looks like the formula is symmetric. You can assume without loss of generality that x >= y. Try



prove(makesubs(S("-x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2"),[('y', 'oo')])





    2



`prove` assumes that formula is well-defined if all variables are positive, so it doesn't have to analyze the denominator (except of choosing the right sign). In this case it is not true, since if $x=1$, then $1-x^2=0$. Also denominator is equal to $(x^2-1)(y^2-1)(xy-1)$ which is negative for $x,y\in (0,1)$. So we need to make some substitution after which new variables can have all positive values, not just these inside (0,1) interval.

We will use a function `makesubs` to generate these substitutions. It has three basic parameters: `formula`, `intervals` and `values`. `intervals` are current limitations of variables, `values` are values of variables for which $quotient$ of `formula` is small. `values` should be inside corresponding `intervals`. This argument is optional but it's better to use it.
Let's go back to our problem. If $x=y$, then $\frac{1}{1-x^2}+\frac{1}{1-y^2}\ge \frac{2}{1-xy}$, so it's the minimum value of the formula. So let `values=(1/2,1/2)` (**warning: do not use decimal point**, for example '0.5,0.5').


```python
newproof()
newformula,newvalues=makesubs('1/(1-x^2)+1/(1-y^2)-2/(1-x*y)','[0,1],[0,1]','1/2,1/2')
prove(newformula*3,newvalues)
```


Substitute $x\to 1 - \frac{1}{a + 1}$



Substitute $y\to 1 - \frac{1}{b + 1}$



numerator: $6 a^{3} b + 3 a^{3} - 12 a^{2} b^{2} - 3 a^{2} b + 3 a^{2} + 6 a b^{3} - 3 a b^{2} - 6 a b + 3 b^{3} + 3 b^{2}$



denominator: $4 a^{2} b + 2 a^{2} + 4 a b^{2} + 8 a b + 3 a + 2 b^{2} + 3 b + 1$



status: 0



From weighted AM-GM inequality:



$$12 a^{2} b^{2} \le 6 a^{3} b+6 a b^{3}$$



$$3 a^{2} b \le 2 a^{3}+b^{3}$$



$$3 a b^{2} \le a^{3}+2 b^{3}$$



$$6 a b \le 3 a^{2}+3 b^{2}$$



$$ 0 \le 0 $$



The sum of all inequalities gives us a proof of the inequality.





    0



Now let's get back to problem 3.

#### Problem 3

If $a,b,c$ are positive real numbers that satisfy $a^2+b^2+c^2=1$, find the minimal value of
$$\frac{a^2b^2}{c^2}+\frac{b^2c^2}{a^2}+\frac{c^2a^2}{b^2}$$

The problem is equivalent to finding minimum of $xy/z+yz/x+zx/y$ assuming $x+y+z=1$ and $x,y,z>0$. The first idea is to suppose that the minimum is reached when $x=y=z$. In that case, $x=y=z=1/3$ and formula is equal to 1. Now we can substitute $z\to 1-x-y$. Constraints for variables are $x>0$, $y>0$, $x+y<1$. We can rewrite it as $x \in (0,1-y)$, $y \in (0,1)$. These two conditions have two important properties:
* constraints for variables are written as intervals,
* there are no "backwards dependencies", i.e. there is no $x$ in the interval of $y$.

If these two conditions hold, then you can use `makesubs` function.


```python
newproof()
formula=Sm('xy/z+yz/x+zx/y-1').subs('z',S('1-x-y'))
newformula,values=makesubs(formula,'[0,1-y],[0,1]','1/3,1/3')
prove(newformula,values)
```


Substitute $x\to - y + 1 + \frac{y - 1}{a + 1}$



Substitute $y\to 1 - \frac{1}{b + 1}$



Substitute $b\to \frac{c}{2}$



numerator: $a^{4} c^{2} + a^{3} c^{2} - 2 a^{3} c - 4 a^{2} c + 4 a^{2} + a c^{2} - 2 a c + c^{2}$



denominator: $a^{3} c^{2} + 2 a^{3} c + 2 a^{2} c^{2} + 4 a^{2} c + a c^{2} + 2 a c$



status: 0



From weighted AM-GM inequality:



$$2 a^{3} c \le a^{4} c^{2}+a^{2}$$



$$4 a^{2} c \le a^{3} c^{2}+2 a^{2}+a c^{2}$$



$$2 a c \le a^{2}+c^{2}$$



$$ 0 \le 0 $$



The sum of all inequalities gives us a proof of the inequality.





    0



The proof is found, so the assumption that 1 is the minimum of `xy/z+yz/x+zx/y` was good.

Functions `S` and `Sm` creates a SymPy object from a string. The only difference is that `Sm` assumes that there are no multi-letter variables and adds a multiplication sign between every two terms which has no operator sign, so object `Sm(xy/z+yz/x+zx/y)` has 3 variables `x,y,z` and `S('xy/z+yz/x+zx/y')` has 6 variables `x,y,z,xy,yz,zx`. 

As you may have noticed, formulas are often cyclic or symmetric. Therefore you can use `cyclize` or `symmetrize` function to reduce the length of the written formula. Here are a few commands which will do the same as each other. 


```python
prove('(a^2+b^2+c^2-a*b-a*c-b*c)*2')
#prove(S('(a^2+b^2+c^2-a*b-a*c-b*c)*2'))
#prove(Sm('2(a^2+b^2+c^2-ab-ac-bc)'))
#prove(cyclize('2*a^2-2*a*b'))
#prove(symmetrize('a^2-a*b'))
```


numerator: $2 a^{2} - 2 a b - 2 a c + 2 b^{2} - 2 b c + 2 c^{2}$



denominator: $1$



status: 0



From weighted AM-GM inequality:



$$2 a b \le a^{2}+b^{2}$$



$$2 a c \le a^{2}+c^{2}$$



$$2 b c \le b^{2}+c^{2}$$



$$ 0 \le 0 $$



The sum of all inequalities gives us a proof of the inequality.





    0



Now look at formula $(x-1)^4$. It's quite obvious that it's nonnegative, but `prove` fails to show this!


```python
prove('(x-1)^4')
```


numerator: $x^{4} - 4 x^{3} + 6 x^{2} - 4 x + 1$



denominator: $1$



status: 2



Program couldn't find any proof.



$$ 4 x^{3}+4 x \le x^{4}+6 x^{2}+1 $$





    2



But there is a relatively simple method to generate a proof using this library. We will make to proofs: one for $x\in (1,\infty)$ and the second one for $(-\infty,1)$.


```python
newproof()
prove(makesubs('(x-1)^4','(1,oo)'))
```


Substitute $x\to a + 1$



numerator: $a^{4}$



denominator: $1$



status: 0



$$ 0 \le a^{4} $$



The sum of all inequalities gives us a proof of the inequality.





    0




```python
newproof()
prove(makesubs('(x-1)^4','(-oo,1)'))
```


Substitute $x\to 1 - a$



numerator: $a^{4}$



denominator: $1$



status: 0



$$ 0 \le a^{4} $$



The sum of all inequalities gives us a proof of the inequality.





    0



Now let's go to the problem 10
#### Problem 10
If $a,b,c,d>0$, prove that
$$\frac a{b+c}+\frac b{c+d}+ \frac c{d+a}+ \frac d{a+b}\geq 2.$$

Let's try a simple approach.


```python
formula=cyclize('a/(b+c)',variables='a,b,c,d')-2
formula
```




$\displaystyle \frac{a}{b + c} + \frac{b}{c + d} + \frac{c}{a + d} + \frac{d}{a + b} - 2$




```python
prove(formula)
```


numerator: $a^{3} c + a^{3} d + a^{2} b^{2} - a^{2} b d - 2 a^{2} c^{2} - a^{2} c d + a^{2} d^{2} + a b^{3} - a b^{2} c - a b^{2} d - a b c^{2} + a c^{3} - a c d^{2} + b^{3} d + b^{2} c^{2} - 2 b^{2} d^{2} + b c^{3} - b c^{2} d - b c d^{2} + b d^{3} + c^{2} d^{2} + c d^{3}$



denominator: $a^{2} b c + a^{2} b d + a^{2} c^{2} + a^{2} c d + a b^{2} c + a b^{2} d + a b c^{2} + 2 a b c d + a b d^{2} + a c^{2} d + a c d^{2} + b^{2} c d + b^{2} d^{2} + b c^{2} d + b c d^{2}$



status: 2



Program couldn't find any proof.



$$ a^{2} b d+2 a^{2} c^{2}+a^{2} c d+a b^{2} c+a b^{2} d+a b c^{2}+a c d^{2}+2 b^{2} d^{2}+b c^{2} d+b c d^{2} \le a^{3} c+a^{3} d+a^{2} b^{2}+a^{2} d^{2}+a b^{3}+a c^{3}+b^{3} d+b^{2} c^{2}+b c^{3}+b d^{3}+c^{2} d^{2}+c d^{3} $$





    2



This problem, like the previous one, can be solved by splitting the domain of variables to several subdomains. But we can also use the symmetry of this inequality. For example, without loss of generality we can assume that $a\ge c$ and $b\ge d$, so $a\in [c,\infty)$, $b\in [d,\infty)$.


```python
newproof()
prove(makesubs(formula,'[c,oo],[d,oo]'))
```


Substitute $a\to c + e$



Substitute $b\to d + f$



numerator: $c^{2} e^{2} - c^{2} e f + c^{2} f^{2} + 2 c d e^{2} + 2 c d f^{2} + c e^{3} + c e f^{2} + c f^{3} + d^{2} e^{2} + d^{2} e f + d^{2} f^{2} + d e^{3} + d e^{2} f + 2 d e f^{2} + d f^{3} + e^{2} f^{2} + e f^{3}$



denominator: $c^{4} + 4 c^{3} d + 2 c^{3} e + 2 c^{3} f + 6 c^{2} d^{2} + 6 c^{2} d e + 6 c^{2} d f + c^{2} e^{2} + 3 c^{2} e f + c^{2} f^{2} + 4 c d^{3} + 6 c d^{2} e + 6 c d^{2} f + 2 c d e^{2} + 6 c d e f + 2 c d f^{2} + c e^{2} f + c e f^{2} + d^{4} + 2 d^{3} e + 2 d^{3} f + d^{2} e^{2} + 3 d^{2} e f + d^{2} f^{2} + d e^{2} f + d e f^{2}$



status: 0



From weighted AM-GM inequality:



Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again.



$$ c^{2} e f \le c^{2} e^{2}+c^{2} f^{2}+2 c d e^{2}+2 c d f^{2}+c e^{3}+c e f^{2}+c f^{3}+d^{2} e^{2}+d^{2} e f+d^{2} f^{2}+d e^{3}+d e^{2} f+2 d e f^{2}+d f^{3}+e^{2} f^{2}+e f^{3} $$





    -1




```python
newproof()
prove(makesubs(formula,'[c,oo],[d,oo]')*2)
```


Substitute $a\to c + e$



Substitute $b\to d + f$



numerator: $2 c^{2} e^{2} - 2 c^{2} e f + 2 c^{2} f^{2} + 4 c d e^{2} + 4 c d f^{2} + 2 c e^{3} + 2 c e f^{2} + 2 c f^{3} + 2 d^{2} e^{2} + 2 d^{2} e f + 2 d^{2} f^{2} + 2 d e^{3} + 2 d e^{2} f + 4 d e f^{2} + 2 d f^{3} + 2 e^{2} f^{2} + 2 e f^{3}$



denominator: $c^{4} + 4 c^{3} d + 2 c^{3} e + 2 c^{3} f + 6 c^{2} d^{2} + 6 c^{2} d e + 6 c^{2} d f + c^{2} e^{2} + 3 c^{2} e f + c^{2} f^{2} + 4 c d^{3} + 6 c d^{2} e + 6 c d^{2} f + 2 c d e^{2} + 6 c d e f + 2 c d f^{2} + c e^{2} f + c e f^{2} + d^{4} + 2 d^{3} e + 2 d^{3} f + d^{2} e^{2} + 3 d^{2} e f + d^{2} f^{2} + d e^{2} f + d e f^{2}$



status: 0



From weighted AM-GM inequality:



$$2 c^{2} e f \le c^{2} e^{2}+c^{2} f^{2}$$



$$ 0 \le c^{2} e^{2}+c^{2} f^{2}+4 c d e^{2}+4 c d f^{2}+2 c e^{3}+2 c e f^{2}+2 c f^{3}+2 d^{2} e^{2}+2 d^{2} e f+2 d^{2} f^{2}+2 d e^{3}+2 d e^{2} f+4 d e f^{2}+2 d f^{3}+2 e^{2} f^{2}+2 e f^{3} $$



The sum of all inequalities gives us a proof of the inequality.





    0



It's a good idea to use intervals that are unbounded from one side (i.e. those which contain $\pm\infty$). In this problem we could assume that $a\in (0,c]$, $b\in (0,d]$ as well. But as you can see, in this case the proof is several times longer.


```python
newproof()
prove(makesubs(formula,'[0,c],[0,d]')*2)
```


Substitute $a\to c - \frac{c}{e + 1}$



Substitute $b\to d - \frac{d}{f + 1}$



numerator: $2 c^{4} e f^{3} + 6 c^{4} e f^{2} + 6 c^{4} e f + 2 c^{4} e - 2 c^{3} d e^{2} f^{2} - 4 c^{3} d e^{2} f - 2 c^{3} d e^{2} + 4 c^{3} d e f^{3} + 8 c^{3} d e f^{2} + 4 c^{3} d e f + 2 c^{3} d f^{3} + 4 c^{3} d f^{2} + 2 c^{3} d f + 2 c^{2} d^{2} e^{3} f + 2 c^{2} d^{2} e^{3} + 4 c^{2} d^{2} e^{2} f + 4 c^{2} d^{2} e^{2} + 2 c^{2} d^{2} e f^{3} + 4 c^{2} d^{2} e f^{2} + 6 c^{2} d^{2} e f + 4 c^{2} d^{2} e + 2 c^{2} d^{2} f^{3} + 4 c^{2} d^{2} f^{2} + 4 c^{2} d^{2} f + 2 c^{2} d^{2} + 4 c d^{3} e^{3} f + 2 c d^{3} e^{3} + 2 c d^{3} e^{2} f^{2} + 12 c d^{3} e^{2} f + 6 c d^{3} e^{2} + 4 c d^{3} e f^{2} + 12 c d^{3} e f + 6 c d^{3} e + 2 c d^{3} f^{2} + 4 c d^{3} f + 2 c d^{3} + 2 d^{4} e^{3} f + 6 d^{4} e^{2} f + 6 d^{4} e f + 2 d^{4} f$



denominator: $c^{4} e^{3} f^{3} + 3 c^{4} e^{3} f^{2} + 3 c^{4} e^{3} f + c^{4} e^{3} + c^{4} e^{2} f^{3} + 3 c^{4} e^{2} f^{2} + 3 c^{4} e^{2} f + c^{4} e^{2} + 4 c^{3} d e^{3} f^{3} + 10 c^{3} d e^{3} f^{2} + 8 c^{3} d e^{3} f + 2 c^{3} d e^{3} + 6 c^{3} d e^{2} f^{3} + 15 c^{3} d e^{2} f^{2} + 12 c^{3} d e^{2} f + 3 c^{3} d e^{2} + 2 c^{3} d e f^{3} + 5 c^{3} d e f^{2} + 4 c^{3} d e f + c^{3} d e + 6 c^{2} d^{2} e^{3} f^{3} + 12 c^{2} d^{2} e^{3} f^{2} + 7 c^{2} d^{2} e^{3} f + c^{2} d^{2} e^{3} + 12 c^{2} d^{2} e^{2} f^{3} + 24 c^{2} d^{2} e^{2} f^{2} + 14 c^{2} d^{2} e^{2} f + 2 c^{2} d^{2} e^{2} + 7 c^{2} d^{2} e f^{3} + 14 c^{2} d^{2} e f^{2} + 8 c^{2} d^{2} e f + c^{2} d^{2} e + c^{2} d^{2} f^{3} + 2 c^{2} d^{2} f^{2} + c^{2} d^{2} f + 4 c d^{3} e^{3} f^{3} + 6 c d^{3} e^{3} f^{2} + 2 c d^{3} e^{3} f + 10 c d^{3} e^{2} f^{3} + 15 c d^{3} e^{2} f^{2} + 5 c d^{3} e^{2} f + 8 c d^{3} e f^{3} + 12 c d^{3} e f^{2} + 4 c d^{3} e f + 2 c d^{3} f^{3} + 3 c d^{3} f^{2} + c d^{3} f + d^{4} e^{3} f^{3} + d^{4} e^{3} f^{2} + 3 d^{4} e^{2} f^{3} + 3 d^{4} e^{2} f^{2} + 3 d^{4} e f^{3} + 3 d^{4} e f^{2} + d^{4} f^{3} + d^{4} f^{2}$



status: 0



From weighted AM-GM inequality:



$$2 c^{3} d e^{2} f^{2} \le c^{4} e f^{3}+c^{2} d^{2} e^{3} f$$



$$2 c^{3} d e^{2} \le c^{4} e+c^{2} d^{2} e^{3}$$



$$4 c^{3} d e^{2} f \le c^{4} e f^{3}+c^{4} e+c^{2} d^{2} e^{3} f+c^{2} d^{2} e^{3}$$



$$ 0 \le 6 c^{4} e f^{2}+6 c^{4} e f+4 c^{3} d e f^{3}+8 c^{3} d e f^{2}+4 c^{3} d e f+2 c^{3} d f^{3}+4 c^{3} d f^{2}+2 c^{3} d f+4 c^{2} d^{2} e^{2} f+4 c^{2} d^{2} e^{2}+2 c^{2} d^{2} e f^{3}+4 c^{2} d^{2} e f^{2}+6 c^{2} d^{2} e f+4 c^{2} d^{2} e+2 c^{2} d^{2} f^{3}+4 c^{2} d^{2} f^{2}+4 c^{2} d^{2} f+2 c^{2} d^{2}+4 c d^{3} e^{3} f+2 c d^{3} e^{3}+2 c d^{3} e^{2} f^{2}+12 c d^{3} e^{2} f+6 c d^{3} e^{2}+4 c d^{3} e f^{2}+12 c d^{3} e f+6 c d^{3} e+2 c d^{3} f^{2}+4 c d^{3} f+2 c d^{3}+2 d^{4} e^{3} f+6 d^{4} e^{2} f+6 d^{4} e f+2 d^{4} f $$



The sum of all inequalities gives us a proof of the inequality.





    0



Function `powerprove` is a shortcut for splitting domain $R_+^n$ on several subdomains and proving the inequality for each of them. This function uses $2^n$ of $n$-dimensional intervals with a common point (by default it's $(1,1,...,1)$), where $n$ is a number of variables. Here there are two examples of using it. As you can see, proofs are very long.


```python
newproof()
#this is equivalent to
#prove(makesubs('(x-1)^4','[1,oo]'))
#prove(makesubs('(x-1)^4','[1,0]')) 
#you can write ends of interval in any order, so [1,0] is the same as [0,1]
#but the substitution is slightly simpler when 0 is on the right side
powerprove('(x-1)^4')
```


numerator: $x^{4} - 4 x^{3} + 6 x^{2} - 4 x + 1$



denominator: $1$



_______________________



Substitute $x\to 1+a$



Numerator after substitutions: $a^{4}$



status: 0



$$ 0 \le a^{4} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $x\to 1/(1+b)$



Numerator after substitutions: $b^{4}$



status: 0



$$ 0 \le b^{4} $$



The sum of all inequalities gives us a proof of the inequality.





    Counter({0: 2})




```python
newproof()
formula=Sm('-(3a+2b+c)(2a^3+3b^2+6c+1)+(4a+4b+4c)(a^4+b^3+c^2+3)')
#this is equivalent to
#prove(makesubs(formula,'[1,oo],[1,oo],[1,oo]'))
#prove(makesubs(formula,'[1,0],[1,oo],[1,oo]'))
#prove(makesubs(formula,'[1,oo],[1,0],[1,oo]'))
#prove(makesubs(formula,'[1,0],[1,0],[1,oo]'))
#prove(makesubs(formula,'[1,oo],[1,oo],[1,0]'))
#prove(makesubs(formula,'[1,0],[1,oo],[1,0]'))
#prove(makesubs(formula,'[1,oo],[1,0],[1,0]'))
#prove(makesubs(formula,'[1,0],[1,0],[1,0]'))
powerprove(formula)
```


numerator: $4 a^{5} + 4 a^{4} b + 4 a^{4} c - 6 a^{4} - 4 a^{3} b - 2 a^{3} c + 4 a b^{3} - 9 a b^{2} + 4 a c^{2} - 18 a c + 9 a + 4 b^{4} + 4 b^{3} c - 6 b^{3} - 3 b^{2} c + 4 b c^{2} - 12 b c + 10 b + 4 c^{3} - 6 c^{2} + 11 c$



denominator: $1$



_______________________



Substitute $a\to 1+d,b\to 1+e,c\to 1+f$



Numerator after substitutions: $4 d^{5} + 4 d^{4} e + 4 d^{4} f + 22 d^{4} + 12 d^{3} e + 14 d^{3} f + 42 d^{3} + 12 d^{2} e + 18 d^{2} f + 34 d^{2} + 4 d e^{3} + 3 d e^{2} - 2 d e + 4 d f^{2} + 4 e^{4} + 4 e^{3} f + 18 e^{3} + 9 e^{2} f + 18 e^{2} + 4 e f^{2} + 2 e f + 4 f^{3} + 14 f^{2}$



status: 0



From weighted AM-GM inequality:



$$2 d e \le d^{2}+e^{2}$$



$$ 0 \le 4 d^{5}+4 d^{4} e+4 d^{4} f+22 d^{4}+12 d^{3} e+14 d^{3} f+42 d^{3}+12 d^{2} e+18 d^{2} f+33 d^{2}+4 d e^{3}+3 d e^{2}+4 d f^{2}+4 e^{4}+4 e^{3} f+18 e^{3}+9 e^{2} f+17 e^{2}+4 e f^{2}+2 e f+4 f^{3}+14 f^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1/(1+g),b\to 1+h,c\to 1+i$



Numerator after substitutions: $4 g^{5} h^{4} + 4 g^{5} h^{3} i + 14 g^{5} h^{3} + 9 g^{5} h^{2} i + 15 g^{5} h^{2} + 4 g^{5} h i^{2} + 2 g^{5} h i + 6 g^{5} h + 4 g^{5} i^{3} + 10 g^{5} i^{2} + 8 g^{5} i + 10 g^{5} + 20 g^{4} h^{4} + 20 g^{4} h^{3} i + 74 g^{4} h^{3} + 45 g^{4} h^{2} i + 78 g^{4} h^{2} + 20 g^{4} h i^{2} + 10 g^{4} h i + 24 g^{4} h + 20 g^{4} i^{3} + 54 g^{4} i^{2} + 30 g^{4} i + 40 g^{4} + 40 g^{3} h^{4} + 40 g^{3} h^{3} i + 156 g^{3} h^{3} + 90 g^{3} h^{2} i + 162 g^{3} h^{2} + 40 g^{3} h i^{2} + 20 g^{3} h i + 36 g^{3} h + 40 g^{3} i^{3} + 116 g^{3} i^{2} + 40 g^{3} i + 60 g^{3} + 40 g^{2} h^{4} + 40 g^{2} h^{3} i + 164 g^{2} h^{3} + 90 g^{2} h^{2} i + 168 g^{2} h^{2} + 40 g^{2} h i^{2} + 20 g^{2} h i + 20 g^{2} h + 40 g^{2} i^{3} + 124 g^{2} i^{2} + 18 g^{2} i + 34 g^{2} + 20 g h^{4} + 20 g h^{3} i + 86 g h^{3} + 45 g h^{2} i + 87 g h^{2} + 20 g h i^{2} + 10 g h i + 2 g h + 20 g i^{3} + 66 g i^{2} + 4 h^{4} + 4 h^{3} i + 18 h^{3} + 9 h^{2} i + 18 h^{2} + 4 h i^{2} + 2 h i + 4 i^{3} + 14 i^{2}$



status: 0



$$ 0 \le 4 g^{5} h^{4}+4 g^{5} h^{3} i+14 g^{5} h^{3}+9 g^{5} h^{2} i+15 g^{5} h^{2}+4 g^{5} h i^{2}+2 g^{5} h i+6 g^{5} h+4 g^{5} i^{3}+10 g^{5} i^{2}+8 g^{5} i+10 g^{5}+20 g^{4} h^{4}+20 g^{4} h^{3} i+74 g^{4} h^{3}+45 g^{4} h^{2} i+78 g^{4} h^{2}+20 g^{4} h i^{2}+10 g^{4} h i+24 g^{4} h+20 g^{4} i^{3}+54 g^{4} i^{2}+30 g^{4} i+40 g^{4}+40 g^{3} h^{4}+40 g^{3} h^{3} i+156 g^{3} h^{3}+90 g^{3} h^{2} i+162 g^{3} h^{2}+40 g^{3} h i^{2}+20 g^{3} h i+36 g^{3} h+40 g^{3} i^{3}+116 g^{3} i^{2}+40 g^{3} i+60 g^{3}+40 g^{2} h^{4}+40 g^{2} h^{3} i+164 g^{2} h^{3}+90 g^{2} h^{2} i+168 g^{2} h^{2}+40 g^{2} h i^{2}+20 g^{2} h i+20 g^{2} h+40 g^{2} i^{3}+124 g^{2} i^{2}+18 g^{2} i+34 g^{2}+20 g h^{4}+20 g h^{3} i+86 g h^{3}+45 g h^{2} i+87 g h^{2}+20 g h i^{2}+10 g h i+2 g h+20 g i^{3}+66 g i^{2}+4 h^{4}+4 h^{3} i+18 h^{3}+9 h^{2} i+18 h^{2}+4 h i^{2}+2 h i+4 i^{3}+14 i^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1+j,b\to 1/(1+k),c\to 1+l$



Numerator after substitutions: $4 j^{5} k^{4} + 16 j^{5} k^{3} + 24 j^{5} k^{2} + 16 j^{5} k + 4 j^{5} + 4 j^{4} k^{4} l + 18 j^{4} k^{4} + 16 j^{4} k^{3} l + 76 j^{4} k^{3} + 24 j^{4} k^{2} l + 120 j^{4} k^{2} + 16 j^{4} k l + 84 j^{4} k + 4 j^{4} l + 22 j^{4} + 14 j^{3} k^{4} l + 30 j^{3} k^{4} + 56 j^{3} k^{3} l + 132 j^{3} k^{3} + 84 j^{3} k^{2} l + 216 j^{3} k^{2} + 56 j^{3} k l + 156 j^{3} k + 14 j^{3} l + 42 j^{3} + 18 j^{2} k^{4} l + 22 j^{2} k^{4} + 72 j^{2} k^{3} l + 100 j^{2} k^{3} + 108 j^{2} k^{2} l + 168 j^{2} k^{2} + 72 j^{2} k l + 124 j^{2} k + 18 j^{2} l + 34 j^{2} + 4 j k^{4} l^{2} + j k^{4} + 16 j k^{3} l^{2} + 8 j k^{3} + 24 j k^{2} l^{2} + 9 j k^{2} + 16 j k l^{2} + 2 j k + 4 j l^{2} + 4 k^{4} l^{3} + 10 k^{4} l^{2} + 3 k^{4} l + 4 k^{4} + 16 k^{3} l^{3} + 44 k^{3} l^{2} + 8 k^{3} l + 18 k^{3} + 24 k^{2} l^{3} + 72 k^{2} l^{2} + 3 k^{2} l + 18 k^{2} + 16 k l^{3} + 52 k l^{2} - 2 k l + 4 l^{3} + 14 l^{2}$



status: 0



From weighted AM-GM inequality:



$$2 k l \le k^{2}+l^{2}$$



$$ 0 \le 4 j^{5} k^{4}+16 j^{5} k^{3}+24 j^{5} k^{2}+16 j^{5} k+4 j^{5}+4 j^{4} k^{4} l+18 j^{4} k^{4}+16 j^{4} k^{3} l+76 j^{4} k^{3}+24 j^{4} k^{2} l+120 j^{4} k^{2}+16 j^{4} k l+84 j^{4} k+4 j^{4} l+22 j^{4}+14 j^{3} k^{4} l+30 j^{3} k^{4}+56 j^{3} k^{3} l+132 j^{3} k^{3}+84 j^{3} k^{2} l+216 j^{3} k^{2}+56 j^{3} k l+156 j^{3} k+14 j^{3} l+42 j^{3}+18 j^{2} k^{4} l+22 j^{2} k^{4}+72 j^{2} k^{3} l+100 j^{2} k^{3}+108 j^{2} k^{2} l+168 j^{2} k^{2}+72 j^{2} k l+124 j^{2} k+18 j^{2} l+34 j^{2}+4 j k^{4} l^{2}+j k^{4}+16 j k^{3} l^{2}+8 j k^{3}+24 j k^{2} l^{2}+9 j k^{2}+16 j k l^{2}+2 j k+4 j l^{2}+4 k^{4} l^{3}+10 k^{4} l^{2}+3 k^{4} l+4 k^{4}+16 k^{3} l^{3}+44 k^{3} l^{2}+8 k^{3} l+18 k^{3}+24 k^{2} l^{3}+72 k^{2} l^{2}+3 k^{2} l+17 k^{2}+16 k l^{3}+52 k l^{2}+4 l^{3}+13 l^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1/(1+m),b\to 1/(1+n),c\to 1+o$



Numerator after substitutions: $4 m^{5} n^{4} o^{3} + 6 m^{5} n^{4} o^{2} + 11 m^{5} n^{4} o + 9 m^{5} n^{4} + 16 m^{5} n^{3} o^{3} + 28 m^{5} n^{3} o^{2} + 40 m^{5} n^{3} o + 38 m^{5} n^{3} + 24 m^{5} n^{2} o^{3} + 48 m^{5} n^{2} o^{2} + 51 m^{5} n^{2} o + 57 m^{5} n^{2} + 16 m^{5} n o^{3} + 36 m^{5} n o^{2} + 30 m^{5} n o + 34 m^{5} n + 4 m^{5} o^{3} + 10 m^{5} o^{2} + 8 m^{5} o + 10 m^{5} + 20 m^{4} n^{4} o^{3} + 34 m^{4} n^{4} o^{2} + 45 m^{4} n^{4} o + 40 m^{4} n^{4} + 80 m^{4} n^{3} o^{3} + 156 m^{4} n^{3} o^{2} + 160 m^{4} n^{3} o + 170 m^{4} n^{3} + 120 m^{4} n^{2} o^{3} + 264 m^{4} n^{2} o^{2} + 195 m^{4} n^{2} o + 246 m^{4} n^{2} + 80 m^{4} n o^{3} + 196 m^{4} n o^{2} + 110 m^{4} n o + 136 m^{4} n + 20 m^{4} o^{3} + 54 m^{4} o^{2} + 30 m^{4} o + 40 m^{4} + 40 m^{3} n^{4} o^{3} + 76 m^{3} n^{4} o^{2} + 70 m^{3} n^{4} o + 70 m^{3} n^{4} + 160 m^{3} n^{3} o^{3} + 344 m^{3} n^{3} o^{2} + 240 m^{3} n^{3} o + 300 m^{3} n^{3} + 240 m^{3} n^{2} o^{3} + 576 m^{3} n^{2} o^{2} + 270 m^{3} n^{2} o + 414 m^{3} n^{2} + 160 m^{3} n o^{3} + 424 m^{3} n o^{2} + 140 m^{3} n o + 204 m^{3} n + 40 m^{3} o^{3} + 116 m^{3} o^{2} + 40 m^{3} o + 60 m^{3} + 40 m^{2} n^{4} o^{3} + 84 m^{2} n^{4} o^{2} + 48 m^{2} n^{4} o + 58 m^{2} n^{4} + 160 m^{2} n^{3} o^{3} + 376 m^{2} n^{3} o^{2} + 152 m^{2} n^{3} o + 248 m^{2} n^{3} + 240 m^{2} n^{2} o^{3} + 624 m^{2} n^{2} o^{2} + 138 m^{2} n^{2} o + 312 m^{2} n^{2} + 160 m^{2} n o^{3} + 456 m^{2} n o^{2} + 52 m^{2} n o + 116 m^{2} n + 40 m^{2} o^{3} + 124 m^{2} o^{2} + 18 m^{2} o + 34 m^{2} + 20 m n^{4} o^{3} + 46 m n^{4} o^{2} + 15 m n^{4} o + 19 m n^{4} + 80 m n^{3} o^{3} + 204 m n^{3} o^{2} + 40 m n^{3} o + 82 m n^{3} + 120 m n^{2} o^{3} + 336 m n^{2} o^{2} + 15 m n^{2} o + 81 m n^{2} + 80 m n o^{3} + 244 m n o^{2} - 10 m n o - 2 m n + 20 m o^{3} + 66 m o^{2} + 4 n^{4} o^{3} + 10 n^{4} o^{2} + 3 n^{4} o + 4 n^{4} + 16 n^{3} o^{3} + 44 n^{3} o^{2} + 8 n^{3} o + 18 n^{3} + 24 n^{2} o^{3} + 72 n^{2} o^{2} + 3 n^{2} o + 18 n^{2} + 16 n o^{3} + 52 n o^{2} - 2 n o + 4 o^{3} + 14 o^{2}$



status: 0



From weighted AM-GM inequality:



$$2 m n \le m^{2}+n^{2}$$



$$2 n o \le n^{2}+o^{2}$$



$$10 m n o \le 2 m^{2}+2 m n^{2} o+4 m o^{2}+2 n^{3}$$



$$ 0 \le 4 m^{5} n^{4} o^{3}+6 m^{5} n^{4} o^{2}+11 m^{5} n^{4} o+9 m^{5} n^{4}+16 m^{5} n^{3} o^{3}+28 m^{5} n^{3} o^{2}+40 m^{5} n^{3} o+38 m^{5} n^{3}+24 m^{5} n^{2} o^{3}+48 m^{5} n^{2} o^{2}+51 m^{5} n^{2} o+57 m^{5} n^{2}+16 m^{5} n o^{3}+36 m^{5} n o^{2}+30 m^{5} n o+34 m^{5} n+4 m^{5} o^{3}+10 m^{5} o^{2}+8 m^{5} o+10 m^{5}+20 m^{4} n^{4} o^{3}+34 m^{4} n^{4} o^{2}+45 m^{4} n^{4} o+40 m^{4} n^{4}+80 m^{4} n^{3} o^{3}+156 m^{4} n^{3} o^{2}+160 m^{4} n^{3} o+170 m^{4} n^{3}+120 m^{4} n^{2} o^{3}+264 m^{4} n^{2} o^{2}+195 m^{4} n^{2} o+246 m^{4} n^{2}+80 m^{4} n o^{3}+196 m^{4} n o^{2}+110 m^{4} n o+136 m^{4} n+20 m^{4} o^{3}+54 m^{4} o^{2}+30 m^{4} o+40 m^{4}+40 m^{3} n^{4} o^{3}+76 m^{3} n^{4} o^{2}+70 m^{3} n^{4} o+70 m^{3} n^{4}+160 m^{3} n^{3} o^{3}+344 m^{3} n^{3} o^{2}+240 m^{3} n^{3} o+300 m^{3} n^{3}+240 m^{3} n^{2} o^{3}+576 m^{3} n^{2} o^{2}+270 m^{3} n^{2} o+414 m^{3} n^{2}+160 m^{3} n o^{3}+424 m^{3} n o^{2}+140 m^{3} n o+204 m^{3} n+40 m^{3} o^{3}+116 m^{3} o^{2}+40 m^{3} o+60 m^{3}+40 m^{2} n^{4} o^{3}+84 m^{2} n^{4} o^{2}+48 m^{2} n^{4} o+58 m^{2} n^{4}+160 m^{2} n^{3} o^{3}+376 m^{2} n^{3} o^{2}+152 m^{2} n^{3} o+248 m^{2} n^{3}+240 m^{2} n^{2} o^{3}+624 m^{2} n^{2} o^{2}+138 m^{2} n^{2} o+312 m^{2} n^{2}+160 m^{2} n o^{3}+456 m^{2} n o^{2}+52 m^{2} n o+116 m^{2} n+40 m^{2} o^{3}+124 m^{2} o^{2}+18 m^{2} o+31 m^{2}+20 m n^{4} o^{3}+46 m n^{4} o^{2}+15 m n^{4} o+19 m n^{4}+80 m n^{3} o^{3}+204 m n^{3} o^{2}+40 m n^{3} o+82 m n^{3}+120 m n^{2} o^{3}+336 m n^{2} o^{2}+13 m n^{2} o+81 m n^{2}+80 m n o^{3}+244 m n o^{2}+20 m o^{3}+62 m o^{2}+4 n^{4} o^{3}+10 n^{4} o^{2}+3 n^{4} o+4 n^{4}+16 n^{3} o^{3}+44 n^{3} o^{2}+8 n^{3} o+16 n^{3}+24 n^{2} o^{3}+72 n^{2} o^{2}+3 n^{2} o+16 n^{2}+16 n o^{3}+52 n o^{2}+4 o^{3}+13 o^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1+p,b\to 1+q,c\to 1/(1+r)$



Numerator after substitutions: $4 p^{5} r^{3} + 12 p^{5} r^{2} + 12 p^{5} r + 4 p^{5} + 4 p^{4} q r^{3} + 12 p^{4} q r^{2} + 12 p^{4} q r + 4 p^{4} q + 18 p^{4} r^{3} + 58 p^{4} r^{2} + 62 p^{4} r + 22 p^{4} + 12 p^{3} q r^{3} + 36 p^{3} q r^{2} + 36 p^{3} q r + 12 p^{3} q + 28 p^{3} r^{3} + 98 p^{3} r^{2} + 112 p^{3} r + 42 p^{3} + 12 p^{2} q r^{3} + 36 p^{2} q r^{2} + 36 p^{2} q r + 12 p^{2} q + 16 p^{2} r^{3} + 66 p^{2} r^{2} + 84 p^{2} r + 34 p^{2} + 4 p q^{3} r^{3} + 12 p q^{3} r^{2} + 12 p q^{3} r + 4 p q^{3} + 3 p q^{2} r^{3} + 9 p q^{2} r^{2} + 9 p q^{2} r + 3 p q^{2} - 2 p q r^{3} - 6 p q r^{2} - 6 p q r - 2 p q + 4 p r^{3} + 4 p r^{2} + 4 q^{4} r^{3} + 12 q^{4} r^{2} + 12 q^{4} r + 4 q^{4} + 14 q^{3} r^{3} + 46 q^{3} r^{2} + 50 q^{3} r + 18 q^{3} + 9 q^{2} r^{3} + 36 q^{2} r^{2} + 45 q^{2} r + 18 q^{2} + 2 q r^{3} - 2 q r + 10 r^{3} + 14 r^{2}$



status: 0



From weighted AM-GM inequality:



$$2 p q r^{3} \le p^{2} q r^{3}+q r^{3}$$



$$2 p q \le p^{2}+q^{2}$$



$$2 q r \le q^{2}+r^{2}$$



$$6 p q r \le 2 p^{3} q+2 q^{2} r+2 r^{2}$$



$$6 p q r^{2} \le 2 p q^{2} r^{3}+p q^{2}+3 p r^{2}$$



$$ 0 \le 4 p^{5} r^{3}+12 p^{5} r^{2}+12 p^{5} r+4 p^{5}+4 p^{4} q r^{3}+12 p^{4} q r^{2}+12 p^{4} q r+4 p^{4} q+18 p^{4} r^{3}+58 p^{4} r^{2}+62 p^{4} r+22 p^{4}+12 p^{3} q r^{3}+36 p^{3} q r^{2}+36 p^{3} q r+10 p^{3} q+28 p^{3} r^{3}+98 p^{3} r^{2}+112 p^{3} r+42 p^{3}+11 p^{2} q r^{3}+36 p^{2} q r^{2}+36 p^{2} q r+12 p^{2} q+16 p^{2} r^{3}+66 p^{2} r^{2}+84 p^{2} r+33 p^{2}+4 p q^{3} r^{3}+12 p q^{3} r^{2}+12 p q^{3} r+4 p q^{3}+p q^{2} r^{3}+9 p q^{2} r^{2}+9 p q^{2} r+2 p q^{2}+4 p r^{3}+p r^{2}+4 q^{4} r^{3}+12 q^{4} r^{2}+12 q^{4} r+4 q^{4}+14 q^{3} r^{3}+46 q^{3} r^{2}+50 q^{3} r+18 q^{3}+9 q^{2} r^{3}+36 q^{2} r^{2}+43 q^{2} r+16 q^{2}+q r^{3}+10 r^{3}+11 r^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1/(1+s),b\to 1+t,c\to 1/(1+u)$



Numerator after substitutions: $4 s^{5} t^{4} u^{3} + 12 s^{5} t^{4} u^{2} + 12 s^{5} t^{4} u + 4 s^{5} t^{4} + 10 s^{5} t^{3} u^{3} + 34 s^{5} t^{3} u^{2} + 38 s^{5} t^{3} u + 14 s^{5} t^{3} + 6 s^{5} t^{2} u^{3} + 27 s^{5} t^{2} u^{2} + 36 s^{5} t^{2} u + 15 s^{5} t^{2} + 8 s^{5} t u^{3} + 18 s^{5} t u^{2} + 16 s^{5} t u + 6 s^{5} t + 8 s^{5} u^{3} + 24 s^{5} u^{2} + 22 s^{5} u + 10 s^{5} + 20 s^{4} t^{4} u^{3} + 60 s^{4} t^{4} u^{2} + 60 s^{4} t^{4} u + 20 s^{4} t^{4} + 54 s^{4} t^{3} u^{3} + 182 s^{4} t^{3} u^{2} + 202 s^{4} t^{3} u + 74 s^{4} t^{3} + 33 s^{4} t^{2} u^{3} + 144 s^{4} t^{2} u^{2} + 189 s^{4} t^{2} u + 78 s^{4} t^{2} + 34 s^{4} t u^{3} + 72 s^{4} t u^{2} + 62 s^{4} t u + 24 s^{4} t + 44 s^{4} u^{3} + 114 s^{4} u^{2} + 90 s^{4} u + 40 s^{4} + 40 s^{3} t^{4} u^{3} + 120 s^{3} t^{4} u^{2} + 120 s^{3} t^{4} u + 40 s^{3} t^{4} + 116 s^{3} t^{3} u^{3} + 388 s^{3} t^{3} u^{2} + 428 s^{3} t^{3} u + 156 s^{3} t^{3} + 72 s^{3} t^{2} u^{3} + 306 s^{3} t^{2} u^{2} + 396 s^{3} t^{2} u + 162 s^{3} t^{2} + 56 s^{3} t u^{3} + 108 s^{3} t u^{2} + 88 s^{3} t u + 36 s^{3} t + 96 s^{3} u^{3} + 216 s^{3} u^{2} + 140 s^{3} u + 60 s^{3} + 40 s^{2} t^{4} u^{3} + 120 s^{2} t^{4} u^{2} + 120 s^{2} t^{4} u + 40 s^{2} t^{4} + 124 s^{2} t^{3} u^{3} + 412 s^{2} t^{3} u^{2} + 452 s^{2} t^{3} u + 164 s^{2} t^{3} + 78 s^{2} t^{2} u^{3} + 324 s^{2} t^{2} u^{2} + 414 s^{2} t^{2} u + 168 s^{2} t^{2} + 40 s^{2} t u^{3} + 60 s^{2} t u^{2} + 40 s^{2} t u + 20 s^{2} t + 100 s^{2} u^{3} + 190 s^{2} u^{2} + 84 s^{2} u + 34 s^{2} + 20 s t^{4} u^{3} + 60 s t^{4} u^{2} + 60 s t^{4} u + 20 s t^{4} + 66 s t^{3} u^{3} + 218 s t^{3} u^{2} + 238 s t^{3} u + 86 s t^{3} + 42 s t^{2} u^{3} + 171 s t^{2} u^{2} + 216 s t^{2} u + 87 s t^{2} + 12 s t u^{3} + 6 s t u^{2} - 4 s t u + 2 s t + 46 s u^{3} + 66 s u^{2} + 4 t^{4} u^{3} + 12 t^{4} u^{2} + 12 t^{4} u + 4 t^{4} + 14 t^{3} u^{3} + 46 t^{3} u^{2} + 50 t^{3} u + 18 t^{3} + 9 t^{2} u^{3} + 36 t^{2} u^{2} + 45 t^{2} u + 18 t^{2} + 2 t u^{3} - 2 t u + 10 u^{3} + 14 u^{2}$



status: 0



From weighted AM-GM inequality:



$$4 s t u \le s^{2} u^{2}+2 s t^{2}+u^{2}$$



$$2 t u \le t^{2}+u^{2}$$



$$ 0 \le 4 s^{5} t^{4} u^{3}+12 s^{5} t^{4} u^{2}+12 s^{5} t^{4} u+4 s^{5} t^{4}+10 s^{5} t^{3} u^{3}+34 s^{5} t^{3} u^{2}+38 s^{5} t^{3} u+14 s^{5} t^{3}+6 s^{5} t^{2} u^{3}+27 s^{5} t^{2} u^{2}+36 s^{5} t^{2} u+15 s^{5} t^{2}+8 s^{5} t u^{3}+18 s^{5} t u^{2}+16 s^{5} t u+6 s^{5} t+8 s^{5} u^{3}+24 s^{5} u^{2}+22 s^{5} u+10 s^{5}+20 s^{4} t^{4} u^{3}+60 s^{4} t^{4} u^{2}+60 s^{4} t^{4} u+20 s^{4} t^{4}+54 s^{4} t^{3} u^{3}+182 s^{4} t^{3} u^{2}+202 s^{4} t^{3} u+74 s^{4} t^{3}+33 s^{4} t^{2} u^{3}+144 s^{4} t^{2} u^{2}+189 s^{4} t^{2} u+78 s^{4} t^{2}+34 s^{4} t u^{3}+72 s^{4} t u^{2}+62 s^{4} t u+24 s^{4} t+44 s^{4} u^{3}+114 s^{4} u^{2}+90 s^{4} u+40 s^{4}+40 s^{3} t^{4} u^{3}+120 s^{3} t^{4} u^{2}+120 s^{3} t^{4} u+40 s^{3} t^{4}+116 s^{3} t^{3} u^{3}+388 s^{3} t^{3} u^{2}+428 s^{3} t^{3} u+156 s^{3} t^{3}+72 s^{3} t^{2} u^{3}+306 s^{3} t^{2} u^{2}+396 s^{3} t^{2} u+162 s^{3} t^{2}+56 s^{3} t u^{3}+108 s^{3} t u^{2}+88 s^{3} t u+36 s^{3} t+96 s^{3} u^{3}+216 s^{3} u^{2}+140 s^{3} u+60 s^{3}+40 s^{2} t^{4} u^{3}+120 s^{2} t^{4} u^{2}+120 s^{2} t^{4} u+40 s^{2} t^{4}+124 s^{2} t^{3} u^{3}+412 s^{2} t^{3} u^{2}+452 s^{2} t^{3} u+164 s^{2} t^{3}+78 s^{2} t^{2} u^{3}+324 s^{2} t^{2} u^{2}+414 s^{2} t^{2} u+168 s^{2} t^{2}+40 s^{2} t u^{3}+60 s^{2} t u^{2}+40 s^{2} t u+20 s^{2} t+100 s^{2} u^{3}+189 s^{2} u^{2}+84 s^{2} u+34 s^{2}+20 s t^{4} u^{3}+60 s t^{4} u^{2}+60 s t^{4} u+20 s t^{4}+66 s t^{3} u^{3}+218 s t^{3} u^{2}+238 s t^{3} u+86 s t^{3}+42 s t^{2} u^{3}+171 s t^{2} u^{2}+216 s t^{2} u+85 s t^{2}+12 s t u^{3}+6 s t u^{2}+2 s t+46 s u^{3}+66 s u^{2}+4 t^{4} u^{3}+12 t^{4} u^{2}+12 t^{4} u+4 t^{4}+14 t^{3} u^{3}+46 t^{3} u^{2}+50 t^{3} u+18 t^{3}+9 t^{2} u^{3}+36 t^{2} u^{2}+45 t^{2} u+17 t^{2}+2 t u^{3}+10 u^{3}+12 u^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1+v,b\to 1/(1+w),c\to 1/(1+x)$



Numerator after substitutions: $4 v^{5} w^{4} x^{3} + 12 v^{5} w^{4} x^{2} + 12 v^{5} w^{4} x + 4 v^{5} w^{4} + 16 v^{5} w^{3} x^{3} + 48 v^{5} w^{3} x^{2} + 48 v^{5} w^{3} x + 16 v^{5} w^{3} + 24 v^{5} w^{2} x^{3} + 72 v^{5} w^{2} x^{2} + 72 v^{5} w^{2} x + 24 v^{5} w^{2} + 16 v^{5} w x^{3} + 48 v^{5} w x^{2} + 48 v^{5} w x + 16 v^{5} w + 4 v^{5} x^{3} + 12 v^{5} x^{2} + 12 v^{5} x + 4 v^{5} + 14 v^{4} w^{4} x^{3} + 46 v^{4} w^{4} x^{2} + 50 v^{4} w^{4} x + 18 v^{4} w^{4} + 60 v^{4} w^{3} x^{3} + 196 v^{4} w^{3} x^{2} + 212 v^{4} w^{3} x + 76 v^{4} w^{3} + 96 v^{4} w^{2} x^{3} + 312 v^{4} w^{2} x^{2} + 336 v^{4} w^{2} x + 120 v^{4} w^{2} + 68 v^{4} w x^{3} + 220 v^{4} w x^{2} + 236 v^{4} w x + 84 v^{4} w + 18 v^{4} x^{3} + 58 v^{4} x^{2} + 62 v^{4} x + 22 v^{4} + 16 v^{3} w^{4} x^{3} + 62 v^{3} w^{4} x^{2} + 76 v^{3} w^{4} x + 30 v^{3} w^{4} + 76 v^{3} w^{3} x^{3} + 284 v^{3} w^{3} x^{2} + 340 v^{3} w^{3} x + 132 v^{3} w^{3} + 132 v^{3} w^{2} x^{3} + 480 v^{3} w^{2} x^{2} + 564 v^{3} w^{2} x + 216 v^{3} w^{2} + 100 v^{3} w x^{3} + 356 v^{3} w x^{2} + 412 v^{3} w x + 156 v^{3} w + 28 v^{3} x^{3} + 98 v^{3} x^{2} + 112 v^{3} x + 42 v^{3} + 4 v^{2} w^{4} x^{3} + 30 v^{2} w^{4} x^{2} + 48 v^{2} w^{4} x + 22 v^{2} w^{4} + 28 v^{2} w^{3} x^{3} + 156 v^{2} w^{3} x^{2} + 228 v^{2} w^{3} x + 100 v^{2} w^{3} + 60 v^{2} w^{2} x^{3} + 288 v^{2} w^{2} x^{2} + 396 v^{2} w^{2} x + 168 v^{2} w^{2} + 52 v^{2} w x^{3} + 228 v^{2} w x^{2} + 300 v^{2} w x + 124 v^{2} w + 16 v^{2} x^{3} + 66 v^{2} x^{2} + 84 v^{2} x + 34 v^{2} + 5 v w^{4} x^{3} + 7 v w^{4} x^{2} + 3 v w^{4} x + v w^{4} + 24 v w^{3} x^{3} + 40 v w^{3} x^{2} + 24 v w^{3} x + 8 v w^{3} + 33 v w^{2} x^{3} + 51 v w^{2} x^{2} + 27 v w^{2} x + 9 v w^{2} + 18 v w x^{3} + 22 v w x^{2} + 6 v w x + 2 v w + 4 v x^{3} + 4 v x^{2} + 7 w^{4} x^{3} + 16 w^{4} x^{2} + 9 w^{4} x + 4 w^{4} + 38 w^{3} x^{3} + 82 w^{3} x^{2} + 46 w^{3} x + 18 w^{3} + 63 w^{2} x^{3} + 120 w^{2} x^{2} + 51 w^{2} x + 18 w^{2} + 38 w x^{3} + 56 w x^{2} + 2 w x + 10 x^{3} + 14 x^{2}$



status: 0



$$ 0 \le 4 v^{5} w^{4} x^{3}+16 v^{5} w^{3} x^{3}+24 v^{5} w^{2} x^{3}+16 v^{5} w x^{3}+4 v^{5} x^{3}+14 v^{4} w^{4} x^{3}+60 v^{4} w^{3} x^{3}+96 v^{4} w^{2} x^{3}+68 v^{4} w x^{3}+18 v^{4} x^{3}+16 v^{3} w^{4} x^{3}+76 v^{3} w^{3} x^{3}+132 v^{3} w^{2} x^{3}+100 v^{3} w x^{3}+28 v^{3} x^{3}+4 v^{2} w^{4} x^{3}+28 v^{2} w^{3} x^{3}+60 v^{2} w^{2} x^{3}+52 v^{2} w x^{3}+16 v^{2} x^{3}+5 v w^{4} x^{3}+24 v w^{3} x^{3}+33 v w^{2} x^{3}+18 v w x^{3}+4 v x^{3}+7 w^{4} x^{3}+38 w^{3} x^{3}+63 w^{2} x^{3}+38 w x^{3}+10 x^{3}+12 v^{5} w^{4} x^{2}+48 v^{5} w^{3} x^{2}+72 v^{5} w^{2} x^{2}+48 v^{5} w x^{2}+12 v^{5} x^{2}+46 v^{4} w^{4} x^{2}+196 v^{4} w^{3} x^{2}+312 v^{4} w^{2} x^{2}+220 v^{4} w x^{2}+58 v^{4} x^{2}+62 v^{3} w^{4} x^{2}+284 v^{3} w^{3} x^{2}+480 v^{3} w^{2} x^{2}+356 v^{3} w x^{2}+98 v^{3} x^{2}+30 v^{2} w^{4} x^{2}+156 v^{2} w^{3} x^{2}+288 v^{2} w^{2} x^{2}+228 v^{2} w x^{2}+66 v^{2} x^{2}+7 v w^{4} x^{2}+40 v w^{3} x^{2}+51 v w^{2} x^{2}+22 v w x^{2}+4 v x^{2}+16 w^{4} x^{2}+82 w^{3} x^{2}+120 w^{2} x^{2}+56 w x^{2}+14 x^{2}+12 v^{5} w^{4} x+48 v^{5} w^{3} x+72 v^{5} w^{2} x+48 v^{5} w x+12 v^{5} x+50 v^{4} w^{4} x+212 v^{4} w^{3} x+336 v^{4} w^{2} x+236 v^{4} w x+62 v^{4} x+76 v^{3} w^{4} x+340 v^{3} w^{3} x+564 v^{3} w^{2} x+412 v^{3} w x+112 v^{3} x+48 v^{2} w^{4} x+228 v^{2} w^{3} x+396 v^{2} w^{2} x+300 v^{2} w x+84 v^{2} x+3 v w^{4} x+24 v w^{3} x+27 v w^{2} x+6 v w x+9 w^{4} x+46 w^{3} x+51 w^{2} x+2 w x+4 v^{5} w^{4}+16 v^{5} w^{3}+24 v^{5} w^{2}+16 v^{5} w+4 v^{5}+18 v^{4} w^{4}+76 v^{4} w^{3}+120 v^{4} w^{2}+84 v^{4} w+22 v^{4}+30 v^{3} w^{4}+132 v^{3} w^{3}+216 v^{3} w^{2}+156 v^{3} w+42 v^{3}+22 v^{2} w^{4}+100 v^{2} w^{3}+168 v^{2} w^{2}+124 v^{2} w+34 v^{2}+v w^{4}+8 v w^{3}+9 v w^{2}+2 v w+4 w^{4}+18 w^{3}+18 w^{2} $$



The sum of all inequalities gives us a proof of the inequality.



_______________________



Substitute $a\to 1/(1+y),b\to 1/(1+z),c\to 1/(1+a_{1})$



Numerator after substitutions: $10 a_{1}^{3} y^{5} z^{3} + 30 a_{1}^{3} y^{5} z^{2} + 24 a_{1}^{3} y^{5} z + 8 a_{1}^{3} y^{5} + 9 a_{1}^{3} y^{4} z^{4} + 86 a_{1}^{3} y^{4} z^{3} + 195 a_{1}^{3} y^{4} z^{2} + 142 a_{1}^{3} y^{4} z + 44 a_{1}^{3} y^{4} + 36 a_{1}^{3} y^{3} z^{4} + 244 a_{1}^{3} y^{3} z^{3} + 480 a_{1}^{3} y^{3} z^{2} + 328 a_{1}^{3} y^{3} z + 96 a_{1}^{3} y^{3} + 54 a_{1}^{3} y^{2} z^{4} + 312 a_{1}^{3} y^{2} z^{3} + 558 a_{1}^{3} y^{2} z^{2} + 360 a_{1}^{3} y^{2} z + 100 a_{1}^{3} y^{2} + 30 a_{1}^{3} y z^{4} + 166 a_{1}^{3} y z^{3} + 282 a_{1}^{3} y z^{2} + 172 a_{1}^{3} y z + 46 a_{1}^{3} y + 7 a_{1}^{3} z^{4} + 38 a_{1}^{3} z^{3} + 63 a_{1}^{3} z^{2} + 38 a_{1}^{3} z + 10 a_{1}^{3} + 11 a_{1}^{2} y^{5} z^{4} + 62 a_{1}^{2} y^{5} z^{3} + 117 a_{1}^{2} y^{5} z^{2} + 78 a_{1}^{2} y^{5} z + 24 a_{1}^{2} y^{5} + 64 a_{1}^{2} y^{4} z^{4} + 346 a_{1}^{2} y^{4} z^{3} + 612 a_{1}^{2} y^{4} z^{2} + 384 a_{1}^{2} y^{4} z + 114 a_{1}^{2} y^{4} + 146 a_{1}^{2} y^{3} z^{4} + 764 a_{1}^{2} y^{3} z^{3} + 1278 a_{1}^{2} y^{3} z^{2} + 756 a_{1}^{2} y^{3} z + 216 a_{1}^{2} y^{3} + 162 a_{1}^{2} y^{2} z^{4} + 816 a_{1}^{2} y^{2} z^{3} + 1284 a_{1}^{2} y^{2} z^{2} + 700 a_{1}^{2} y^{2} z + 190 a_{1}^{2} y^{2} + 73 a_{1}^{2} y z^{4} + 370 a_{1}^{2} y z^{3} + 549 a_{1}^{2} y z^{2} + 258 a_{1}^{2} y z + 66 a_{1}^{2} y + 16 a_{1}^{2} z^{4} + 82 a_{1}^{2} z^{3} + 120 a_{1}^{2} z^{2} + 56 a_{1}^{2} z + 14 a_{1}^{2} + 16 a_{1} y^{5} z^{4} + 74 a_{1} y^{5} z^{3} + 120 a_{1} y^{5} z^{2} + 72 a_{1} y^{5} z + 22 a_{1} y^{5} + 75 a_{1} y^{4} z^{4} + 350 a_{1} y^{4} z^{3} + 543 a_{1} y^{4} z^{2} + 298 a_{1} y^{4} z + 90 a_{1} y^{4} + 140 a_{1} y^{3} z^{4} + 660 a_{1} y^{3} z^{3} + 972 a_{1} y^{3} z^{2} + 472 a_{1} y^{3} z + 140 a_{1} y^{3} + 126 a_{1} y^{2} z^{4} + 592 a_{1} y^{2} z^{3} + 798 a_{1} y^{2} z^{2} + 296 a_{1} y^{2} z + 84 a_{1} y^{2} + 42 a_{1} y z^{4} + 206 a_{1} y z^{3} + 228 a_{1} y z^{2} + 4 a_{1} y z + 9 a_{1} z^{4} + 46 a_{1} z^{3} + 51 a_{1} z^{2} + 2 a_{1} z + 9 y^{5} z^{4} + 38 y^{5} z^{3} + 57 y^{5} z^{2} + 34 y^{5} z + 10 y^{5} + 40 y^{4} z^{4} + 170 y^{4} z^{3} + 246 y^{4} z^{2} + 136 y^{4} z + 40 y^{4} + 70 y^{3} z^{4} + 300 y^{3} z^{3} + 414 y^{3} z^{2} + 204 y^{3} z + 60 y^{3} + 58 y^{2} z^{4} + 248 y^{2} z^{3} + 312 y^{2} z^{2} + 116 y^{2} z + 34 y^{2} + 19 y z^{4} + 82 y z^{3} + 81 y z^{2} - 2 y z + 4 z^{4} + 18 z^{3} + 18 z^{2}$



status: 0



From weighted AM-GM inequality:



$$2 y z \le y^{2}+z^{2}$$



$$ 0 \le 11 a_{1}^{2} y^{5} z^{4}+16 a_{1} y^{5} z^{4}+9 y^{5} z^{4}+10 a_{1}^{3} y^{5} z^{3}+62 a_{1}^{2} y^{5} z^{3}+74 a_{1} y^{5} z^{3}+38 y^{5} z^{3}+30 a_{1}^{3} y^{5} z^{2}+117 a_{1}^{2} y^{5} z^{2}+120 a_{1} y^{5} z^{2}+57 y^{5} z^{2}+24 a_{1}^{3} y^{5} z+78 a_{1}^{2} y^{5} z+72 a_{1} y^{5} z+34 y^{5} z+8 a_{1}^{3} y^{5}+24 a_{1}^{2} y^{5}+22 a_{1} y^{5}+10 y^{5}+9 a_{1}^{3} y^{4} z^{4}+64 a_{1}^{2} y^{4} z^{4}+75 a_{1} y^{4} z^{4}+40 y^{4} z^{4}+86 a_{1}^{3} y^{4} z^{3}+346 a_{1}^{2} y^{4} z^{3}+350 a_{1} y^{4} z^{3}+170 y^{4} z^{3}+195 a_{1}^{3} y^{4} z^{2}+612 a_{1}^{2} y^{4} z^{2}+543 a_{1} y^{4} z^{2}+246 y^{4} z^{2}+142 a_{1}^{3} y^{4} z+384 a_{1}^{2} y^{4} z+298 a_{1} y^{4} z+136 y^{4} z+44 a_{1}^{3} y^{4}+114 a_{1}^{2} y^{4}+90 a_{1} y^{4}+40 y^{4}+36 a_{1}^{3} y^{3} z^{4}+146 a_{1}^{2} y^{3} z^{4}+140 a_{1} y^{3} z^{4}+70 y^{3} z^{4}+244 a_{1}^{3} y^{3} z^{3}+764 a_{1}^{2} y^{3} z^{3}+660 a_{1} y^{3} z^{3}+300 y^{3} z^{3}+480 a_{1}^{3} y^{3} z^{2}+1278 a_{1}^{2} y^{3} z^{2}+972 a_{1} y^{3} z^{2}+414 y^{3} z^{2}+328 a_{1}^{3} y^{3} z+756 a_{1}^{2} y^{3} z+472 a_{1} y^{3} z+204 y^{3} z+96 a_{1}^{3} y^{3}+216 a_{1}^{2} y^{3}+140 a_{1} y^{3}+60 y^{3}+54 a_{1}^{3} y^{2} z^{4}+162 a_{1}^{2} y^{2} z^{4}+126 a_{1} y^{2} z^{4}+58 y^{2} z^{4}+312 a_{1}^{3} y^{2} z^{3}+816 a_{1}^{2} y^{2} z^{3}+592 a_{1} y^{2} z^{3}+248 y^{2} z^{3}+558 a_{1}^{3} y^{2} z^{2}+1284 a_{1}^{2} y^{2} z^{2}+798 a_{1} y^{2} z^{2}+312 y^{2} z^{2}+360 a_{1}^{3} y^{2} z+700 a_{1}^{2} y^{2} z+296 a_{1} y^{2} z+116 y^{2} z+100 a_{1}^{3} y^{2}+190 a_{1}^{2} y^{2}+84 a_{1} y^{2}+33 y^{2}+30 a_{1}^{3} y z^{4}+73 a_{1}^{2} y z^{4}+42 a_{1} y z^{4}+19 y z^{4}+166 a_{1}^{3} y z^{3}+370 a_{1}^{2} y z^{3}+206 a_{1} y z^{3}+82 y z^{3}+282 a_{1}^{3} y z^{2}+549 a_{1}^{2} y z^{2}+228 a_{1} y z^{2}+81 y z^{2}+172 a_{1}^{3} y z+258 a_{1}^{2} y z+4 a_{1} y z+46 a_{1}^{3} y+66 a_{1}^{2} y+7 a_{1}^{3} z^{4}+16 a_{1}^{2} z^{4}+9 a_{1} z^{4}+4 z^{4}+38 a_{1}^{3} z^{3}+82 a_{1}^{2} z^{3}+46 a_{1} z^{3}+18 z^{3}+63 a_{1}^{3} z^{2}+120 a_{1}^{2} z^{2}+51 a_{1} z^{2}+17 z^{2}+38 a_{1}^{3} z+56 a_{1}^{2} z+2 a_{1} z+10 a_{1}^{3}+14 a_{1}^{2} $$



The sum of all inequalities gives us a proof of the inequality.





    Counter({0: 8})



Now let's take a look at slightly another kind of the problem.
#### Problem
Let $f:R^3\to R$ be a convex function. Prove that
$$f(1,2,3)+f(2,3,1)+f(3,1,2)\le f(4,3,-1)+f(3,-1,4)+f(-1,4,3).$$

To create a proof, we will use `provef` function. It assumes that $f$ is convex and nonnegative, then it tries to find a proof. However, if the last inequality is $0\le 0$, then the proof works for any convex function.


```python
provef('(-f(1,2,3)-f(2,3,1)-f(3,1,2)+f(4,3,-1)+f(3,-1,4)+f(-1,4,3))*21')
```


numerator: $21 f{\left(-1,4,3 \right)} - 21 f{\left(1,2,3 \right)} - 21 f{\left(2,3,1 \right)} + 21 f{\left(3,-1,4 \right)} - 21 f{\left(3,1,2 \right)} + 21 f{\left(4,3,-1 \right)}$



denominator: $1$



status: 0



From Jensen inequality:



$$21f(1, 2, 3) \le 11f(-1, 4, 3)+8f(3, -1, 4)+2f(4, 3, -1)$$



$$21f(2, 3, 1) \le 8f(-1, 4, 3)+2f(3, -1, 4)+11f(4, 3, -1)$$



$$21f(3, 1, 2) \le 2f(-1, 4, 3)+11f(3, -1, 4)+8f(4, 3, -1)$$



$$ 0 \le 0 $$



The sum of all inequalities gives us a proof of the inequality.





    0



Let's try to solve problem 6 from the finals of LXIII Polish Mathematical Olympiad. It was one of the hardest inequality in the history of this contest, solved only by 3 finalists.

#### Problem
Prove the inequality
$$\left(\frac{a - b}{c}\right)^2 + \left(\frac{b - c}{a}\right)^2 + \left(\frac{c - a}{b}\right)^2\ge 2 \sqrt{2} \left(\frac{a - b}{c} + \frac{b - c}{a}+ \frac{c-a}{b}\right)$$
for any positive numbers $a,b,c$.

The first observation is that the formula is cyclic, so without loss of generality we may assume that $a\ge b,c$. We can go a step further and divide it into two cases: $a\ge b\ge c$ and $a\ge c\ge b$.


```python
shiro.display=lambda x:None #turn off printing of proofs
newproof()
formula=cyclize('((a-b)/c)^2-2*sqrt(2)*(a-b)/c')
```


```python
formula1=makesubs(formula,'[b,oo],[c,oo]',variables='a,b') #a>=b>=c
prove(formula1) 
```




    2




```python
formula2=makesubs(formula,'[c,oo],[b,oo]',variables='a,c') #a>=c>=b
prove(formula2) 
```




    0



So the case $a\ge c\ge b$ is done, but $a\ge b\ge c$ is not. But maybe we can adjust values.


```python
values=findvalues(formula1)
values
```

    Optimization terminated successfully.
             Current function value: 1.000000
             Iterations: 137
             Function evaluations: 249





    (1.7908873553542452e-10, 2.5326984818340415e-10, 7.129450063690368)



First and second value is approximately equal to 0, so we can try to replace 0 with 1.


```python
prove(formula1,values='1,1,7')
```




    2



The key observation is that the `formula1` is homogenous, so we can scale values.


```python
newvalues=(1,values[1]/values[0],values[2]/values[0])
newvalues
```




    (1, 1.4142142855953455, 39809595184.05965)




```python
newvalues[1]**2
```




    2.000002045581953



Now the third value is very big. Technically we could use it, but it would run into overflow error, so we will use 1 instead of it. Second value is very close to $\sqrt{2}$, so this value will be our next try.


```python
prove(formula1,values='1,sqrt(2),1')
```




    0



So after getting the code all together we have got the following proof.


```python
newproof()
shiro.display=lambda x:display(Latex(x)) #turn on printing proofs 
formula=cyclize('((a-b)/c)^2-2*sqrt(2)*(a-b)/c')
display(Latex('Case $a\ge c\ge b$'))
formula1=makesubs(formula,'[c,oo],[b,oo]',variables='a,c,b')
prove(formula1)
display(Latex('Case $a\ge b\ge c$'))
formula2=makesubs(formula,'[b,oo],[c,oo]')
prove(formula2,values='1,2**(1/2),1')
```


Case $a\ge c\ge b$



Substitute $a\to c + d$



Substitute $c\to b + e$



numerator: $2 b^{4} d^{2} + 2 b^{4} d e + 2 b^{4} e^{2} + 4 b^{3} d^{3} + 2 \sqrt{2} b^{3} d^{2} e + 10 b^{3} d^{2} e + 2 \sqrt{2} b^{3} d e^{2} + 6 b^{3} d e^{2} + 4 b^{3} e^{3} + 2 b^{2} d^{4} + 2 \sqrt{2} b^{2} d^{3} e + 10 b^{2} d^{3} e + 6 \sqrt{2} b^{2} d^{2} e^{2} + 12 b^{2} d^{2} e^{2} + 4 b^{2} d e^{3} + 4 \sqrt{2} b^{2} d e^{3} + 2 b^{2} e^{4} + 2 b d^{4} e + 2 \sqrt{2} b d^{3} e^{2} + 6 b d^{3} e^{2} + 4 b d^{2} e^{3} + 4 \sqrt{2} b d^{2} e^{3} + 2 \sqrt{2} b d e^{4} + d^{4} e^{2} + 2 d^{3} e^{3} + d^{2} e^{4}$



denominator: $b^{6} + 2 b^{5} d + 4 b^{5} e + b^{4} d^{2} + 6 b^{4} d e + 6 b^{4} e^{2} + 2 b^{3} d^{2} e + 6 b^{3} d e^{2} + 4 b^{3} e^{3} + b^{2} d^{2} e^{2} + 2 b^{2} d e^{3} + b^{2} e^{4}$



status: 0



$$ 0 \le 2 b^{4} d^{2}+2 b^{4} d e+2 b^{4} e^{2}+4 b^{3} d^{3}+2 \sqrt{2} b^{3} d^{2} e+10 b^{3} d^{2} e+2 \sqrt{2} b^{3} d e^{2}+6 b^{3} d e^{2}+4 b^{3} e^{3}+2 b^{2} d^{4}+2 \sqrt{2} b^{2} d^{3} e+10 b^{2} d^{3} e+6 \sqrt{2} b^{2} d^{2} e^{2}+12 b^{2} d^{2} e^{2}+4 \sqrt{2} b^{2} d e^{3}+4 b^{2} d e^{3}+2 b^{2} e^{4}+2 b d^{4} e+2 \sqrt{2} b d^{3} e^{2}+6 b d^{3} e^{2}+4 \sqrt{2} b d^{2} e^{3}+4 b d^{2} e^{3}+2 \sqrt{2} b d e^{4}+d^{4} e^{2}+2 d^{3} e^{3}+d^{2} e^{4} $$



The sum of all inequalities gives us a proof of the inequality.



Case $a\ge b\ge c$



Substitute $a\to b + f$



Substitute $b\to c + g$



Substitute $f\to \sqrt{2} h$



numerator: $2 c^{4} g^{2} + 2 \sqrt{2} c^{4} g h + 4 c^{4} h^{2} + 4 c^{3} g^{3} - 4 c^{3} g^{2} h + 6 \sqrt{2} c^{3} g^{2} h - 4 \sqrt{2} c^{3} g h^{2} + 20 c^{3} g h^{2} + 8 \sqrt{2} c^{3} h^{3} + 2 c^{2} g^{4} - 8 c^{2} g^{3} h + 4 \sqrt{2} c^{2} g^{3} h - 12 \sqrt{2} c^{2} g^{2} h^{2} + 24 c^{2} g^{2} h^{2} - 8 c^{2} g h^{3} + 20 \sqrt{2} c^{2} g h^{3} + 8 c^{2} h^{4} - 4 c g^{4} h - 8 \sqrt{2} c g^{3} h^{2} + 8 c g^{3} h^{2} - 8 c g^{2} h^{3} + 12 \sqrt{2} c g^{2} h^{3} + 8 c g h^{4} + 2 g^{4} h^{2} + 4 \sqrt{2} g^{3} h^{3} + 4 g^{2} h^{4}$



denominator: $c^{6} + 4 c^{5} g + 2 \sqrt{2} c^{5} h + 6 c^{4} g^{2} + 6 \sqrt{2} c^{4} g h + 2 c^{4} h^{2} + 4 c^{3} g^{3} + 6 \sqrt{2} c^{3} g^{2} h + 4 c^{3} g h^{2} + c^{2} g^{4} + 2 \sqrt{2} c^{2} g^{3} h + 2 c^{2} g^{2} h^{2}$



status: 0



From weighted AM-GM inequality:



$$4 c^{3} g^{2} h \le 2 c^{4} g^{2}+2 c^{2} g^{2} h^{2}$$



$$4 \sqrt{2} c^{3} g h^{2} \le 2 \sqrt{2} c^{4} g h+\sqrt{2} c^{3} h^{3}+\sqrt{2} c g^{2} h^{3}$$



$$8 c^{2} g^{3} h \le 4 c^{3} g^{3}+4 c g^{3} h^{2}$$



$$12 \sqrt{2} c^{2} g^{2} h^{2} \le 6 \sqrt{2} c^{3} g^{2} h+6 \sqrt{2} c g^{2} h^{3}$$



$$8 c^{2} g h^{3} \le 4 c^{3} g h^{2}+2 c^{2} h^{4}+2 g^{2} h^{4}$$



$$4 c g^{4} h \le 2 c^{2} g^{4}+2 g^{4} h^{2}$$



$$8 \sqrt{2} c g^{3} h^{2} \le 4 \sqrt{2} c^{2} g^{3} h+4 \sqrt{2} g^{3} h^{3}$$



$$8 c g^{2} h^{3} \le 4 c g^{3} h^{2}+4 c g h^{4}$$



$$ 0 \le 4 c^{4} h^{2}+16 c^{3} g h^{2}+7 \sqrt{2} c^{3} h^{3}+22 c^{2} g^{2} h^{2}+20 \sqrt{2} c^{2} g h^{3}+6 c^{2} h^{4}+5 \sqrt{2} c g^{2} h^{3}+4 c g h^{4}+2 g^{2} h^{4} $$



The sum of all inequalities gives us a proof of the inequality.





    0



d74b5062289dd255397c707ce31cdfb0cb3982db
ipynb
Jupyter Notebook
.ipynb_checkpoints/tutorial-checkpoint.ipynb
urojony/shiroin
64157741dfd705d7e0be6b0be88d89a28e178f40
BSD-3-Clause
2020-12-13T19:58:17.000Z
2020-12-13T19:58:17.000Z
.ipynb_checkpoints/tutorial-checkpoint.ipynb
urojony/shiroin
64157741dfd705d7e0be6b0be88d89a28e178f40
BSD-3-Clause
.ipynb_checkpoints/tutorial-checkpoint.ipynb
urojony/shiroin
64157741dfd705d7e0be6b0be88d89a28e178f40
BSD-3-Clause
2020-12-13T19:55:52.000Z
2020-12-13T19:55:52.000Z
Qwen/Qwen-72B
1. YES
2. YES