Title: Proving the existence of localized patterns and saddle node bifurcations in 1D activator-inhibitor type models Show Chinese title

Title: 证明一维激活剂-抑制剂类型模型中局部模式和鞍点分支的存在性

Abstract: In this paper, we present a general framework for constructively proving the existence and stability of stationary localized 1D solutions and saddle-node bifurcations in activator--inhibitor systems using computer-assisted proofs. Specifically, we develop the necessary analysis to compute explicit upper bounds required in a Newton--Kantorovich approach. Given an approximate solution $\bar{\mathbf{u}}$, this approach relies on establishing that a well-chosen fixed point map is contracting on a neighborhood $\bar{\mathbf{u}}$. For this matter, we construct an approximate inverse of the linearization around $\bar{\mathbf{u}}$, and establish sufficient conditions under which the contraction is achieved. This provides a framework for which computer-assisted analysis can be applied to verify the existence and local uniqueness of solutions in a vicinity of $\bar{\mathbf{u}}$, and control the linearization around $\bar{\mathbf{u}}$. Furthermore, we extend the method to rigorously establish saddle-node bifurcations of localized solutions for the same type of models, by considering a well--chosen zero--finding problem. This depends on the rigorous control of the spectrum of the linearization around the bifurcation point. Finally, we demonstrate the effectiveness of the framework by proving the existence and stability of multiple steady-state patterns in various activator--inhibitor systems, as well as a saddle--node bifurcation in the Glycolysis model. Show Chinese abstract

Abstract: 在本文中，我们提出了一种通用框架，使用计算机辅助证明来构造性地证明激活子-抑制子系统中静态局域1D解和鞍点分岔的存在性和稳定性。 具体来说，我们开发了必要的分析来计算牛顿-康托罗维奇方法所需的显式上界。 给定一个近似解$\bar{\mathbf{u}}$，该方法依赖于在邻域$\bar{\mathbf{u}}$上建立一个经过良好选择的不动点映射是收缩的。 为此，我们构建了围绕$\bar{\mathbf{u}}$的线性化的一个近似逆，并建立了在这些条件下收缩得以实现的充分条件。 这提供了一个框架，使得计算机辅助分析可以应用于验证在$\bar{\mathbf{u}}$附近的解的存在性和局部唯一性，并控制围绕$\bar{\mathbf{u}}$的线性化。 此外，我们通过考虑一个经过良好选择的零点寻找问题，将该方法扩展到严格建立相同类型模型中局域解的鞍点分岔。 这取决于在分岔点周围线性化的谱的严格控制。 最后，我们通过证明各种激活子-抑制子系统中多个稳态模式的存在性和稳定性，以及糖酵解模型中的一个鞍点分岔，展示了该框架的有效性。