Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations

در دهه‌های گذشته، مسائل ریاضی مختلفی توسط اثبات‌های کامپیوتری حل شده‌اند، از جمله حدس کپلر، وجود هرج و مرج، وجود جاذبه لورنز، مسئله معروف چهار رنگ و موارد دیگر. در بسیاری از موارد، اثبات‌های به کمک رایانه دارای مزیت قابل‌توجهی هستند (در مقایسه با یک اثبات «تئوری») و همچنین اطلاعات کمی دقیق را ارائه می‌کنند.

نویسندگان بیش از ربع قرن برای ایجاد روش‌هایی برای تأیید صحت کار کرده‌اند. محاسبه راه‌حل‌های معادلات دیفرانسیل جزئی، عمدتاً برای مسائل بیضی غیرخطی به شکل -∆u=f(x,u,∇u) با شرایط مرزی دیریکله. در اینجا منظور از "محاسبات تایید شده" یک رویکرد عددی به کمک کامپیوتر برای اثبات وجود یک راه حل در یک همسایگی نزدیک و صریح از یک راه حل تقریبی است. اطلاعات کمی ارائه شده توسط این تکنیک ها نیز از دیدگاه تخمین های خطای پسینی برای حل های تقریبی معادلات دیفرانسیل جزئی مربوطه به معنای دقیق ریاضی قابل توجه است.

در این تک نگاری، نویسندگان شرح مفصلی از محاسبات تایید شده و اثبات های کامپیوتری برای معادلات دیفرانسیل جزئی که آنها ایجاد کردند. در بخش اول، روش‌هایی که عمدتاً توسط نویسندگان ناکائو و واتانابه مورد مطالعه قرار گرفته‌اند، ارائه شده‌اند. این روش‌ها مبتنی بر پیش‌بینی ابعاد محدود و تخمین‌های خطای پیشینی سازنده برای تقریب‌های اجزای محدود معادله پواسون هستند. در بخش دوم، رویکردهای کامپیوتری از طریق مرزهای ارزش ویژه توسعه یافته توسط نویسنده Plum به تفصیل توضیح داده شده است. وظیفه اصلی این روش شامل ایجاد مرزهای مقدار ویژه برای خطی کردن مسئله غیرخطی مربوطه در راه حل تقریبی محاسبه شده است. برخی از اظهارات کوتاه در مورد سایر رویکردها نیز در بخش سوم آورده شده است. هر روش در بخش های I و II با مثال های عددی مناسب همراه است که سودمندی واقعی روش های نویسندگان را تایید می کند. همچنین در برخی از نمونه‌ها الگوریتم‌های کامپیوتری کاربردی ارائه شده است تا خوانندگان بتوانند به راحتی برنامه‌های تأیید را خودشان پیاده‌سازی کنند.

In the last decades, various mathematical problems have been solved by computer-assisted proofs, among them the Kepler conjecture, the existence of chaos, the existence of the Lorenz attractor, the famous four-color problem, and more. In many cases, computer-assisted proofs have the remarkable advantage (compared with a “theoretical” proof) of additionally providing accurate quantitative information.

The authors have been working more than a quarter century to establish methods for the verified computation of solutions for partial differential equations, mainly for nonlinear elliptic problems of the form -∆u=f(x,u,∇u) with Dirichlet boundary conditions. Here, by “verified computation” is meant a computer-assisted numerical approach for proving the existence of a solution in a close and explicit neighborhood of an approximate solution. The quantitative information provided by these techniques is also significant from the viewpoint of a posteriori error estimates for approximate solutions of the concerned partial differential equations in a mathematically rigorous sense.

In this monograph, the authors give a detailed description of the verified computations and computer-assisted proofs for partial differential equations that they developed. In Part I, the methods mainly studied by the authors Nakao and Watanabe are presented. These methods are based on a finite dimensional projection and constructive a priori error estimates for finite element approximations of the Poisson equation. In Part II, the computer-assisted approaches via eigenvalue bounds developed by the author Plum are explained in detail. The main task of this method consists of establishing eigenvalue bounds for the linearization of the corresponding nonlinear problem at the computed approximate solution. Some brief remarks on other approaches are also given in Part III. Each method in Parts I and II is accompanied by appropriate numerical examples that confirm the actual usefulness of the authors’ methods. Also in some examples practical computer algorithms are supplied so that readers can easily implement the verification programs by themselves.