Proving the existence of localized patterns and saddle node bifurcations in 1D activator-inhibitor type models
Dominic Blanco, Matthieu Cadiot, Daniel Fassler
TL;DR
The paper addresses the constructive verification of stationary localized patterns and saddle-node bifurcations in one-dimensional activator–inhibitor PDEs. It develops a general computer-assisted framework based on a fixed-point formulation and a Newton–Kantorovich scheme, including an explicit approximate inverse of the linearization and contraction estimates to certify local existence and stability near an approximate solution. The approach also provides a rigorous procedure to detect saddle-node bifurcations by solving a well-chosen zero-finding problem and by rigorously controlling the spectrum of the linearization at the bifurcation point. Applications to multiple steady patterns and a saddle-node bifurcation in the Glycolysis model demonstrate the framework's effectiveness across various activator–inhibitor systems.
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.