Rigorous verification of Hopf bifurcations in functional differential equations

We propose a rigorously validated numerical method to prove the existence of Hopf bifurcations in functional differential equations of mixed type. The eigenvalue transversality and steady state conditions are verified using the Newton-Kantorovich theorem. The non-resonance condition and simplicity of the critical eigenvalues are verified by either computing a pair of generalized Morse indices of the step map, or by applying the argument principle to the characteristic equation and a suitable contour in the complex plane, computing the contour integral with a rigorous integration approach based on Taylor expansion. As a first application and test problem, we prove the existence of Hopf bifurcations in the Lasota-Wazewska-Czyzewska model and a pair of two such coupled equations. We then use our method to prove the existence of periodic traveling waves in the Fisher equation with nonlocal reaction. These periodic traveling waves are solutions of an ill-posed functional differential equation of mixed type.