Computer-assisted proofs in PDE: a survey
Javier Gómez-Serrano
在这次调查中，我们提出了一些最新的结果，计算机辅助证明偏微分方程，集中在那些来自不可压缩流体的问题。特别强调的是技术，而不是结果本身。
In this survey we present some recent results concerning computer-assisted proofs in partial differential equations, focusing in those coming from problems in incompressible fluids. Particular emphasis is put on the techniques, as opposed to the results themselves.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Computer assisted proof of branches of stationary and periodic solution, and Hopf bifurcations, for dissipative PDEs
本文以具有扩散和Dirichlet边界条件的时滞系统为例，讨论了耗散偏微分方程定常解和周期解分支存在性的计算机辅助证明方法，并讨论了周期解分支通过Hopf分支从定常解分支产生的情况.
Symbolic dynamics for Kuramoto-Sivashinsky PDE on the line --- a computer-assisted proof
本文研究了具有奇数和周期边界条件的Kuramoto-Sivashinsky PDE在直线上的符号动力学，通过计算机辅助证明了存在可数无穷多个具有任意大周期的周期轨道。
Validated matrix multiplication transform for orthogonal polynomials with applications to computer-assisted proofs for PDEs
本文针对复杂几何上非线性PDE的严格计算分析，提出验证矩阵乘法变换（MMT）算法以可靠评估谱方法中的非线性项，并结合Zernike多项式构建了圆盘上两类非线性椭圆PDE解存在性的计算机辅助证明。
A computer assisted proof of the symmetries of least energy nodal solutions on squares
本文证明了当$p$接近2时，正方形上Dirichlet边界条件为零的Lane-Emden方程$-Δu = |u|^{p-2}u$的最小能量节点解关于一条对角线为奇数，关于另一条对角线为偶数.我们还表明，这种对称性打破矩形接近正方形。
On turning waves for the inhomogeneous Muskat problem: a computer-assisted proof
我们展示了一个家庭的图形，开发转向奇点（即他们的Lipschitz的爆炸，他们不再是一个图形，通过从稳定的不稳定的政权）的非均匀的，两相Muskat问题的渗透率是由一个非负的阶梯函数。我们研究了不同的渗透率的选择和不同的边界条件（包括在无限远和考虑有限/无限深）的发展或预防的奇性短时间的影响。在一般情况下（非均匀，封闭），我们证明了一个分叉图的外观或不奇点时，介质的深度和渗透率的变化。的证据进行了使用经典的分析技术和计算机辅助验证相结合。
A computer-assisted existence proof for Emden's equation on an unbounded L-shaped domain
我们证明了存在性，非退化，并在无穷远的非平凡的解决方案埃姆登的方程$-Δu = | u |^3$上的一个无界的$L$形域，Dirichlet边界条件的指数衰减。除了这个结果的直接价值，我们也把这个解决方案作为一个积木的解决方案扩大有界域的角落，建立在未来的工作。我们的证明大量使用计算机辅助：从一个数值近似解开始，我们使用一个不动点参数来证明附近的精确解的存在性。在证明过程中建立的特征值界也意味着解的非退化性。
Computer-Assisted Proof of the Main Theorem of 'The Classification of Branched Willmore Spheres in the $3$-Sphere and the $4$-Sphere'
我们使用免费的数学软件Sage对论文“The Classification of Branched Willmore spheres in the $3$ -Sphere and the $4$ -Sphere”（arXiv：1706.01405）中的主要定理4.11中的四次和八次亚纯微分的全纯性进行了计算机辅助证明。
Computer-assisted Proof Under Audit: Typos, Certificate Errors, and Reproducible Exact Checks for a Symbolic Invertibility Proof
本研究对已发表的分析领域计算机辅助证明的证书开展源级审计，发现11处影响证明的缺陷及排版错误，给出反例，指出证书未证明结论，未来将提供更简单的修正证明。
A Computer-Assisted Uniqueness Proof for a Semilinear Elliptic Boundary Value Problem
各种各样的文章，开始与著名的文件（吉达斯，倪和尼伦伯格在通讯。Math.Phys.68，209-243（1979））致力于半线性椭圆边值问题的唯一性问题-Δu=λu+u^p在Ω中，u>0在Ω中，u=0在Ω的边界上，其中λ的范围在0和第一Dirichlet Laplacian特征值之间。到目前为止，这个问题在Ω是球的情况下得到了解决，对于更一般的域，在λ=0的情况下得到了解决。在（McKenna等人，J. Differ.当量ag 247，2140-2162（2009）），我们提出了一种计算机辅助的方法来解决这个唯一性问题，它确实在Ω=（0，1）x（0，1）和p=2的情况下提供了证明。由于高数值复杂性，我们无法在（McKenna等人，J. Differ.当量ag 247，2140-2162（2009））来处理更高的p值。这里，通过显著降低复杂度，我们将证明p=3的情况的唯一性。
Computer-assisted validation of the existence of periodic orbit in the Brusselator system
本文研究带扩散和Dirichlet边界条件的Brusselator系统，通过计算机辅助和偏微分方程严格积分证明了特定参数下周期轨道的存在性，并给出了倍周期分岔的证据。
On the potential lack of response in a model of second-harmonic generation. A computer-assisted proof
本文通过计算机辅助证明，严格验证了非线性光学中二次谐波产生模型在低频区域存在广义透射特征值，其特征函数具有爆破解行为，并提供了开源算法实现。
Computer-Assisted Proofs of Gap Solitons in Bose-Einstein Condensates
本文提出通过计算机辅助证明方法，首次在非扰动参数域中严格证明了格罗斯-皮塔耶夫斯基方程中间隙孤子的存在性。
Existence and instability of steady states for a triangular cross-diffusion system: a computer-assisted proof
在本文中，我们提出并应用计算机辅助方法来研究一个三角形交叉扩散系统的平衡态。我们的方法包括在一个后验验证过程中，这是基于使用一个固定点参数周围的数值计算的解决方案，在牛顿-康托洛维奇定理的精神。它使我们能够证明存在各种非齐次稳态不同的参数值。在某些情况下，我们得到多达13个共存的稳态。我们还应用后验验证程序来研究所获得的稳态的线性稳定性，证明他们中的许多人实际上是不稳定的。
Numerical Computations and Computer Assisted Proofs of Periodic Orbits of the Kuramoto-Sivashinsky Equation
我们提出的数值结果和计算机辅助证明的存在性周期轨道的Kuramoto-Sivashinky方程。这两个结果都是基于将周期轨道的存在性记为泛函的零点。这导致使用牛顿算法的数值计算的解决方案，并结合严格的区间运算的一些后验分析，严格验证的存在性的解决方案。这是在[19]中为几种类型的轨道开发的方法的一个特殊情况。[33]中出现了一个独立的实现，覆盖重叠但不同的地面，使用不同的功能设置。
Continuation of homoclinic orbits in the suspension bridge equation: a computer-assisted proof
本文证明了吊桥方程$u""+βu" + e^u-1=0$对所有参数值$β\in [0.5,1.9]$的对称同宿轨道的存在性。对每个$β$，计算稳定流形的参数化，并通过求解投影边值问题得到对称同宿轨道.证明是计算机辅助的，并结合了一致收缩定理和半径多项式的方法，它提供了一种有效的手段来确定一个集，集中在一个数值逼近的解决方案，在这类牛顿算子是一个收缩。
Singularities and heteroclinic connections in complex-valued evolutionary equations with a quadratic nonlinearity
本文研究了复值演化偏微分方程（PDE）解的动力学性质，并通过计算机辅助证明证明了从非平凡平衡点到零的异宿轨道的存在性.我们还表明，存在的无界解沿非稳定流形在平衡点以下的异宿轨道的存在。我们的计算机辅助证明由三个独立的技术严格的数值：一个封闭的本地非稳定流形的平衡，一个严格的集成偏微分方程，和建设性的验证零平衡周围的捕获区域。
Existence of globally attracting solutions for one-dimensional viscous Burgers equation with nonautonomous forcing - a computer assisted proof
本文通过计算机辅助证明，证明了在特定粘性和非自治强迫下，一维粘性Burgers方程在周期边界条件下存在全局吸引解，且强迫周期性时解也周期性。
Computer-assisted proofs for some nonlinear diffusion problems
在过去的三十年中，强大的计算机辅助技术已经发展，以验证形式为$Δu +f(u,\nabla u) = 0$的半线性椭圆问题的后验数值解。通过研究定义在数值解周围的一个精心选择的不动点问题，这些技术使得有可能证明解在数值解的一个显式（通常很小）邻域中的存在性。在这项工作中，我们开发了一个类似的方法，更广泛的系统，包括非线性扩散项的形式$ΔΦ(u)$。特别是，这使我们能够获得新的结果，从人口动力学的交叉扩散系统的稳定状态：（非三角形）SKT模型。我们还重新审视了计算机辅助证明的背景下，自动微分的想法，并提出了一种基于微分-代数方程的替代方法。
Computer-assisted proofs for the many steady states of a chemotaxis model with local sensing
本文研究具有局部感知的趋化交叉扩散方程组的多个稳态，提出基于傅里叶级数分解和不动点论证的计算机辅助证明方法，以处理非多项式非线性并严格验证多种共存平衡态的存在性。
From heteroclinic loops to homoclinic snaking in reversible systems: rigorous forcing through computer-assisted proofs
本文利用计算机辅助证明在时间可逆系统中构造平衡点与周期轨道之间的异宿连接参数化环，从而严格证明了 Swift-Hohenberg 和 Gray-Scott 问题中的同宿蛇形现象，展示了计算机辅助方法在分析非线性系统全局动力学中的有效性。
Rigorous numerics for ill-posed PDEs: periodic orbits in the Boussinesq equation
本文开发了用于分析不稳定性偏微分方程周期轨道的计算机辅助技术，以Boussinesq方程为例，通过利用解的对称性和牛顿-康托罗维奇类型论证（半径多项式方法），在具有几何衰减的加权ℓ¹Banach空间中严格证明了周期轨道的存在性。
Turing instability for nonlocal heterogeneous reaction-diffusion systems: A computer-assisted proof approach
本文提出一种计算机辅助证明方法，通过基变换和Gershgorin圆盘定理处理异质非局部反应扩散系统中的强耦合无限微分系统，证明了图灵不稳定性，并得出分岔点的精确阈值。
Analytic finite-rank corrections for singularly weighted estimates in a computer-assisted proof of 3D Euler singularity
研究流体方程自相似奇点形成的计算机辅助证明中奇异加权估计问题，通过回顾解析低秩修正方法，在数值步骤确定相关量，利用泰勒展开导出低秩修正执行消失条件，还介绍其在二维布辛涅斯克/三维欧拉稳定性论证中的应用及更广泛适用性。
Computer-assisted proof of heteroclinic connections in the one-dimensional Ohta-Kawasaki model
本文基于一维Ohta-Kawasaki模型，通过计算机辅助证明了异稳连接的存在，揭示了在该模型中局部和全局能量极小值之间的连接，以及在该模型中存在多稳态行为，与Cahn-Hilliard方程不同。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。