Непростое неравенство

[g______d]

Побуду немного занудой и добавлю, что в принципе, проверка истинности системы полиномиальных неравенств с рациональными коэффициентами -- алгоритмически разрешимая задача.

https://en.wikipedia.org/wiki/Tarski–Seidenberg_theorem
https://en.wikipedia.org/wiki/Decidabil ... al_numbers

https://en.wikipedia.org/wiki/Cylindric ... omposition

(но время работы очень длинное).

Конкретно для данных неравенств, если бы стояла задача придумать computer assisted proof, я бы перенёс всё влево и искал минимум получившейся функции (там нужно будет сводить всё к октанту на сфере, поскольку функция однородная, таким образом, параметров на самом деле два). Сначала можно проверить внутренние точки области, для них обе производных должны обращаться в нуль, это два полиномиальных уравнения с двумя неизвестными, скорее всего с помощью базисов Грёбнера это сведётся к перебору конечного числа точек. Кроме этих точек, нужно ещё проверить границу области; но на границе это будет уже одномерная задача, там уже как-нибудь получится.

Интересно (хотя здесь наверное оффтоп), насколько GPU могут ускорить эти алгоритмы.

[g______d]

Решило! Минуты за две. Всё, больше не буду спамить.

In[1]:= FullSimplify[
 CylindricalDecomposition[{a^3/(13 a^2 + 5 b^2) + 
     b^3/(13 b^2 + 5 c^2) + c^3/(13 c^2 + 5 a^2) >= (a + b + c)/18, 
   a > 0, b > 0, c > 0}, {a, b, c}]]

Out[1]= a > 0 && b > 0 && c > 0

[nnosipov]

g______d в сообщении #1351514 писал(а):

Конкретно для данных неравенств, если бы стояла задача придумать computer assisted proof, я бы перенёс всё влево и искал минимум получившейся функции (там нужно будет сводить всё к октанту на сфере, поскольку функция однородная, таким образом, параметров на самом деле два). Сначала можно проверить внутренние точки области, для них обе производных должны обращаться в нуль, это два полиномиальных уравнения с двумя неизвестными, скорее всего с помощью базисов Грёбнера это сведётся к перебору конечного числа точек. Кроме этих точек, нужно ещё проверить границу области; но на границе это будет уже одномерная задача, там уже как-нибудь получится.

Я тоже так думал, пока не попробовал реализовать этот план на каком-нибудь неочевидном примере. На самом деле, может возникнуть куча дополнительных технических проблем с непредсказуемым результатом.

А вот то, что

CylindricalDecomposition

работает, и за очень разумное время --- это уже интересно. Другое дело, мы опять, скорее всего, не узнаем, насколько этим доказательствам можно доверять (я имею в виду Mathematica).

[g______d]

nnosipov в сообщении #1390648 писал(а):

Другое дело, мы опять, скорее всего, не узнаем, насколько этим доказательствам можно доверять (я имею в виду Mathematica).

Ну, это далеко не новый алгоритм, и он много где реализован. Вот нашёл обзор с большим количеством ссылок (в том числе и на программы с открытым кодом).

https://arxiv.org/pdf/1504.06484.pdf

Я так понимаю, что вариациями на его тему активно пользуются при компьютерной формализации доказательств.

[nnosipov]

g______d в сообщении #1390652 писал(а):

Вот нашёл обзор с большим количеством ссылок

Да, спасибо. Авторы известны, особенно первый.

[kotenok gav]

Есть еще такая книга, посвященная как раз таким доказательствам, очень хорошая. A=B называется, вроде.

[g______d]

Она в основном про комбинаторные тождества, судя по всему. Это другое.

[kotenok gav]

Далеко нет. Она в основном про нахождение суммы гипергеометрических функций. Возможно, там и для неравенств что-нибудь найдется.

[g______d]

kotenok gav в сообщении #1390834 писал(а):

Возможно, там и для неравенств что-нибудь найдется.

Если не открывать книгу -- то возможно.

[Rak so dna]

arqady в сообщении #1141802 писал(а):

Для положительных $a$, $b$ и $c$ докажите, что:

$$\frac{a^3}{13a^2+5b^2}+\frac{b^3}{13b^2+5c^2}+\frac{c^3}{13c^2+5a^2}\geq\frac{a+b+c}{18}$$

\small\begin{align*} &\frac{18}{5}\bigl(13\,a^2+5\,b^2\bigr)\bigl(13\,b^2+5\,c^2\bigr)\bigl(13\,c^2+5\,a^2\bigr)\left( \frac{a^3}{13\,a^2+5\,b^2}+\frac{b^3}{13\,b^2+5\,c^2}+\frac{c^3}{13\,c^2+5\,a^2} - \frac{a+b+c}{18} \right) = \\\\ &=\frac{1}{171}\sum\limits_{cyc}{a\,\Bigl((83\,b+40\,c)\,a^2-(80\,b^2-32\,b\,c+162\,c^2)\,a+b\,c\,(12\,b+75\,c)\Bigr)^2}+ \\ &+\frac{25}{18297}\sum\limits_{cyc}{a\,\Bigl( (134\,b-107\,c)\,a^2-(103\,b^2+92\,b\,c-141\,c^2)\,a+b\,c\,(137\,b-110\,c) \Bigr)^2}+ \\ &+\frac{1094}{737979}\sum\limits_{cyc}{a^2\,c\,\left(b-c\right)^2\left(8\,a+3\,b-11\,c\right)^2}+\frac{4}{2213937}\sum\limits_{cyc}{a\,c\,\left(a-b\right)^2\left(b-c\right)^2\bigl(123\,a+194205\,b+176\,c\bigr)} \end{align*}

(maxima code)

f(t) := 18/5*(13*a^2+5*b^2)*(13*b^2+5*c^2)*(13*c^2+5*a^2)*(  a^3/(13*a^2+5*b^2) + b^3/(13*b^2+5*c^2) + c^3/(13*c^2+5*a^2) - (a+b+c)/18  ) ;

r(t) := 

1/171*(
     c*( (83*a+40*b)*c^2-(80*a^2-32*a*b+162*b^2)*c+a*b*(12*a+75*b) )^2
  + a*( (83*b+40*c)*a^2-(80*b^2-32*b*c+162*c^2)*a+b*c*(12*b+75*c) )^2
  + b*( (83*c+40*a)*b^2-(80*c^2-32*c*a+162*a^2)*b+c*a*(12*c+75*a) )^2
)

+ 25/18297*(
     c*( (134*a-107*b)*c^2-(103*a^2+92*a*b-141*b^2)*c+a*b*(137*a-110*b) )^2
  + a*( (134*b-107*c)*a^2-(103*b^2+92*b*c-141*c^2)*a+b*c*(137*b-110*c) )^2
  + b*( (134*c-107*a)*b^2-(103*c^2+92*c*a-141*a^2)*b+c*a*(137*c-110*a) )^2  
)

+ 1094/737979*(
     a^2*c*(b-c)^2*(8*a+3*b-11*c)^2
  + b^2*a*(c-a)^2*(8*b+3*c-11*a)^2
  + c^2*b*(a-b)^2*(8*c+3*a-11*b)^2
)

+ 4/2213937*(
     a*c*(a-b)^2*(b-c)^2*(123*a+194205*b+176*c)
  + b*a*(b-c)^2*(c-a)^2*(123*b+194205*c+176*a)
  + c*b*(c-a)^2*(a-b)^2*(123*c+194205*a+176*b)
) ;

rat(f(t) - r(t));