From a7167126e576333f2f5aa604cbb65c7aed9cebfb Mon Sep 17 00:00:00 2001 From: urojony Date: Thu, 16 Apr 2020 08:58:06 +0200 Subject: [PATCH] pretty printing --- .ipynb_checkpoints/examples-checkpoint.ipynb | 229 +- __pycache__/shiroindev.cpython-37.pyc | Bin 13496 -> 13936 bytes __pycache__/test.cpython-37.pyc | Bin 0 -> 444 bytes examples.ipynb | 2902 +++++++++++++++--- shiroindev.py | 70 +- 5 files changed, 2777 insertions(+), 424 deletions(-) create mode 100644 __pycache__/test.cpython-37.pyc diff --git a/.ipynb_checkpoints/examples-checkpoint.ipynb b/.ipynb_checkpoints/examples-checkpoint.ipynb index 37e6fc7..9b4ce1a 100644 --- a/.ipynb_checkpoints/examples-checkpoint.ipynb +++ b/.ipynb_checkpoints/examples-checkpoint.ipynb @@ -2,12 +2,14 @@ "cells": [ { "cell_type": "code", - "execution_count": 1, + "execution_count": 7, "metadata": {}, "outputs": [], "source": [ "from shiroindev import *\n", - "sSeed=1" + "sSeed=1\n", + "from IPython.display import Latex\n", + "sPrint=lambda x:display(Latex(x))" ] }, { @@ -36,21 +38,20 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 8, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "numerator: $$a^2-ab-ac+b^2-bc+c^2$$\n", - "denominator: $$1$$\n", + "numerator: $a^2-ab-ac+b^2-bc+c^2$\n", + "denominator: $1$\n", "status: 0\n", "From weighted AM-GM inequality:\n", "\n", "Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again.\n", - "$$ ab+ac+bc \\le \n", - "a^2+b^2+c^2 $$\n" + "$$ ab+ac+bc \\le a^2+b^2+c^2 $$\n" ] }, { @@ -59,7 +60,7 @@ "0" ] }, - "execution_count": 2, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -759,10 +760,10 @@ "From weighted AM-GM inequality:\n", "$$2a^2b^2c^3d \\le a^3bc^2d^2+ab^3c^4$$\n", "$$2a^2c^3d \\le a^3c^2d^2+ac^4$$\n", - "$$4a^2bc^3d \\le a^3bc^2d^2+a^3c^2d^2+ab^3c^4+ac^4$$\n", + "$$4a^2bc^3d \\le a^3bc^2d^2+a^3c^2d^2+ab^2c^4+abc^4$$\n", "\n", "$$ 0 \\le \n", - "4a^3bcd^3+2a^3bd^4+2a^3cd^3+2a^2b^2cd^3+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4+4a^2c^2d^2+6a^2cd^3+4ab^3c^3d+2ab^3c^2d^2+6ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+6abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3 $$\n", + "4a^3bcd^3+2a^3bd^4+2a^3cd^3+2a^2b^2cd^3+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4+4a^2c^2d^2+6a^2cd^3+ab^3c^4+4ab^3c^3d+2ab^3c^2d^2+5ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+5abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+ac^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3 $$\n", "The sum of all inequalities gives us a proof of the inequality.\n" ] }, @@ -781,6 +782,214 @@ "prove(makesubs(formula,'[0,c],[0,d]')*2)" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "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." + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "numerator: $$x^4-4x^3+6x^2-4x+1$$\n", + "denominator: $$1$$\n", + "\n", + "\\hline\n", + "\n", + "Substitute $x\\to 1+x$\n", + "Numerator after substitutions: x^4\n", + "status: 0\n", + "\n", + "$$ 0 \\le \n", + "x^4 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $x\\to 1/(1+x)$\n", + "Numerator after substitutions: x^4\n", + "status: 0\n", + "\n", + "$$ 0 \\le \n", + "x^4 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n" + ] + } + ], + "source": [ + "powerprove('(x-1)^4')" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "numerator: $$4a^5+4a^4b+4a^4c-6a^4-4a^3b-2a^3c+4ab^3-9ab^2+4ac^2-18ac+9a+4b^4+4b^3c-6b^3-3b^2c+4bc^2-12bc+10b+4c^3-6c^2+11c$$\n", + "denominator: $$1$$\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1+c$\n", + "Numerator after substitutions: 4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+34a^2+4ab^3+3ab^2-2ab+4ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2\n", + "status: 0\n", + "From weighted AM-GM inequality:\n", + "$$2ab \\le a^2+b^2$$\n", + "\n", + "$$ 0 \\le \n", + "4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+33a^2+4ab^3+3ab^2+4ac^2+4b^4+4b^3c+18b^3+9b^2c+17b^2+4bc^2+2bc+4c^3+14c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1+c$\n", + "Numerator after substitutions: 4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2\n", + "status: 0\n", + "\n", + "$$ 0 \\le \n", + "4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1+c$\n", + "Numerator after substitutions: 4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2\n", + "status: 0\n", + "From weighted AM-GM inequality:\n", + "$$2bc \\le b^2+c^2$$\n", + "\n", + "$$ 0 \\le \n", + "4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+17b^2+16bc^3+52bc^2+4c^3+13c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1+c$\n", + "Numerator after substitutions: 4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+116a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2-10abc-2ab+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2\n", + "status: 0\n", + "From weighted AM-GM inequality:\n", + "$$2ab \\le a^2+b^2$$\n", + "$$2bc \\le b^2+c^2$$\n", + "$$10abc \\le 2a^3c+2a^2+2b^3+4bc^2$$\n", + "\n", + "$$ 0 \\le \n", + "4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+38a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+116a^2b+40a^2c^3+124a^2c^2+18a^2c+31a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+16b^3+24b^2c^3+72b^2c^2+3b^2c+16b^2+16bc^3+48bc^2+4c^3+13c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1/(1+c)$\n", + "Numerator after substitutions: 4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+12a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2-2abc^3-6abc^2-6abc-2ab+4ac^3+4ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2\n", + "status: 0\n", + "From weighted AM-GM inequality:\n", + "$$2ab \\le a^2+b^2$$\n", + "$$2bc \\le b^2+c^2$$\n", + "$$6abc \\le 3a^2c+3b^2c$$\n", + "$$2abc^3 \\le a^2bc^3+bc^3$$\n", + "$$6abc^2 \\le a^4b+a^2c^3+b^4c^2+bc^3+2c^2$$\n", + "\n", + "$$ 0 \\le \n", + "4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+3a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+11a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+15a^2c^3+66a^2c^2+81a^2c+33a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2+4ac^3+4ac^2+4b^4c^3+11b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+42b^2c+16b^2+10c^3+11c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1/(1+c)$\n", + "Numerator after substitutions: 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+87ab^2+12abc^3+6abc^2-4abc+2ab+46ac^3+66ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2\n", + "status: 0\n", + "From weighted AM-GM inequality:\n", + "$$2bc \\le b^2+c^2$$\n", + "$$4abc \\le a^2c^2+2ab^2+c^2$$\n", + "\n", + "$$ 0 \\le \n", + "4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+189a^2c^2+84a^2c+34a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+85ab^2+12abc^3+6abc^2+2ab+46ac^3+66ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+17b^2+2bc^3+10c^3+12c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1/(1+c)$\n", + "Numerator after substitutions: 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2\n", + "status: 0\n", + "\n", + "$$ 0 \\le \n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n", + "\n", + "\\hline\n", + "\n", + "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1/(1+c)$\n", + "Numerator after substitutions: 11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc-2ab+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2\n", + "status: 0\n", + "From weighted AM-GM inequality:\n", + "$$2ab \\le a^2+b^2$$\n", + "\n", + "$$ 0 \\le \n", + "11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+33a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+17b^2+38bc^3+56bc^2+2bc+10c^3+14c^2 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n" + ] + } + ], + "source": [ + "formula=Sm('-(3a + 2b + c)(2a^3 + 3b^2 + 6c + 1) + (4a + 4b + 4c)(a^4 + b^3 + c^2 + 3)')\n", + "powerprove(formula)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Now let's take a look at slightly another kind of the problem.\n", + "#### Problem\n", + "Let $f:R^3\\to R$ be a convex function. Prove that\n", + "$$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).$$\n", + "\n", + "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." + ] + }, + { + "cell_type": "code", + "execution_count": 31, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "numerator: $$21f(-1,4,3)-21f(1,2,3)-21f(2,3,1)+21f(3,-1,4)-21f(3,1,2)+21f(4,3,-1)$$\n", + "denominator: $$1$$\n", + "status: 0\n", + "From Jensen inequality:\n", + "$$21f(1, 2, 3) \\le 11f(-1, 4, 3)+8f(3, -1, 4)+2f(4, 3, -1)$$\n", + "$$21f(2, 3, 1) \\le 8f(-1, 4, 3)+2f(3, -1, 4)+11f(4, 3, -1)$$\n", + "$$21f(3, 1, 2) \\le 2f(-1, 4, 3)+11f(3, -1, 4)+8f(4, 3, -1)$$\n", + "\n", + "$$ 0 \\le \n", + "0 $$\n", + "The sum of all inequalities gives us a proof of the inequality.\n" + ] + } + ], + "source": [ + "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')" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/__pycache__/shiroindev.cpython-37.pyc b/__pycache__/shiroindev.cpython-37.pyc index 3f0754cf7382d943ba290c1330ddcf0be5cc5d34..ac4b1c532075c55ce8a27a9344ffbd49999b418a 100644 GIT binary patch literal 13936 zcmds8TWlQHd7k?Ym&@fv6mOF0l`Pv_S)wJ{aTG_9tyq?0$7U5vh>{IuV!3CQTyihu znW0Q=W}7BdV!DW3CA}mK(1t4dQXo%75flYl^r;B?(1)Pt!=NaNv@b^AQXnYw(th8W z*&9tIPTTaMOU;=x=bSm`KmYyz&*;-bLun1azx?;_ymjG{ru_>a+P^F+FXHllsB41=n+TwZedx z_6C;I!azA#(NJcDBT~W@10pR3MMeyXtQZy}VpNQYBdgiM(9VQ6bVa+BEo8l{H?W@Z zvKO_jU%$z9$E(A&k-|sZK5zyn=DM$rV3NF>B4j} zcBU{RCdA}jt#C|CiD}%Aiy3hY_eaEW@d)m-Vpcqg`=cT!PT-ysC&gp9pAe_Szr5+&)}XH&x()X zep~$QzZf}{)p|pEB~I4`27KhfkMrclL$C!bzx)V!xx zWz$=2$mY}jT17T0b>ZFasm^cSktw{w%QsNCx_WM=>)SPe95m$f&5ZEsjasE1Kc)Pj z7;O8`N9pU^D}GQ3fQsg^s|{J(t`>8}GIpBt+daU-^Uc}C_FRW_`_DHYy($~E+}mDd zbuI8j?(!RFUwI=}se9a5CAjl^^MxC09_Fm&8s%KETJ82#JU_Quxs7t$&lPiZ!@g$#z%nV2T6*7Cg|w+3_omTIMrZLN}la+^i$!9#7ndGpmES8X&ld<@v=hY2hDcWM|XE2a6| z7aQBTQn8*Z`aqzk_Sx9xyS`6Mt$KBGCeRF+i$N|j0YY<9QRFqR?tAqfL_VL_qf`P= zJ{9TLBL`ELylUi@WijS?^IGHW$nkbIfr`imes6n`T`dOQPKo@*pM%T9^%5@s3W`;& zW#BS*76L8QLVeeOqB^x?w5*mLT0-BjvrGXs79|A< zAezm}X5NV`k})ztg@RpYyO_;)Z&)7GGEu8zjLoKU2RP%k~zS)XLLrI6) zeG`xmEjCk2Z+&@gKHqAZZ!Mj_k=F~uo~}+w+t`>-Vxd))(DMV%<(N_%fcM`1N|-1*bgL> zqA`Ci(sv^L&VkK5NMEd0{GimRZC*OZ`N?~Z)|^>>TULUF`HR&?3HtaFD(zu;TWwa3 zV5FQw5n1cdmvR!-yeX&HJk92T+eKL^u2en$z@m{8&;B$b+1FQuXa> z6_6f;(N-{?$E$4+pFzE(2#yL30qZ1=|9KST>boGp6#&|@-qFfB_}jSahPrC8;hLZy z;9H?dxy2|aw88svtMk6bwhg0kV-L&{TC8I;&SHlTNSY2G5Y37YMp`<#i@4a;W7?~& zz$Ti|wvjCx+jW8M=kbO-&7x!blt@b=_+z-bv@flBrH#XA-vQQ0*7K#nI3vIBKbQ5gIu)+X^!l#PY zjI2HeGax^SdS??9LW+ozZgP|bm0@Jjor7{Ah>;1$Ff!p0 z9t1Yqb^&6S05MPkwJ}BXUBPq51E4?oIS|b17QIyp`57M9!-i(jh5%i#t-oa;U^sB6cv~NKgS=>JH_5 zAN&Pn+B8m|mQP}=e1gR+i$_oZ9-1=w80&{KndQTj5`eZncn$RqFfkSqU`WFl7{%%r zLTw*>CXD-ruIorEQ(OsRa&AT?>Mt09Mc`I6vSL&FQ%> zojd!9;@RfqvxWSv{M?u3;`*(8(_T7%dT9aTOtN&h0}D{B!&^VW){`vAtO)@kJ=REF z!bZmR+GjDqCnYp91H@CX5$`PGxnrV97G4VZe~(JM-xhsTb7zeP3GN8&+^s_5pW5(G z;T{A^zSdz4r{Mv@ZGq=Xw}r+#a4?Gvu7;J|g&9%p_N2z(9^R~lKYLs&8;Mst1+P}y zPlX8n;VZht8`g4Ksm>ZsvW62ny>oT?Q=R@)Z-3~7DJAdjqNG ze(K?IUw$C=jHqAX*MGh!{m54FZZsHx5_BFBNX7JdoReQ>L6*t8U7?7a+r{cOl(DU1 z#MmCuHbn!Sh%*}O2{;d`nc-ywMBBkaTie{gyFOi9&2$rg{enILO_|Yi_>(u$)6qLw zJainef51aK^1$7~WydZ@U<79Dcik^e5p&%6w?e>nWgYqu; zNt1sHzHkS%m?Pj!r{maX>s)AuuBwB-l2&W$9NsfA3TTW1ILoYYQl% zk)prckiwImSVk~e^P>z}RM5MOC|4O6Nn4W7_7KjhGI+A994BdWA%H5Xa-mAqbdggO zpqx;4H?qr!2>r-`3G<{cU*;PY+ahE0?SoVuT26wJ1^VMF80%A!X&J^~{F{KZQexBk zh@vgyGRUx@Vl$2}F)-nes*b5R6PJGtwlUDwbyBK@bXjXK30G)eo<-DVqSq286Kv35e_vBPHqvP^la^8N;~1_ZxW;iE-T8Cqf~?Z8KWI(ttOPD*8>NK@XT8~) z495gCNSF8aaB^BhkBf4GJxMt{iQwX*79N2MkV=8>&`1y3C^ zqex*5&hzu;R5K|qJ+k#*zgw>zlA71N(Y7plF4N8nFkkLWnp&q;(4YX~f)v@Nfo#!Eh=Z!!F0eqlmYiiY|uU zb6V5k^m?Y12?s@L!?aE$B#uXLtQ=l((!-$ z$#XL=G>ucInsyHPH@Hbpb#_G~Lx+O#oX-@Y$`_1-X^_KW&LA|%WIaKx+6N*BmA06{ z8}b+mxUI|-$xhtR4R8Mg?a3x1{oMb*RQCTRE^*A(#%0qybt>01b0F*g^mrjZ0j*E( z#`ip-TrBxH67x;fNVbg3T5+?-4J)xH1+Q5kl_iJyL(ad?UNGspBXtL;g~>71NCi?JsW0cLS$h9V6gGlQCg+VRBC zOzW1JM%~g4%)=helGbPNo~55OCUn<2gLVs%hKrfb=%>{fN8`v@v~aaFdXc%og|h^B ztYf%FR2$|%>xeF!*h5DU3_NsV&@*_rGnQmwRW7xK1i*D<2m);*EuYYF7y+*pUjG;1 zFF-rn{kaiN=JR4w2l@3hoD%)>cx4N21%~U3u||p$sgdp-P_z#QF7k|MXH#ApYD&miZg>#hOaSs)O{ zF28}N4q|9R^0H~ z8yO`4#JonX0RZx=sP`>Tg|C)pilujXq0@JfQ#~NGqp)8L$8bL!3lqJ7WC#dZ{evH| z7(tq+gs?{a81!^l4X`XV>k>ML+5T{3&6a5+VTlkWJZy{+J zyTkG9=!Kikcfu5?J-i5hGdH|DvFAY_q(e4x%tJg62Kha<8C)`l!C)L^ovDQn@T+n= z9w&7;D-M*V;c(pUm4ME9(y#1@wrS-qeJb~>+umHy_Kf+QWYVNLruI2UX<_1K?)u!x zrg<`d=5R2WPVb)L5X%DTt>h>JgsRlb9}(B5yTHgCW<^Ru3H4V|ht0(Cs3)RKS$f_w z4!u_zRX?_%OmwK+k5a92g~QVoA7j+HxH8yXE3Hf_GF+$l7ClsDLnFIR%^)|~@M#v5 z{K$YkH_9J6{6jJfoN$cr<}ge%pg>>-pvP1>0@E@AGh-R^kmqx{d=Fzfa!eeja4FUD z7ntLJTaJ-HNbSr+nw6xhP<*!KhABujf?0%V>OR>{LZ-G>ZfXcA@dggH)jO9U)mPAV zYYJhtyFUcMXzvd(?8bUX&>7u5aURr|-=B1kh zOtPMTdhYyFij{Gi&*!H)S=a~q8To5`5A=tH{rO+bp<_v{~6035!eL`cwf0~8A6?f>>?7VLPIM5%_K=ji^Fdj9Hv&2 zqiwsc(!`LApQv{AjRR!j$2h!2iavCBi2E*%umZSbO!(uQJ$=pCaOCgoq1Djh-aWJ( z7-2w4V0-sdd&Zt2oIT^1Hl-njrM+X|$Q{-ehhR2sAClB<4yEMMhT40u-Z6*n8Mr5J zi@})Vx5Qoo34(fEt|zN#9IIB~8V0@@{D^A=gL~>-wPybs>UbY({9SjAWEb%oL%-Y_ zOjKb%oi&nKfyq663NRd_-vAu_Jd6O^WIXXQsqvlOS(&=Q{!M%@*|UF@;=unxlG`3+2`)M^JdzU<;Uf=d}*<#$Xm%Gt+Z@g8*Y9%xQ3 zZ2KQ-0_bR}zr@#zTz+lHybsz5b5~I*m#@%;v!kx#Lo=nZ`=Fs6SI~6xK?yX956J`l zK4%Xc@>>d~$igwo`NIHts|(04vuJnwF?ISjpDZfB&3zxT`IU#P*+DzqCWZFn$wra% z>KD;puwhfJt#-X|7zC?b2$XUBh+9|G@8TPzJxBB&viU=aUhA%!AC0Z;*NCF8vN&LJ zc`O>+(*xG_HFnV2;#(HDp0DzercT-2#N{ju@cU5-De=4BXTgE(#Bo|Q&}L0Pa@*s& z?r2-u6!CtW6DtZT6YI7m>J{#U2_nr>fvqyJtW6je{8Cq?KW0#l=?gHi^iw-`e7mFI}$FqTtj{b^LHpi=Ah0{9xc-w@Dg=g1}+nqwX+0mj?6C( zC$8Z$PkUcihpIT{hDPNP=rwqSPI3gwPgPP3vDf26a(!zC$DfY!`|#meU!S=(L*0ot z(9?GuYRWGF5cx$G{63|9FkN7S%A~3M84)FKv7oM#Z?WjlK1bQU^U88a{Bp3?lV-{Q zLm8Fq!51FiMPKJ50~-$=Z~r+w^mr-2)2gPTZ?k2ogJ}3FI1YoBW&B=-NBlk$KFr-1 zix2-&7s-B1+!F#30{ILIeCSAlJ}J*K%e+XVy2-$$)OXcC#kR)k(d zg_~KYb4?=R1o1k)Mv7ag9eCE-GIlPZX0-$QTk|cGt{9y$5YD8-RWa}lq4OS03k;mi zFH7K>EpWE21vuI^wx3#5hYeSiN>HMWFK45SU*V_P#k$wn_VZ3GY}9?q$}9 zAAIaYTtr6IkMyDp*xpZS`7YXimk8i^ehtP1Ab4MY0;TFL5e57aMZ6R$euzq&uFA7C zWR7{Nb$nb9=V9tD`c;O8F%J;N~$P*;R7xF@q-e@=ZM4LgTO}>W^yc;AW$73 zgV*7`8nPKezUt~A5#9^D+MP3a2mh;t??Bd$L)NtQ6h5oQ{}+MROU?r7IdbdUkQ=O? zciSF7j9H%JDD*0H1IO}vXo2u34m+R-m2Oj*?x;i%K_S^{Y$BTG5eL$}2(9G}PW%-X z{Wy$RPT7Y>q@9KWe%FY*7l$4z|u=DSW4N7+O>yrf@?@+amY}sK;kM zf5;kxsDr3Tx4-3YdVfZ2FjEj~abjZ}scN~87JOU1D0fkjcR&1OE-qe$qtoqvmj8#O zyd7*y{2vlY7fPBe$jFk|i`=)1vR=d7kI)VzF3&AczM^K}(8~uzWxy9NRQaQ*l~QSyQ3EQg z231ZCsk|CiBkI6vzLeb_^Ricr#awC78}tUe!HdS`S8sCO(Q2+XR2oXw$d~eHJ6IjA zjg&@e2TBKOqovW>!P3FnSZShV+B56Z!oe<8|V+q&fkl>kdMk6dl&+E%q( zD6e3qg5U1JDi@m5^X<7F)9qhqK7Ca;YK6OAWpyp^RN_lpD=as*s;d5c zP*|zd72Xg`0m#DLO0b4k0&f-IFE_lEmCAC(s|WsU;kv$82pR=!FQ{x(J(+wZ+3u}- zn4-qT;y25fRd3ZXrs5accrKJz%a!_Uv+x8c>i1&EXPYz0TD}())_@McQmxdntyL1J zuu;YyJk(~JH$NW~s*T3Fj{)obFkxl?UJc`PWqG#n<;GTFxm+)leIU@2eKxlEuJ035 zt6rUy2buwMIVeOnKxj?~MPBpjzE|%-Bzhmr7-ofSB)|&x*YSA{YK+% zl=8MWfQrZke(!jZTP+9P_Oe9|#V>`+#`Q8T{|bs#qh;Z;x90*QG(vO7f*LrnV6~i< z8#>Bdcl20jh0dz^NsJ8b(3P6KId;=PyS+jIu;w+ilK~LzW@V$8iX4(LvO$HCTW7uG z)bS9R%aOVA=Y}4~=ts}Lum<|Qu&SHhYC|_)@YgE30p9TL^i*dz?nRj;?bVu|ZX6-h z)QCpPF&%Tv%$Qj-Z|X_3EE59$c+cRHEkd0dfw5;QQ(1u(8p>AAyVjmfZTOIPXhgX~ zD?YRy+O2pr^kZl|w6V3J`DS|It*_0@7F$jGt%Y;fi)LwfrBPK&{u(5FiO7Fs79yjW zTBv#}!OSCb25)EzRPm8nYz{4aZDwI+_SB0D#o|J%X)T{--Gt6N=0o)Cm^&sm>dZ&x$qo`Zn~UojF8>6IRdC1RQSgP?vcM^LM;Q}XBeZrf z$G5Fb2XmN@%(ut{exQqXWX+z9%OF&P>sI6XE|?{BSjT2k^Bq1QX*zsB zF%v!*X_@3M;$p{)X)jwTT9FNP9J#u&Rae;lvv@;4$AS_c7vyJ6Mm~qDOZ(+DZ+ZQ3 zwC{t3+b5y@F%$wzu4V3mAIB0N>@L*1e9??~M4;#ZFxLg3ZxL=-7CGKt9wHysFoeTu&jshO5~LFsxSHmgyAInb{Dxz8;!gAml<$cD?fAJ}}`M~Hof3m6ob>60v|2|(G;vL5qRJlBh8NO&u2=7^kE(9$6(d5b#|C<>^= zRw8yV;7CvbJ93BeeF*-7GHqHXPwHndR#Tto!z`vy0G<=9Kh65%nauHFN(n&Q9$ZDe z15AvC1eh!6iGdMTKOY)<;4@`Cv`k}r8Vqmmz$z?`LUlWPvO#p29YX5#u{vFR?HJGn3iaVA2#+kpir*Wu1T z#nx#SWY&ZLkr`{GE@30a*aJVL@W)@P_TrVQ?0bj=wikc+^G~@AeDkE1zbx{I_XLG_JpZ0EfSrX*K{y6 z?fE0~MAKdf8hufpb>c*SC#Y~sgqtu;p zbqgximC!J@GPF3+Kqt_Q27BVn{mNr_331R?FxS>0Z{S^@@?+SU#0!7U9EbkPnTPSG z-$YMGo6uXQeiWMh43&1kfxCmtjU5SMEp{h%p#NH_?LPzFormyG7T<5B!}Ol}&;aH$ ztpR1On(^2%qm|vBq_49$(i&7|m<5IhrwrsSuHQ7aXTkyW6k0jZEhn0Gur(BT2UxNObK_jL-T;yyV@@$?B-7q6{1Vl-zvw0Tp*%*bk6}rCd5GbQ5h_R)6 zl{IS6Xr$~fHMH`yry*8C`k7KwG25ZsE{&}T8SnC~H+Q)SHLRyj`7en6}wn94vw z%5+hxtUx&>)--Zg5D5BF3WmwkzJ7^sIBbiojl27)I<%C88gulr-@;g*{)drcWW~R6 z$ROn~YmNwQ8Eru_Es3}mF>;yV27lCTWKSEHKMso*7^G7xtE|=_q>>Uwn{irX!-i}? zN|~E#SEz)@TWagE_RwEbgnNM1DMU$n-zZv|=0c7T=|y!2*k zA{% zGb#kxGS7cDr_3aLd2sV@!S7!LUOS`3kQ|EZauK{g*J5|ji7!A+IHK+%oOI8R!3T^;ZV~5<{L)+aCkU8Vi_&? z;Nj8mDb%bMT)0+t^F}<6zJX9T3wxJ)mz?FchS&?d+ZcPK^%Nq1{4rz;t#%DPhg(M< zn51${^9SbQ_0~A}Z5pjt0sqj4={ZH6G~JpA^1*O80bMdNN&X&Mcd*A_ykR`BHh%&9 z!POL+$CQ7uhwhk|TZK=78Ho`WuRzaEvo5_gz{tH4y2bD&W9GcsVCl)oxrJo7K1e-Q+)^p zJW3{Ux-NY;^87cnCwq;|v;Pm%&_HP6{}Q20thSlQE`YZG)1!gnA-JU1JWq*_q`yc) zzK$Yt$eEE{D{u7pQS?v{?P56crQmktnKT^`q(Dy3W;q8du09VSj7Kp6volm z&!dl*f?tK|(+{{?Ov507@7}iQT43%>kPQauo~!g;4u|#Z z&BSg8+6RCx8}3RLZni6j`0Pi@Fm`P@P7Uq2aHG?pW`3R~dEL7gdl&RGI%FY7Ji)u* z9(xQgxZnf^gE7SPGDh6TkK$S!BlbBf4sxd8RNU$1@Xk5TukGx#=@c$~rts_A-ihw^ zG`82{df@iPfmzog(OpQd;lU<>MOq@o}s(ic#hAQhGK!G z(7_bqND>Azx1v372`ACF8dX2e$}tTgnHf==n(=#-t@s!tht*x{E0(f2pbLCqp2bOy zb?X#(U1P%~7EF{z7VNaO@}aXfWT?OZ69lz@VTOe~5%fFMlawQ{7$dMA8H=_C8Kd9B zn2vZdW0b}v8si6;<9}N`5$C73XCb5_z!EV}w=!WG!ip#qF_zpX+F8K#=B=9s;=#!v zjWc9<=Mn_%3fdMK{brb1HJR7S;u_rkR^QBbF!KQB%v>@q;|&}^Wc$}S(q1PU4$9H2 zM8Z5)>^>m^bSL8Yd=Rl%?>J-~d&fx(k1>d-GQogi9ui;t>|t&m^{PygqeSjxFBfJX zk`c3026ALWVGb>6wjfK!cacd8^30YostJY>(GKlbX)uW2y%}539F&dz2FNDLrkTku ztigx!vdsY`Hw))pm^pV!_!Y|$i;3G{#9+*{SJ&*c~^_+QB>Z7Lq zeY|zGBPg_EJP4wB_5TUFw=F1bI~Ce`8dePK*|K5JY}hlT#KfKm3y)>HaByJ)qH zxOW$A`$ky$UyqxgU+qz4o zMb)N}$|JFpqDLWAkYf*0Yt6cB1i2jpn1ic@1badafh`?o`kpgFnc?2mk*>-j$-}q5 z1Lc7uk{x(SP#EAQwt>H}GFpbiGT%Y}l5y zW!H0$gMeF2I7AHDuefy~d>7xKD#O-(qQ{$mEWIn;Rf{9BWn{b~(bs=w)tV0iA}!q(kf;vNmoxa1t|;Vql_S6rq1!oW{-_pDvt)f#eze40`BP zGGUO#TcZ{e5lCv_%0L-m{ti*d7t|EuUN%vI(`MqbaM`$=?FDFTWLS~re*@n@x_hP^ zJ>t+8dXxu+Z@_^|B?pE4Oe4)O_I7+^Y;GRLAz@0~Fnn~?*Jp1YrpCk@=;=E&wDmOr zqOY^yw;Ao@Tgg#Lwn}nTH`)Is7Nab_%tGSw-r&6VRBvUQ_@z2DdQv$#U?>M1Wq~>U zN9gMuu)BEZxZa<@Lyt!RJgp-7ghsVn4pZCoD{zDa-O3nw1rF+aOsX(HV$DDKGgdd| z)i*JF9EuPE%};vpkzaxJ$M|3Sx0w=GYULenk9lOn&42;)`>1sYO(K)nLg+PAxS8AZ zcu7Q@x?SU`gS1dFD4a{StnEvvIqh(IakgdCZKC4@!ePsyRk3jHm3kKj1!m2q?+-U> zj#_2nPt7n5&fjr-$L8BiGUGQ_$3t6Y~X$KIh4}7Ocd}(6!8*N{0NmcUBwH;XEDqL z-R4IUlIy5v&@WygLkl2`hqvcLSm`+Y!N*DX;|CSO=Lm}6dBC4kc5=X$AW#ln!Rzoe zE!_+uUv)W>gU~=Jx}yz2gaW!Er?G+1R>EATf;dJ6K}G-Who9{E`Kxemy4~lZ>=OQu zM6jj3r6o5h1Jyn>MIPik()X+w=~cfh&2-s^SK$ zI^*&Y5+lv?n~!IneK{Hpfh_%ay}zULor7-+h)l`tgg`+7*Pu{|9VpR@0yXwf2nAY5 zP=N|}Py{;Y0YOEa`{MBpWP^P|BOb_q42ez2ZAze_Kw2OaQnPU3ZE5T*3tS>)Q`TBa zHe2)4j);SUjk@OiSIc- h%R<8+?$??VW?cJsL^3(P_=3O6s|j%|VvI5IcmPNxQ04#t literal 0 HcmV?d00001 diff --git a/examples.ipynb b/examples.ipynb index c2447e4..4df967b 100644 --- a/examples.ipynb +++ b/examples.ipynb @@ -7,14 +7,16 @@ "outputs": [], "source": [ "from shiroindev import *\n", - "sSeed=1" + "sVars.seed=1\n", + "from IPython.display import Latex\n", + "sVars.print=lambda x:display(Latex(x))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "The first line obviously loads this package. The second one sets a seed for proving functions. If you don't write it, you can get slightly different proof each time you run a function. \n", + "The first line obviously loads this package. The second one sets a seed for proving functions. If you don't write it, you can get slightly different proof each time you run a function. The next two lines\n", "\n", "Now let's make some proofs. We will use problems from https://www.imomath.com/index.php?options=593&lmm=0." ] @@ -40,18 +42,86 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$a^2-ab-ac+b^2-bc+c^2$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "\n", - "Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again.\n", - "$$ ab+ac+bc \\le \n", - "a^2+b^2+c^2 $$\n" - ] + "data": { + "text/latex": [ + "numerator: $a^2-ab-ac+b^2-bc+c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ ab+ac+bc \\le a^2+b^2+c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -88,21 +158,88 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$2a^2-2ab-2ac+2b^2-2bc+2c^2$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2ab \\le a^2+b^2$$\n", - "$$2ac \\le a^2+c^2$$\n", - "$$2bc \\le b^2+c^2$$\n", - "\n", - "$$ 0 \\le \n", - "0 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "numerator: $2a^2-2ab-2ac+2b^2-2bc+2c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$$$2ac \\le a^2+c^2$$$$2bc \\le b^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 0 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -140,17 +277,74 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$a^2-ab-ac-ad+b^2+c^2+d^2$$\n", - "denominator: $$1$$\n", - "status: 2\n", - "\n", - "Program couldn't find any proof.\n", - "$$ ab+ac+ad \\le \n", - "a^2+b^2+c^2+d^2 $$\n" - ] + "data": { + "text/latex": [ + "numerator: $a^2-ab-ac-ad+b^2+c^2+d^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 2" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Program couldn't find any proof." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ ab+ac+ad \\le a^2+b^2+c^2+d^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -180,22 +374,100 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ a \\to 2a $\n", - "numerator: $$4a^2-2ab-2ac-2ad+b^2+c^2+d^2$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2ab \\le a^2+b^2$$\n", - "$$2ac \\le a^2+c^2$$\n", - "$$2ad \\le a^2+d^2$$\n", - "\n", - "$$ 0 \\le \n", - "a^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $a\\to 2a$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $4a^2-2ab-2ac-2ad+b^2+c^2+d^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$$$2ac \\le a^2+c^2$$$$2ad \\le a^2+d^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le a^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -225,22 +497,100 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ a \\to 7a/4 $\n", - "numerator: $$49a^2-28ab-28ac-28ad+16b^2+16c^2+16d^2$$\n", - "denominator: $$16$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$28ab \\le 14a^2+14b^2$$\n", - "$$28ac \\le 14a^2+14c^2$$\n", - "$$28ad \\le 14a^2+14d^2$$\n", - "\n", - "$$ 0 \\le \n", - "7a^2+2b^2+2c^2+2d^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $a\\to 7a/4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $49a^2-28ab-28ac-28ad+16b^2+16c^2+16d^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $16$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$28ab \\le 14a^2+14b^2$$$$28ac \\le 14a^2+14c^2$$$$28ad \\le 14a^2+14d^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 7a^2+2b^2+2c^2+2d^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -276,19 +626,98 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$-x^3y+2x^2y^2-x^2-xy^3+2xy-y^2$$\n", - "denominator: $$x^3y^3-x^3y-x^2y^2+x^2-xy^3+xy+y^2-1$$\n", - "status: 2\n", - "\n", - "Program couldn't find any proof.\n", - "$$ x^3y+x^2+xy^3+y^2 \\le \n", - "2x^2y^2+2xy $$\n", - "It looks like the formula is symmetric. You can assume without loss of generality that x >= y Try\n", - "prove(makesubs(S(\" -x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2 \"), [('y', 'inf')] )\n" - ] + "data": { + "text/latex": [ + "numerator: $-x^3y+2x^2y^2-x^2-xy^3+2xy-y^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $x^3y^3-x^3y-x^2y^2+x^2-xy^3+xy+y^2-1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 2" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Program couldn't find any proof." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ x^3y+x^2+xy^3+y^2 \\le 2x^2y^2+2xy $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "It looks like the formula is symmetric. You can assume without loss of generality that x >= y. Try" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "prove(makesubs(S(\"-x**3*y + 2*x**2*y**2 - x**2 - x*y**3 + 2*x*y - y**2\"),[('y', 'inf')])" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -321,24 +750,112 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ x \\to 1-1/(x+1) $\n", - "Substitute $ y \\to 1-1/(y+1) $\n", - "numerator: $$6x^3y+3x^3-12x^2y^2-3x^2y+3x^2+6xy^3-3xy^2-6xy+3y^3+3y^2$$\n", - "denominator: $$4x^2y+2x^2+4xy^2+8xy+3x+2y^2+3y+1$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$12x^2y^2 \\le 6x^3y+6xy^3$$\n", - "$$3x^2y \\le 2x^3+y^3$$\n", - "$$3xy^2 \\le x^3+2y^3$$\n", - "$$6xy \\le 3x^2+3y^2$$\n", - "\n", - "$$ 0 \\le \n", - "0 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $x\\to 1-1/(x+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $y\\to 1-1/(y+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $6x^3y+3x^3-12x^2y^2-3x^2y+3x^2+6xy^3-3xy^2-6xy+3y^3+3y^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $4x^2y+2x^2+4xy^2+8xy+3x+2y^2+3y+1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$12x^2y^2 \\le 6x^3y+6xy^3$$$$3x^2y \\le 2x^3+y^3$$$$3xy^2 \\le x^3+2y^3$$$$6xy \\le 3x^2+3y^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 0 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -381,24 +898,124 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ x \\to -y+1+(y-1)/(x+1) $\n", - "Substitute $ y \\to 1-1/(y+1) $\n", - "Substitute $ y \\to y/2 $\n", - "numerator: $$x^4y^2+x^3y^2-2x^3y-4x^2y+4x^2+xy^2-2xy+y^2$$\n", - "denominator: $$x^3y^2+2x^3y+2x^2y^2+4x^2y+xy^2+2xy$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2x^3y \\le x^4y^2+x^2$$\n", - "$$4x^2y \\le x^3y^2+2x^2+xy^2$$\n", - "$$2xy \\le x^2+y^2$$\n", - "\n", - "$$ 0 \\le \n", - "0 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $x\\to -y+1+(y-1)/(x+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $y\\to 1-1/(y+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $y\\to y/2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $x^4y^2+x^3y^2-2x^3y-4x^2y+4x^2+xy^2-2xy+y^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $x^3y^2+2x^3y+2x^2y^2+4x^2y+xy^2+2xy$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2x^3y \\le x^4y^2+x^2$$$$4x^2y \\le x^3y^2+2x^2+xy^2$$$$2xy \\le x^2+y^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 0 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -434,21 +1051,88 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$2a^2-2ab-2ac+2b^2-2bc+2c^2$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2ab \\le a^2+b^2$$\n", - "$$2ac \\le a^2+c^2$$\n", - "$$2bc \\le b^2+c^2$$\n", - "\n", - "$$ 0 \\le \n", - "0 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "numerator: $2a^2-2ab-2ac+2b^2-2bc+2c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$$$2ac \\le a^2+c^2$$$$2bc \\le b^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 0 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -482,17 +1166,74 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$x^4-4x^3+6x^2-4x+1$$\n", - "denominator: $$1$$\n", - "status: 2\n", - "\n", - "Program couldn't find any proof.\n", - "$$ 4x^3+4x \\le \n", - "x^4+6x^2+1 $$\n" - ] + "data": { + "text/latex": [ + "numerator: $x^4-4x^3+6x^2-4x+1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 2" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Program couldn't find any proof." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 4x^3+4x \\le x^4+6x^2+1 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -522,18 +1263,86 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ x \\to x+1 $\n", - "numerator: $$x^4$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "\n", - "$$ 0 \\le \n", - "x^4 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $x\\to x+1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $x^4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le x^4 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -558,18 +1367,86 @@ }, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ x \\to 1-x $\n", - "numerator: $$x^4$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "\n", - "$$ 0 \\le \n", - "x^4 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $x\\to 1-x$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $x^4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le x^4 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -628,17 +1505,74 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$a^3c+a^3d+a^2b^2-a^2bd-2a^2c^2-a^2cd+a^2d^2+ab^3-ab^2c-ab^2d-abc^2+ac^3-acd^2+b^3d+b^2c^2-2b^2d^2+bc^3-bc^2d-bcd^2+bd^3+c^2d^2+cd^3$$\n", - "denominator: $$a^2bc+a^2bd+a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+2abcd+abd^2+ac^2d+acd^2+b^2cd+b^2d^2+bc^2d+bcd^2$$\n", - "status: 2\n", - "\n", - "Program couldn't find any proof.\n", - "$$ a^2bd+2a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+acd^2+2b^2d^2+bc^2d+bcd^2 \\le \n", - "a^3c+a^3d+a^2b^2+a^2d^2+ab^3+ac^3+b^3d+b^2c^2+bc^3+bd^3+c^2d^2+cd^3 $$\n" - ] + "data": { + "text/latex": [ + "numerator: $a^3c+a^3d+a^2b^2-a^2bd-2a^2c^2-a^2cd+a^2d^2+ab^3-ab^2c-ab^2d-abc^2+ac^3-acd^2+b^3d+b^2c^2-2b^2d^2+bc^3-bc^2d-bcd^2+bd^3+c^2d^2+cd^3$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $a^2bc+a^2bd+a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+2abcd+abd^2+ac^2d+acd^2+b^2cd+b^2d^2+bc^2d+bcd^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 2" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Program couldn't find any proof." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ a^2bd+2a^2c^2+a^2cd+ab^2c+ab^2d+abc^2+acd^2+2b^2d^2+bc^2d+bcd^2 \\le a^3c+a^3d+a^2b^2+a^2d^2+ab^3+ac^3+b^3d+b^2c^2+bc^3+bd^3+c^2d^2+cd^3 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -668,20 +1602,110 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ a \\to a+c $\n", - "Substitute $ b \\to b+d $\n", - "numerator: $$a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d-abc^2+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2$$\n", - "denominator: $$a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "\n", - "Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again.\n", - "$$ abc^2 \\le \n", - "a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2 $$\n" - ] + "data": { + "text/latex": [ + "Substitute $a\\to a+c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $b\\to b+d$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d-abc^2+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Program couldn't find a solution with integer coefficients. Try to multiple the formula by some integer and run this function again." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ abc^2 \\le a^3c+a^3d+a^2b^2+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^3+ab^2c+2ab^2d+abd^2+b^3c+b^3d+b^2c^2+2b^2cd+b^2d^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -704,21 +1728,112 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ a \\to a+c $\n", - "Substitute $ b \\to b+d $\n", - "numerator: $$2a^3c+2a^3d+2a^2b^2+2a^2bd+2a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d-2abc^2+2abd^2+2b^3c+2b^3d+2b^2c^2+4b^2cd+2b^2d^2$$\n", - "denominator: $$a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2abc^2 \\le a^2c^2+b^2c^2$$\n", - "\n", - "$$ 0 \\le \n", - "2a^3c+2a^3d+2a^2b^2+2a^2bd+a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d+2abd^2+2b^3c+2b^3d+b^2c^2+4b^2cd+2b^2d^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $a\\to a+c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $b\\to b+d$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $2a^3c+2a^3d+2a^2b^2+2a^2bd+2a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d-2abc^2+2abd^2+2b^3c+2b^3d+2b^2c^2+4b^2cd+2b^2d^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $a^2bc+a^2bd+a^2c^2+2a^2cd+a^2d^2+ab^2c+ab^2d+3abc^2+6abcd+3abd^2+2ac^3+6ac^2d+6acd^2+2ad^3+b^2c^2+2b^2cd+b^2d^2+2bc^3+6bc^2d+6bcd^2+2bd^3+c^4+4c^3d+6c^2d^2+4cd^3+d^4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2abc^2 \\le a^2c^2+b^2c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 2a^3c+2a^3d+2a^2b^2+2a^2bd+a^2c^2+4a^2cd+2a^2d^2+2ab^3+2ab^2c+4ab^2d+2abd^2+2b^3c+2b^3d+b^2c^2+4b^2cd+2b^2d^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -748,23 +1863,124 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "Substitute $ a \\to c-c/(a+1) $\n", - "Substitute $ b \\to d-d/(b+1) $\n", - "numerator: $$2a^3bc^2d^2+4a^3bcd^3+2a^3bd^4+2a^3c^2d^2+2a^3cd^3-2a^2b^2c^3d+2a^2b^2cd^3-4a^2bc^3d+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4-2a^2c^3d+4a^2c^2d^2+6a^2cd^3+2ab^3c^4+4ab^3c^3d+2ab^3c^2d^2+6ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+6abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+2ac^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3$$\n", - "denominator: $$a^3b^3c^4+4a^3b^3c^3d+6a^3b^3c^2d^2+4a^3b^3cd^3+a^3b^3d^4+3a^3b^2c^4+10a^3b^2c^3d+12a^3b^2c^2d^2+6a^3b^2cd^3+a^3b^2d^4+3a^3bc^4+8a^3bc^3d+7a^3bc^2d^2+2a^3bcd^3+a^3c^4+2a^3c^3d+a^3c^2d^2+a^2b^3c^4+6a^2b^3c^3d+12a^2b^3c^2d^2+10a^2b^3cd^3+3a^2b^3d^4+3a^2b^2c^4+15a^2b^2c^3d+24a^2b^2c^2d^2+15a^2b^2cd^3+3a^2b^2d^4+3a^2bc^4+12a^2bc^3d+14a^2bc^2d^2+5a^2bcd^3+a^2c^4+3a^2c^3d+2a^2c^2d^2+2ab^3c^3d+7ab^3c^2d^2+8ab^3cd^3+3ab^3d^4+5ab^2c^3d+14ab^2c^2d^2+12ab^2cd^3+3ab^2d^4+4abc^3d+8abc^2d^2+4abcd^3+ac^3d+ac^2d^2+b^3c^2d^2+2b^3cd^3+b^3d^4+2b^2c^2d^2+3b^2cd^3+b^2d^4+bc^2d^2+bcd^3$$\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2a^2b^2c^3d \\le a^3bc^2d^2+ab^3c^4$$\n", - "$$2a^2c^3d \\le a^3c^2d^2+ac^4$$\n", - "$$4a^2bc^3d \\le a^3bc^2d^2+a^3c^2d^2+ab^2c^4+abc^4$$\n", - "\n", - "$$ 0 \\le \n", - "4a^3bcd^3+2a^3bd^4+2a^3cd^3+2a^2b^2cd^3+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4+4a^2c^2d^2+6a^2cd^3+ab^3c^4+4ab^3c^3d+2ab^3c^2d^2+5ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+5abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+ac^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "Substitute $a\\to c-c/(a+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $b\\to d-d/(b+1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "numerator: $2a^3bc^2d^2+4a^3bcd^3+2a^3bd^4+2a^3c^2d^2+2a^3cd^3-2a^2b^2c^3d+2a^2b^2cd^3-4a^2bc^3d+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4-2a^2c^3d+4a^2c^2d^2+6a^2cd^3+2ab^3c^4+4ab^3c^3d+2ab^3c^2d^2+6ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+6abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+2ac^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $a^3b^3c^4+4a^3b^3c^3d+6a^3b^3c^2d^2+4a^3b^3cd^3+a^3b^3d^4+3a^3b^2c^4+10a^3b^2c^3d+12a^3b^2c^2d^2+6a^3b^2cd^3+a^3b^2d^4+3a^3bc^4+8a^3bc^3d+7a^3bc^2d^2+2a^3bcd^3+a^3c^4+2a^3c^3d+a^3c^2d^2+a^2b^3c^4+6a^2b^3c^3d+12a^2b^3c^2d^2+10a^2b^3cd^3+3a^2b^3d^4+3a^2b^2c^4+15a^2b^2c^3d+24a^2b^2c^2d^2+15a^2b^2cd^3+3a^2b^2d^4+3a^2bc^4+12a^2bc^3d+14a^2bc^2d^2+5a^2bcd^3+a^2c^4+3a^2c^3d+2a^2c^2d^2+2ab^3c^3d+7ab^3c^2d^2+8ab^3cd^3+3ab^3d^4+5ab^2c^3d+14ab^2c^2d^2+12ab^2cd^3+3ab^2d^4+4abc^3d+8abc^2d^2+4abcd^3+ac^3d+ac^2d^2+b^3c^2d^2+2b^3cd^3+b^3d^4+2b^2c^2d^2+3b^2cd^3+b^2d^4+bc^2d^2+bcd^3$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2a^2b^2c^3d \\le a^3bc^2d^2+ab^3c^4$$$$2a^2c^3d \\le a^3c^2d^2+ac^4$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$4a^2bc^3d \\le a^3bc^2d^2+a^3c^2d^2+ab^3c^4+ac^4$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^3bcd^3+2a^3bd^4+2a^3cd^3+2a^2b^2cd^3+4a^2bc^2d^2+12a^2bcd^3+6a^2bd^4+4a^2c^2d^2+6a^2cd^3+4ab^3c^3d+2ab^3c^2d^2+6ab^2c^4+8ab^2c^3d+4ab^2c^2d^2+4ab^2cd^3+6abc^4+4abc^3d+6abc^2d^2+12abcd^3+6abd^4+4ac^2d^2+6acd^3+2b^3c^3d+2b^3c^2d^2+4b^2c^3d+4b^2c^2d^2+2b^2cd^3+2bc^3d+4bc^2d^2+4bcd^3+2bd^4+2c^2d^2+2cd^3 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { "data": { @@ -790,36 +2006,198 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 19, "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$x^4-4x^3+6x^2-4x+1$$\n", - "denominator: $$1$$\n", - "\n", - "\\hline\n", - "\n", - "Substitute $x\\to 1+x$\n", - "Numerator after substitutions: x^4\n", - "status: 0\n", - "\n", - "$$ 0 \\le \n", - "x^4 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $x\\to 1/(1+x)$\n", - "Numerator after substitutions: x^4\n", - "status: 0\n", - "\n", - "$$ 0 \\le \n", - "x^4 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "numerator: $x^4-4x^3+6x^2-4x+1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to 1+x$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $x^4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le x^4 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $x\\to 1/(1+x)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $x^4$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le x^4 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -828,121 +2206,816 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 20, "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$4a^5+4a^4b+4a^4c-6a^4-4a^3b-2a^3c+4ab^3-9ab^2+4ac^2-18ac+9a+4b^4+4b^3c-6b^3-3b^2c+4bc^2-12bc+10b+4c^3-6c^2+11c$$\n", - "denominator: $$1$$\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1+c$\n", - "Numerator after substitutions: 4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+34a^2+4ab^3+3ab^2-2ab+4ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2ab \\le a^2+b^2$$\n", - "\n", - "$$ 0 \\le \n", - "4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+33a^2+4ab^3+3ab^2+4ac^2+4b^4+4b^3c+18b^3+9b^2c+17b^2+4bc^2+2bc+4c^3+14c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1+c$\n", - "Numerator after substitutions: 4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2\n", - "status: 0\n", - "\n", - "$$ 0 \\le \n", - "4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1+c$\n", - "Numerator after substitutions: 4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2bc \\le b^2+c^2$$\n", - "\n", - "$$ 0 \\le \n", - "4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+17b^2+16bc^3+52bc^2+4c^3+13c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1+c$\n", - "Numerator after substitutions: 4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+116a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2-10abc-2ab+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2ab \\le a^2+b^2$$\n", - "$$2bc \\le b^2+c^2$$\n", - "$$10abc \\le 5a^2b+5bc^2$$\n", - "\n", - "$$ 0 \\le \n", - "4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+111a^2b+40a^2c^3+124a^2c^2+18a^2c+33a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+16b^2+16bc^3+47bc^2+4c^3+13c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1/(1+c)$\n", - "Numerator after substitutions: 4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+12a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2-2abc^3-6abc^2-6abc-2ab+4ac^3+4ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$6abc \\le 2a^3+2b^2+2bc^3$$\n", - "$$2ab \\le a^2+b^2$$\n", - "$$2bc \\le b^2+c^2$$\n", - "$$6abc^2 \\le 3a^2c^2+2b^2c^3+b^2$$\n", - "$$2abc^3 \\le a^2c^3+b^2c^3$$\n", - "\n", - "$$ 0 \\le \n", - "4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+40a^3+12a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+15a^2c^3+63a^2c^2+84a^2c+33a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2+4ac^3+4ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+6b^2c^3+36b^2c^2+45b^2c+13b^2+10c^3+13c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1/(1+c)$\n", - "Numerator after substitutions: 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+87ab^2+12abc^3+6abc^2-4abc+2ab+46ac^3+66ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2bc \\le b^2+c^2$$\n", - "$$4abc \\le 2a^2+b^4c^2+c^2$$\n", - "\n", - "$$ 0 \\le \n", - "4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+190a^2c^2+84a^2c+32a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+87ab^2+12abc^3+6abc^2+2ab+46ac^3+66ac^2+4b^4c^3+11b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+17b^2+2bc^3+10c^3+12c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1/(1+c)$\n" - ] + "data": { + "text/latex": [ + "numerator: $4a^5+4a^4b+4a^4c-6a^4-4a^3b-2a^3c+4ab^3-9ab^2+4ac^2-18ac+9a+4b^4+4b^3c-6b^3-3b^2c+4bc^2-12bc+10b+4c^3-6c^2+11c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" }, { - "name": "stdout", - "output_type": "stream", - "text": [ - "Numerator after substitutions: 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2\n", - "status: 0\n", - "\n", - "$$ 0 \\le \n", - "4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n", - "\n", - "\\hline\n", - "\n", - "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1/(1+c)$\n", - "Numerator after substitutions: 11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc-2ab+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2\n", - "status: 0\n", - "From weighted AM-GM inequality:\n", - "$$2ab \\le a^2+b^2$$\n", - "\n", - "$$ 0 \\le \n", - "11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+33a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+17b^2+38bc^3+56bc^2+2bc+10c^3+14c^2 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1+c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+34a^2+4ab^3+3ab^2-2ab+4ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5+4a^4b+4a^4c+22a^4+12a^3b+14a^3c+42a^3+12a^2b+18a^2c+33a^2+4ab^3+3ab^2+4ac^2+4b^4+4b^3c+18b^3+9b^2c+17b^2+4bc^2+2bc+4c^3+14c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1+c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5b^4+4a^5b^3c+14a^5b^3+9a^5b^2c+15a^5b^2+4a^5bc^2+2a^5bc+6a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4+20a^4b^3c+74a^4b^3+45a^4b^2c+78a^4b^2+20a^4bc^2+10a^4bc+24a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4+40a^3b^3c+156a^3b^3+90a^3b^2c+162a^3b^2+40a^3bc^2+20a^3bc+36a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4+40a^2b^3c+164a^2b^3+90a^2b^2c+168a^2b^2+40a^2bc^2+20a^2bc+20a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4+20ab^3c+86ab^3+45ab^2c+87ab^2+20abc^2+10abc+2ab+20ac^3+66ac^2+4b^4+4b^3c+18b^3+9b^2c+18b^2+4bc^2+2bc+4c^3+14c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1+c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2bc \\le b^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5b^4+16a^5b^3+24a^5b^2+16a^5b+4a^5+4a^4b^4c+18a^4b^4+16a^4b^3c+76a^4b^3+24a^4b^2c+120a^4b^2+16a^4bc+84a^4b+4a^4c+22a^4+14a^3b^4c+30a^3b^4+56a^3b^3c+132a^3b^3+84a^3b^2c+216a^3b^2+56a^3bc+156a^3b+14a^3c+42a^3+18a^2b^4c+22a^2b^4+72a^2b^3c+100a^2b^3+108a^2b^2c+168a^2b^2+72a^2bc+124a^2b+18a^2c+34a^2+4ab^4c^2+ab^4+16ab^3c^2+8ab^3+24ab^2c^2+9ab^2+16abc^2+2ab+4ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+17b^2+16bc^3+52bc^2+4c^3+13c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1+c$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+116a^2b+40a^2c^3+124a^2c^2+18a^2c+34a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+15ab^2c+81ab^2+80abc^3+244abc^2-10abc-2ab+20ac^3+66ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+18b^3+24b^2c^3+72b^2c^2+3b^2c+18b^2+16bc^3+52bc^2-2bc+4c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$$$2bc \\le b^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$10abc \\le 2a^2+2ab^2c+4ac^2+2b^3$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5b^4c^3+6a^5b^4c^2+11a^5b^4c+9a^5b^4+16a^5b^3c^3+28a^5b^3c^2+40a^5b^3c+38a^5b^3+24a^5b^2c^3+48a^5b^2c^2+51a^5b^2c+57a^5b^2+16a^5bc^3+36a^5bc^2+30a^5bc+34a^5b+4a^5c^3+10a^5c^2+8a^5c+10a^5+20a^4b^4c^3+34a^4b^4c^2+45a^4b^4c+40a^4b^4+80a^4b^3c^3+156a^4b^3c^2+160a^4b^3c+170a^4b^3+120a^4b^2c^3+264a^4b^2c^2+195a^4b^2c+246a^4b^2+80a^4bc^3+196a^4bc^2+110a^4bc+136a^4b+20a^4c^3+54a^4c^2+30a^4c+40a^4+40a^3b^4c^3+76a^3b^4c^2+70a^3b^4c+70a^3b^4+160a^3b^3c^3+344a^3b^3c^2+240a^3b^3c+300a^3b^3+240a^3b^2c^3+576a^3b^2c^2+270a^3b^2c+414a^3b^2+160a^3bc^3+424a^3bc^2+140a^3bc+204a^3b+40a^3c^3+116a^3c^2+40a^3c+60a^3+40a^2b^4c^3+84a^2b^4c^2+48a^2b^4c+58a^2b^4+160a^2b^3c^3+376a^2b^3c^2+152a^2b^3c+248a^2b^3+240a^2b^2c^3+624a^2b^2c^2+138a^2b^2c+312a^2b^2+160a^2bc^3+456a^2bc^2+52a^2bc+116a^2b+40a^2c^3+124a^2c^2+18a^2c+31a^2+20ab^4c^3+46ab^4c^2+15ab^4c+19ab^4+80ab^3c^3+204ab^3c^2+40ab^3c+82ab^3+120ab^2c^3+336ab^2c^2+13ab^2c+81ab^2+80abc^3+244abc^2+20ac^3+62ac^2+4b^4c^3+10b^4c^2+3b^4c+4b^4+16b^3c^3+44b^3c^2+8b^3c+16b^3+24b^2c^3+72b^2c^2+3b^2c+16b^2+16bc^3+52bc^2+4c^3+13c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1+a,b\\to 1+b,c\\to 1/(1+c)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+12a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+12a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+3ab^2c^3+9ab^2c^2+9ab^2c+3ab^2-2abc^3-6abc^2-6abc-2ab+4ac^3+4ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2abc^3 \\le a^2bc^3+bc^3$$$$2ab \\le a^2+b^2$$$$2bc \\le b^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$6abc \\le 2a^3b+2b^2c+2c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$6abc^2 \\le 2ab^2c^3+ab^2+3ac^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5c^3+12a^5c^2+12a^5c+4a^5+4a^4bc^3+12a^4bc^2+12a^4bc+4a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+12a^3bc^3+36a^3bc^2+36a^3bc+10a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+11a^2bc^3+36a^2bc^2+36a^2bc+12a^2b+16a^2c^3+66a^2c^2+84a^2c+33a^2+4ab^3c^3+12ab^3c^2+12ab^3c+4ab^3+ab^2c^3+9ab^2c^2+9ab^2c+2ab^2+4ac^3+ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+43b^2c+16b^2+bc^3+10c^3+11c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1/(1+a),b\\to 1+b,c\\to 1/(1+c)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+87ab^2+12abc^3+6abc^2-4abc+2ab+46ac^3+66ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+18b^2+2bc^3-2bc+10c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$4abc \\le a^2c^2+2ab^2+c^2$$$$2bc \\le b^2+c^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+10a^5b^3c^3+34a^5b^3c^2+38a^5b^3c+14a^5b^3+6a^5b^2c^3+27a^5b^2c^2+36a^5b^2c+15a^5b^2+8a^5bc^3+18a^5bc^2+16a^5bc+6a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+20a^4b^4c^3+60a^4b^4c^2+60a^4b^4c+20a^4b^4+54a^4b^3c^3+182a^4b^3c^2+202a^4b^3c+74a^4b^3+33a^4b^2c^3+144a^4b^2c^2+189a^4b^2c+78a^4b^2+34a^4bc^3+72a^4bc^2+62a^4bc+24a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+40a^3b^4c^3+120a^3b^4c^2+120a^3b^4c+40a^3b^4+116a^3b^3c^3+388a^3b^3c^2+428a^3b^3c+156a^3b^3+72a^3b^2c^3+306a^3b^2c^2+396a^3b^2c+162a^3b^2+56a^3bc^3+108a^3bc^2+88a^3bc+36a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+40a^2b^4c^3+120a^2b^4c^2+120a^2b^4c+40a^2b^4+124a^2b^3c^3+412a^2b^3c^2+452a^2b^3c+164a^2b^3+78a^2b^2c^3+324a^2b^2c^2+414a^2b^2c+168a^2b^2+40a^2bc^3+60a^2bc^2+40a^2bc+20a^2b+100a^2c^3+189a^2c^2+84a^2c+34a^2+20ab^4c^3+60ab^4c^2+60ab^4c+20ab^4+66ab^3c^3+218ab^3c^2+238ab^3c+86ab^3+42ab^2c^3+171ab^2c^2+216ab^2c+85ab^2+12abc^3+6abc^2+2ab+46ac^3+66ac^2+4b^4c^3+12b^4c^2+12b^4c+4b^4+14b^3c^3+46b^3c^2+50b^3c+18b^3+9b^2c^3+36b^2c^2+45b^2c+17b^2+2bc^3+10c^3+12c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1+a,b\\to 1/(1+b),c\\to 1/(1+c)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 4a^5b^4c^3+12a^5b^4c^2+12a^5b^4c+4a^5b^4+16a^5b^3c^3+48a^5b^3c^2+48a^5b^3c+16a^5b^3+24a^5b^2c^3+72a^5b^2c^2+72a^5b^2c+24a^5b^2+16a^5bc^3+48a^5bc^2+48a^5bc+16a^5b+4a^5c^3+12a^5c^2+12a^5c+4a^5+14a^4b^4c^3+46a^4b^4c^2+50a^4b^4c+18a^4b^4+60a^4b^3c^3+196a^4b^3c^2+212a^4b^3c+76a^4b^3+96a^4b^2c^3+312a^4b^2c^2+336a^4b^2c+120a^4b^2+68a^4bc^3+220a^4bc^2+236a^4bc+84a^4b+18a^4c^3+58a^4c^2+62a^4c+22a^4+16a^3b^4c^3+62a^3b^4c^2+76a^3b^4c+30a^3b^4+76a^3b^3c^3+284a^3b^3c^2+340a^3b^3c+132a^3b^3+132a^3b^2c^3+480a^3b^2c^2+564a^3b^2c+216a^3b^2+100a^3bc^3+356a^3bc^2+412a^3bc+156a^3b+28a^3c^3+98a^3c^2+112a^3c+42a^3+4a^2b^4c^3+30a^2b^4c^2+48a^2b^4c+22a^2b^4+28a^2b^3c^3+156a^2b^3c^2+228a^2b^3c+100a^2b^3+60a^2b^2c^3+288a^2b^2c^2+396a^2b^2c+168a^2b^2+52a^2bc^3+228a^2bc^2+300a^2bc+124a^2b+16a^2c^3+66a^2c^2+84a^2c+34a^2+5ab^4c^3+7ab^4c^2+3ab^4c+ab^4+24ab^3c^3+40ab^3c^2+24ab^3c+8ab^3+33ab^2c^3+51ab^2c^2+27ab^2c+9ab^2+18abc^3+22abc^2+6abc+2ab+4ac^3+4ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "\n", + "\\hline\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Substitute $a\\to 1/(1+a),b\\to 1/(1+b),c\\to 1/(1+c)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "Numerator after substitutions: $11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+34a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc-2ab+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+18b^2+38bc^3+56bc^2+2bc+10c^3+14c^2$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From weighted AM-GM inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$2ab \\le a^2+b^2$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 11a^5b^4c^2+16a^5b^4c+9a^5b^4+10a^5b^3c^3+62a^5b^3c^2+74a^5b^3c+38a^5b^3+30a^5b^2c^3+117a^5b^2c^2+120a^5b^2c+57a^5b^2+24a^5bc^3+78a^5bc^2+72a^5bc+34a^5b+8a^5c^3+24a^5c^2+22a^5c+10a^5+9a^4b^4c^3+64a^4b^4c^2+75a^4b^4c+40a^4b^4+86a^4b^3c^3+346a^4b^3c^2+350a^4b^3c+170a^4b^3+195a^4b^2c^3+612a^4b^2c^2+543a^4b^2c+246a^4b^2+142a^4bc^3+384a^4bc^2+298a^4bc+136a^4b+44a^4c^3+114a^4c^2+90a^4c+40a^4+36a^3b^4c^3+146a^3b^4c^2+140a^3b^4c+70a^3b^4+244a^3b^3c^3+764a^3b^3c^2+660a^3b^3c+300a^3b^3+480a^3b^2c^3+1278a^3b^2c^2+972a^3b^2c+414a^3b^2+328a^3bc^3+756a^3bc^2+472a^3bc+204a^3b+96a^3c^3+216a^3c^2+140a^3c+60a^3+54a^2b^4c^3+162a^2b^4c^2+126a^2b^4c+58a^2b^4+312a^2b^3c^3+816a^2b^3c^2+592a^2b^3c+248a^2b^3+558a^2b^2c^3+1284a^2b^2c^2+798a^2b^2c+312a^2b^2+360a^2bc^3+700a^2bc^2+296a^2bc+116a^2b+100a^2c^3+190a^2c^2+84a^2c+33a^2+30ab^4c^3+73ab^4c^2+42ab^4c+19ab^4+166ab^3c^3+370ab^3c^2+206ab^3c+82ab^3+282ab^2c^3+549ab^2c^2+228ab^2c+81ab^2+172abc^3+258abc^2+4abc+46ac^3+66ac^2+7b^4c^3+16b^4c^2+9b^4c+4b^4+38b^3c^3+82b^3c^2+46b^3c+18b^3+63b^2c^3+120b^2c^2+51b^2c+17b^2+38bc^3+56bc^2+2bc+10c^3+14c^2 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -964,25 +3037,92 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 21, "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "numerator: $$21f(-1,4,3)-21f(1,2,3)-21f(2,3,1)+21f(3,-1,4)-21f(3,1,2)+21f(4,3,-1)$$\n", - "denominator: $$1$$\n", - "status: 0\n", - "From Jensen inequality:\n", - "$$21f(1, 2, 3) \\le 11f(-1, 4, 3)+8f(3, -1, 4)+2f(4, 3, -1)$$\n", - "$$21f(2, 3, 1) \\le 8f(-1, 4, 3)+2f(3, -1, 4)+11f(4, 3, -1)$$\n", - "$$21f(3, 1, 2) \\le 2f(-1, 4, 3)+11f(3, -1, 4)+8f(4, 3, -1)$$\n", - "\n", - "$$ 0 \\le \n", - "0 $$\n", - "The sum of all inequalities gives us a proof of the inequality.\n" - ] + "data": { + "text/latex": [ + "numerator: $21f(-1,4,3)-21f(1,2,3)-21f(2,3,1)+21f(3,-1,4)-21f(3,1,2)+21f(4,3,-1)$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "denominator: $1$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "status: 0" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "From Jensen inequality:" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$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)$$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$$ 0 \\le 0 $$" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "The sum of all inequalities gives us a proof of the inequality." + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ diff --git a/shiroindev.py b/shiroindev.py index dcc0e49..1c21cea 100644 --- a/shiroindev.py +++ b/shiroindev.py @@ -4,8 +4,12 @@ import warnings,operator warnings.filterwarnings("ignore") #Seed is needed to select the weights in linprog function. #None means that the seed is random. -sSeed=None -sTranslation={} +class Empty: + pass +sVars=Empty() +sVars.print=print +sVars.seed=None +sVars.translation={} translationList=['numerator:','denominator:','status:', 'Substitute',"Formula after substitution:", "Numerator after substitutions:","From weighted AM-GM inequality:", @@ -19,7 +23,7 @@ translationList=['numerator:','denominator:','status:', ] #Initialize english-english dictionary. for phrase in translationList: - sTranslation[phrase]=phrase + sVars.translation[phrase]=phrase from scipy.optimize import linprog import random from sympy import S,cancel,fraction,Pow,expand,solve,latex @@ -84,12 +88,12 @@ def _input2fraction(formula,variables,values): subst=[] for x,y in zip(variables,values): if y!=1: - print(sTranslation['Substitute'],'$',x,'\\to',slatex(S(y)*S(x)),'$') + sVars.print(sVars.translation['Substitute']+' $'+str(x)+'\\to '+slatex(S(y)*S(x))+'$') subst+=[(x,x*y)] formula=formula.subs(subst) numerator,denominator=fractioncancel(formula) - print(sTranslation['numerator:'],'$$'+slatex(numerator)+'$$') - print(sTranslation['denominator:'],'$$'+slatex(denominator)+'$$') + sVars.print(sVars.translation['numerator:']+' $'+slatex(numerator)+'$') + sVars.print(sVars.translation['denominator:']+' $'+slatex(denominator)+'$') return (numerator,denominator) def _formula2list(formula,variables): #Splits a polynomial to a difference of two polynomials with positive @@ -151,15 +155,15 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ #If there are some inequalities with all integer coefficients, subtract #them from the original one. #If LHS is empty, then break. - localseed=sSeed + localseed=sVars.seed bufer='' itern=0 if len(lcoef)==0: #if LHS is empty - print(sTranslation['status:'], 0) + sVars.print(sVars.translation['status:']+' 0') status=0 elif len(rcoef)==0: #if RHS is empty, but LHS is not - print(sTranslation['status:'], 2) + sVars.print(sVars.translation['status:']+' 2') status=2 itermax=0 foundreal=0 @@ -196,9 +200,9 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ res=linprog(vecc,A_eq=A,b_eq=b,A_ub=A_ub,b_ub=b_ub,options={'maxiter':linprogiter}) status=res.status if itern==1: - print(sTranslation['status:'],status) + sVars.print(sVars.translation['status:']+' '+str(status)) if status==0: - print(sTranslation[theorem]) + sVars.print(sVars.translation[theorem]) if status==2: #if real solution of current inequality doesn't exist if foundreal==0: #if this is the first inequality, then break break @@ -209,7 +213,8 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ bufer='' continue if status==0:#if found a solution with real coefficients - print(bufer,end='') + if bufer: + sVars.print(bufer) foundreal=1 bufer='' oldlfun,oldrfun=lfun,rfun @@ -236,29 +241,28 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ if(c):bufer+='+' else:c=1 bufer+=_writ2(int(round(j)),k,variables) - bufer+='$$\n' + bufer+='$$' lcoef,lfun=_remzero(lcoef,lfun) rcoef,rfun=_remzero(rcoef,rfun) - print(bufer) + sVars.print(bufer) lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)]) if lhs=='': lhs='0' elif status==0: - print(sTranslation[ + sVars.print(sVars.translation[ "Program couldn't find a solution with integer coefficients. Try "+ "to multiple the formula by some integer and run this function again."]) elif(status==2): - print(sTranslation["Program couldn't find any proof."]) + sVars.print(sVars.translation["Program couldn't find any proof."]) #return res.status elif status==1: - print(sTranslation["Try to set higher linprogiter parameter."]) - print('$$ ',slatex(lhs),' \\le ') + sVars.print(sVars.translation["Try to set higher linprogiter parameter."]) rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)]) if rhs=='': rhs='0' - print(slatex(rhs),' $$') + sVars.print('$$ '+slatex(lhs)+' \\le '+slatex(rhs)+' $$') if lhs=='0': - print(sTranslation['The sum of all inequalities gives us a proof of the inequality.']) + sVars.print(sVars.translation['The sum of all inequalities gives us a proof of the inequality.']) return status def _isiterable(obj): try: @@ -287,11 +291,11 @@ def prove(formula,values=None,variables=None,niter=200,linprogiter=10000): st=_list2proof(*(_formula2list(num,variables)+(variables,niter,linprogiter))) if st==2 and issymetric(num): fs=sorted([str(x) for x in num.free_symbols]) - print(sTranslation["It looks like the formula is symmetric. "+ - "You can assume without loss of generality that "], - ' >= '.join([str(x) for x in fs]),sTranslation['Try']) - print('prove(makesubs(S("',num,'"),', - [(str(x),'inf') for x in variables[1:]],')') + sVars.print(sVars.translation["It looks like the formula is symmetric. "+ + "You can assume without loss of generality that "]+ + ' >= '.join([str(x) for x in fs])+'. '+sVars.translation['Try']) + sVars.print('prove(makesubs(S("'+str(num)+'"),'+ + str([(str(x),'inf') for x in variables[1:]])+')') return st def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000): #This is a bruteforce and ineffective function for proving inequalities. @@ -306,7 +310,7 @@ def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000): for j in range(len(variables)): subst2+=[(variables[j],1+variables[j])] for i in range(1<