Development of Computer-Assisted Proofs in Dynamical Systems

About

This workshop brings together researchers working on rigorous, computer-assisted methods for the study of dynamical systems. Topics span validated numerics, and constructive proofs in finite- and infinite-dimensional dynamical systems.

Speakers

• Jan Bouwe van den BergVrije Universiteit Amsterdam
• Hugo ChuÉcole Polytechnique
• Kevin ConstantineauMcGill University
• Alvaro Fernandez MoraMonash University
• Olivier HénotNational Taiwan University
• Jonathan JaquetteNew Jersey Institute of Technology
• Xuefeng LiuTokyo Woman's Christian University
• Kaname MatsueKyushu University
• Juan MirandaFlorida Atlantic University
• Konstantin MischaikowRutgers University
• Hiroaki MiyauchiUniversity of Tsukuba
• Keiichi MorikuniUniversity of Tsukuba

Schedule

1. Day 1Wednesday 9 September

   1. 09:30–10:30 Konstantin Mischaikow Computer-assisted proofs and latent dynamics abstract

      The motivation for this talk is twofold.

      The global dynamics of high dimensional or infinite dimensional systems can be extremely complicated. To be a bit more explicit, consider parameter dependent partial differential equations that model formation of amorphous or crystalline materials. As a function of the parameters the dimension and complexity of the dynamics on the global attractor grow dramatically and the number of attractors can change. Thus a rigorous understanding of the global dynamics is probably computationally intractable.

      Much of the above mentioned dynamics is of limited interest in applications. For material science the most fundamental question is: as a function of parameters what is the domain of attraction of the attractors that correspond to desirable or undesirable material?

      I will describe some recent results. The first is a theorem that indicates that at least theoretically we can learn dynamics as expressed by Morse representations and Conley indices from data. The second is a theorem that indicates that given an explicit bound an attracting block obtained from a low dimensional latent dynamical system can be lifted to an attracting block of the high dimensional system. I will show some numerical results and then pose the question of whether with additional analysis these numerical results can be made rigorous.

   2. 10:30–11:00 Break
   3. 11:00–12:00 Xuefeng Liu Non-uniqueness of Leray–Hopf solutions: computer-assisted approaches with and without axisymmetry abstract

      The non-uniqueness of Leray–Hopf solutions to the unforced 3D Navier–Stokes equations was recently established by Hou, Wang and Yang through a computer-assisted proof, in which a self-similar profile is constructed and a second solution obtained from an unstable eigenvalue of the linearization about it. Their framework exploits axisymmetry, which reduces incompressibility to a scalar stream function.

      This talk reviews that result and then presents an on-going approach designed to dispense with axisymmetry, where no such reduction exists. The proposal is to enforce incompressibility at the discrete level using exactly divergence-free Scott–Vogelius finite elements, and to quantify the associated projection error by an extended hypercircle (Prager–Synge) estimate with explicit constants, so that verified computation can supply the bounds a rigorous existence argument needs.

   4. 12:00–14:00 Lunch 🍱
   5. 14:00–15:00 Jan Bouwe van den Berg CAPs for localized traveling waves in the two-dimensional suspension bridge equation abstract

      Traveling waves are a central feature in the dynamics of the suspension bridge PDE. While most studies have focused on the one-dimensional case, we develop computer-assisted proof (CAP) techniques to rigorously establish the existence of periodic and localized traveling waves in two dimensions. Our approach relies on a Newton-Kantorovich framework combined with careful Fourier analysis, where the main challenge is the combination of the exponential nonlinearity and the large amplitudes of the wave. By deriving computable bounds that control aliasing errors, we can control both the residue and the contraction constant of the fixed point operator sufficiently to prove the existence of traveling wave solutions. Moreover, the methodology provides explicit bounds on numerical deficiencies and allows us to enclose the spectrum of the linearized operator rigorously, yielding conclusions about orbital stability. This talk is based on work with and by Lindsey van der Aalst, Matthieu Cadiot, Jean-Philippe Lessard.

   6. 15:00–16:00 Keiichi Morikuni Verified numerical eigenvalue computation of differential operators using complex moments with applications to Schrödinger and Mathieu equations abstract

      A numerical verification analogue of our operator eigensolver is established to enclose eigenvalues of a linear, self-adjoint, and ordinary differential operator in a Hilbert space. The eigensolver computes complex moments via contour integration of the resolvent along a path enclosing the interval on the real axis that contains the desired eigenvalues. These moments then form a block Hankel matrix pencil whose eigenvalues include those of interest. The truncation error arising from approximating the integral by a quadrature rule depends on the spectrum lying outside the region of interest. To obtain an explicit bound on this exterior spectrum, we focus on the case where the operator is a perturbed Laplacian and evaluate the effect of the perturbation via the Krylov–Weinstein bound. Numerical experiments on Mathieu’s and Schrödinger’s equations demonstrate the performance of the method.

   7. 16:00–16:30 Break
   8. 16:30–17:00 Kevin Constantineau Platonic constellations of periodic motions in the $(n+1)$-body problem abstract

      We study the spatial $(n+1)$-body problem formed by one heavy central mass together with $n$ equal masses placed on a single orbit of a polyhedral rotation group $H\in\{\mathbb{T},\mathbb{O},\mathbb{I}\}$, so that $n=|H|\in\{12,24,60\}$. Imposing the symmetry $q_{L}=L\,q_{I}$ for $L\in H$ reduces the problem to a single $2\pi$-periodic reference curve, with reduced action $\mathcal{A}_{H}=\mathcal{A}_{0}+\varepsilon \mathcal{A}_{1}$, in which $\varepsilon$ is the inverse central mass and $\mathcal{A}_{0}$ is the Kepler action. At $\varepsilon=0$ the critical set contains, as one connected component, the five-dimensional manifold of Kepler ellipses of minimal period $2\pi$, which we prove to be a nondegenerate critical manifold. A Lyapunov–Schmidt reduction along this manifold turns the continuation problem into the search for nondegenerate critical points of an explicit function $\Phi(e,\psi)$ of the eccentricity $e$ and the spatial orientation $\psi$. We verify this condition by a computer-assisted argument in which we rigorously compute integrals using Fourier methods. We thereby obtain, for each of the three groups, families of periodic solutions of the $(n+1)$-body problem with $n+1\in\{13,25,61\}$ bodies, bifurcating from Kepler ellipses and carrying the full tetrahedral, octahedral, or icosahedral symmetry.

2. Day 2Thursday 10 September

   1. 10:00–11:30 Olivier Hénot Tutorial — RadiiPolynomial.jl Download slides · Pluto notebook ↓
   2. 12:00–14:00 Lunch 🍱
   3. 14:00–15:00 Jonathan Jaquette Axisymmetric Navier–Stokes equations with swirl: computer-assisted proofs of steady states with an eye towards richer dynamics abstract

      The global regularity of solutions to the 3D Navier–Stokes equations is famously unknown, and the axisymmetric case with swirl is perhaps the simplest geometry in which blowup may occur. We study this setting on a periodic cylinder with no-slip boundary conditions and time-independent body forcing, where weak solutions are guaranteed to have a global attractor and computer-assisted proofs are uniquely positioned to give rigorous results in a non-perturbative regime. In this geometry the equations reduce to a system in a periodic axial variable and a radial variable. In any problem one wants the basis used to express solutions to have several desirable properties: easy to express differential operators, easy to compute products, and rapid convergence properties. Fourier series are best for periodic domains, but there is no uniformly best option for radial variables.

      Our approach for developing computer-assisted proofs of steady states of the Navier-Stokes equations in a cylindrical domain uses a Fourier–Jacobi (Zernike) basis. This approach has its advantages: the differential operators act as sparse ladder and conversion operators between Jacobi families; multiplication via interpolation may be computed accurately and relatively quickly; the spectral coefficients of solutions converge geometrically. However laborious quantitative estimates are required for the computer-assisted proof: e.g. the derivative nonlinearity requires bilinear estimates from multiplying different polynomial bases, and inverting the Stokes operator on this basis and recovering explicit decay estimates requires significant effort. With this infrastructure in place we prove the existence of steady states, and we expect the framework to apply more broadly to PDEs in cylindrical geometries, and to richer dynamics.

   4. 15:00–16:00 Alvaro Fernandez Mora Computer-assisted approach for the infinitesimal Hilbert 16th problem abstract

      The infinitesimal Hilbert's 16th problem asks for a uniform upper bound on the number of limit cycles in polynomial Hamiltonian vector fields under polynomial perturbations. Let Z(n) denote this maximum number of limit cycles, where n is the degree of the perturbation and n+1 is the degree of the Hamiltonian. Upper bounds for Z(n) remain largely unknown even for low degrees. In this work, we present novel computer-assisted techniques to approach this classical problem. We apply our framework to construct an alternative proof of the celebrated result Z(2)=2. While the quadratic case is one of the few cases that has been fully solved, our primary objective is to build a scalable toolkit capable of overcoming the algebraic complexity that currently limits the study of Z(n) for large n.

   5. 18:00 Workshop dinner 🍶 京の禅 車 四条烏丸店 · Kyō-no-Zen Kuruma, Shijō-Karasuma

3. Day 3Friday 11 September

   1. 10:00–11:00 Kaname Matsue Algebraic-dynamical correspondence of oscillatory blow-up solutions abstract

      Rigorous detection and characterization of blow-up solutions to differential equations constitute challenging problems in differential equations and numerical analysis, particularly in understanding the global behavior of solutions and in dealing with dynamics at infinity.

      In recent years, a combination of rigorous numerics (computer-assisted proofs) and techniques from dynamical systems, including compactifications, time-scale desingularizations, and invariant manifold theory, has provided a systematic methodology for capturing both qualitative and quantitative properties of blow-up solutions for certain classes of ordinary differential equations. Despite its potential, however, this approach may require substantial and intricate computations associated with compactification and desingularization.

      An alternative viewpoint is provided by an algebraic-dynamical correspondence based on asymptotic expansions of type-I blow-up solutions. On the algebraic side, the leading-order asymptotic profiles and their scaling exponents are characterized by balance relations derived directly from the original differential equations. On the dynamical side, these profiles are related to invariant structures governing the dynamics at infinity. This correspondence makes it possible to extract essential information on blow-up behavior without explicitly constructing a compactification, while retaining a connection with the dynamical mechanisms responsible for the singularity.

      In this talk, I will present a recent development of this framework for blow-up solutions exhibiting oscillatory divergence. In particular, I will discuss how periodic solutions of the associated balance equation are related to oscillatory blow-up trajectories and how their dynamical properties determine the asymptotic behavior of the original solutions. Several concrete examples will be presented to illustrate the correspondence. The resulting framework provides a structural description of oscillatory blow-up and may also offer a useful basis for future rigorous numerical studies of a broader class of finite-time singularities.

   2. 11:00–11:30 Juan Miranda Computer-assisted proofs for nonlinear problems in the Borel plane and validated numerics for complex convolutions abstract

      The Borel transform is a useful tool for studying functional equations whose solutions are infinitely differentiable but not analytic. For nonlinear problems, matters are complicated by the fact that the transform takes pointwise multiplications to complex convolutions. Nevertheless, Bonckaert and Maesschalck (2008) have shown that complex convolution results in a Banach algebra structure, after introduction of an appropriate norm. I will discuss how these tools are used to approximate non-analytic functions and obtain rigorous computer assisted error bounds on divergent series in computer assisted proofs.

   3. 12:00–14:00 Lunch 🍱
   4. 14:00–15:00 Hugo Chu Computer-assisted proofs for PDEs via Newton iterations: a matrix-free approach abstract

      Computer-assisted proofs have become increasingly common in the study of differential equations and dynamical systems. Many of these proofs rely on a common strategy: first compute a numerical approximation of a solution, then construct a quasi-Newton operator, and finally prove that this operator is a contraction in an explicit neighbourhood of the approximation. Using compactness estimates, the construction of such a quasi-Newton operator can be reduced to the numerical computation of a finite-dimensional inverse. In practice, however, this inverse matrix can be extremely large — easily exceeding the RAM available for a standard cluster job. For three or four-dimensional PDEs, this step frequently becomes the main computational bottleneck.

      In this talk, I will present a new matrix-free approach for handling the finite-dimensional component. This method relies only on standard tools from scientific computing and numerical linear algebra. By leveraging algorithms such as iterative solvers and discrete transforms, the approach is naturally parallelisable and scales better than the traditional methods used in most computer-assisted proofs, both in terms of memory usage and runtime. Time permitting, I will also discuss some of the computational and algorithmic challenges that arise with this new method. This is joint work with Maxime Breden (École Polytechnique).

   5. 15:00–15:30 Hiroaki Miyauchi Computer-assisted proofs for radially symmetric solutions of a semilinear elliptic PDE on the disk via a Fourier–Bessel basis abstract

      We present a computer-assisted proof of the existence and uniqueness of a radially symmetric solution to the semilinear elliptic equation \(\Delta u + u^{2} = 0\) on the unit disk under the Dirichlet boundary condition.

      An approximate solution is represented by an expansion in the Fourier–Bessel basis, whose basis functions are eigenfunctions of the Laplace operator restricted to the space of radially symmetric functions in \(L^{2}(\Omega)\). In this basis, the matrix representation of the Laplace operator is diagonal. Therefore, the original partial differential equation can be rewritten as an equation \(\mathbb{F}(U)=0\) for the coefficients in the Fourier–Bessel expansion. The nonlinear term \(u^2\) leads to sums of products of these coefficients, with the coefficients of these sums given by integrals of products of three Fourier–Bessel basis functions.

      The existence and uniqueness of a solution are proved by combining the Newton–Kantorovich theorem with the radii-polynomial approach. For this purpose, we construct an approximate inverse operator of the form \(A=\Delta^{-1}B\). To verify the conditions in the Newton–Kantorovich argument, we derive bounds for the quantities \(\mathcal{Y}_{0}\), \(\mathcal{Z}_{1}\), and \(\mathcal{Z}_{2}\) using the structure of the Fourier–Bessel basis.

      The quantity \(\mathcal{Y}_{0}\) is a bound for the residual of the approximate solution, \(\mathcal{Z}_{1}\) measures the error of the approximate inverse operator, and \(\mathcal{Z}_{2}\) bounds the local variation of the Fréchet derivative.

      In particular, the tail part of the coefficients arising from the projection of the nonlinear term onto the Fourier–Bessel basis is estimated by using gradient bounds in the Sobolev space \(H^{1}_{0}(\Omega)\) together with the lower bound \(\nu_{0,k}\geq \pi\left(k-\frac14\right)\) for the positive zeros of the Bessel function of the first kind of order zero.

      The bound \(\mathcal{Z}_{2}\), which controls the variation of the Fréchet derivative near the approximate solution, is obtained by using a Gagliardo–Nirenberg inequality for the \(L^{4}(\Omega)\) norm on the unit disk. In addition, the residual associated with the approximate solution is bounded by evaluating a single one-dimensional integral using interval arithmetic.

      All conditions required for the computer-assisted proof are verified with interval arithmetic for the truncation dimensions \(N=50,100,150,\) and \(200\). For each truncation dimension, we find an interval on which the radii polynomial is strictly negative. This proves the existence and uniqueness of a true solution in a neighborhood of the computed approximation.

      We further observe that the residual bound \(\mathcal{Y}_{0}\) decays at a rate consistent with \(O(N^{-5/2})\) as the truncation dimension \(N\) increases. This decay is mainly determined by the tail part that arises when the finite-dimensional approximation is extended to the infinite-dimensional space by setting all coefficients beyond the truncation dimension equal to zero.

   6. 15:30 Closing

Venue