2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3
 
 Re: Непростое неравенство
Сообщение03.11.2018, 22:02 
Заслуженный участник
Аватара пользователя


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

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 могут ускорить эти алгоритмы.

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение02.05.2019, 07:01 
Заслуженный участник
Аватара пользователя


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

Код:
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

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение02.05.2019, 08:09 
Заслуженный участник


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

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

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение02.05.2019, 08:32 
Заслуженный участник
Аватара пользователя


08/11/11
5553
nnosipov в сообщении #1390648 писал(а):
Другое дело, мы опять, скорее всего, не узнаем, насколько этим доказательствам можно доверять (я имею в виду Mathematica).


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

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

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

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение02.05.2019, 08:54 
Заслуженный участник


20/12/10
6078
g______d в сообщении #1390652 писал(а):
Вот нашёл обзор с большим количеством ссылок
Да, спасибо. Авторы известны, особенно первый.

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение03.05.2019, 14:04 


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

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение03.05.2019, 18:52 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение03.05.2019, 20:26 


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

 Профиль  
                  
 
 Re: Непростое неравенство
Сообщение04.05.2019, 03:33 
Заслуженный участник
Аватара пользователя


08/11/11
5553
kotenok gav в сообщении #1390834 писал(а):
Возможно, там и для неравенств что-нибудь найдется.


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 39 ]  На страницу Пред.  1, 2, 3

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group