1D 激活-抑制模型中局部模式与鞍点分叉的存在性证明

本文提出了一套用于构造性证明 1D 激活-抑制系统中 stationary（平稳）局部解及鞍点分叉存在性和稳定性的通用框架，采用计算机辅助证明方法。具体而言，我们开发了计算 Newton--Kantorovich 方法中所需显式上界的必要分析。给定一个近似解 $\bar{\mathbf{u}}$，该方法依赖于在 $\bar{\mathbf{u}}$ 的邻域内建立一个选取合适的固定点映像是收缩的。为此，我们构造对 $\bar{\mathbf{u}}$ 处线性化的近似逆，并确立实现收缩的充分条件。这为一种可应用于计算机辅助分析的框架提供了支持，以验证 $\bar{\mathbf{u}}$ 附近解的存在性和局部唯一性，并控制 $\bar{\mathbf{u}}$ 处的线性化。此外，我们将该方法扩展到严格建立相同模型类型的局部解的鞍点分叉，通过考虑一个选取合适的零点寻找出问题。这取决于对 $\bar{\mathbf{u}}$ 处分叉点的线性化谱的严格控制。最后，我们通过在各种激活-抑制系统中证明多个稳态图案的存在性与稳定性，以及在糖酵解模型中证明鞍点分叉来展示该框架的有效性。