二维 Gray-Scott 方程组：局域定态模式存在性的构造性证明

在本文中，我们提出了一个用于在半线性偏微分方程组中构造光滑局域解的综合框架，特别侧重于 Gray-Scott 模型。具体而言，我们构造了一个用于研究自治半线性 PDE 方程组的自然 Hilbert 空间 $\mathcal{H}$，在该空间上乘积和微分算子是良定义的。然后，给定一个近似解 $\mathbf{u}_0$，我们基于在 $\mathbf{u}_0$ 附近线性化的近似逆的构造，推导了一种 Newton-Kantorovich 方法。特别地，我们推导出了一个条件，在此条件下我们证明了在 $\mathbf{u}_0$ 的邻域内存在唯一解。该条件可以通过不同上界的显式计算来验证，我们给出了其分析细节。此外，我们提供了一个额外条件，在此条件下证明了局域模式是（空间）周期解的无界分支在周期趋于无穷大时的极限。然后，我们通过（构造性地）证明 2D Gray-Scott 模型中四种不同局域模式的存在性来演示我们的方法。此外，这些解被证明满足 $D_4$ 对称性，即正方形的对称性。执行计算机辅助证明的算法细节可在 GitHub 上获取。