Registered Data

[01768] Computer-assisted proofs in differential equations

  • Session Time & Room :
    • 01768 (1/4) : 3C (Aug.23, 13:20-15:00) @G405
    • 01768 (2/4) : 3D (Aug.23, 15:30-17:10) @G405
    • 01768 (3/4) : 3E (Aug.23, 17:40-19:20) @G405
    • 01768 (4/4) : 4C (Aug.24, 13:20-15:00) @G405
  • Type : Proposal of Minisymposium
  • Abstract : Several phenomena from biology, physics and chemistry are described by differential equations. While the presence of nonlinearities complicates the mathematical analysis, the challenges are greater for PDEs and delay equations, which are infinite dimensional. Numerics have therefore become the primary tool used by scientists, which leads to the question of validity of the outputs. To address this, the field of computer-assisted proofs (CAPs) in dynamics emerged at the intersection of scientific computing, nonlinear, numerical and functional analysis and approximation theory. This minisymposium will bring experts describing novel CAPs techniques to study cutting-edge problems in finite and infinite dimensional differential equations.
  • Organizer(s) : Jean-Philippe Lessard, Akitoshi Takayasu, Nobito Yamamoto
  • Classification : 35-XX, 37-XX, 65-XX, 34-XX, 65Gxx
  • Minisymposium Program :
    • 01768 (1/4) : 3C @G405 [Chair: Akitoshi Takayasu]
      • [04529] Numerical verification methods for ODEs with conservative quantity
        • Format : Talk at Waseda University
        • Author(s) :
          • Nobito Yamamoto (The University of Electro-Communications)
          • Koki Nitta (The University of Electro-Communications)
        • Abstract : We are treating ODEs with conservative quantity and interested in proving existence of time-global solutions remaining in a given sphere with common points on the surface. There is difficulty in computing the solution orbits for a long time due to drift between solutions of conservative systems. Our method is based on verified computation of the conservative quantity and the flow on the surface of the sphere. Numerical examples derived from Schroedinger equation will be shown.
      • [04834] Computer-assisted Existence Proofs for Navier-Stokes Equations on an Unbounded Strip with Obstacle
        • Format : Talk at Waseda University
        • Author(s) :
          • Michael Plum (Karlsruhe Institute of Technology)
          • Jonathan Wunderlich (Karlsruhe Institute of Technology)
        • Abstract : The incompressible stationary 2D Navier-Stokes equations are considered on an unbounded strip domain with a compact obstacle. A computer- assisted existence and enclosure result for the velocity (in a suitable diver- gence-free Sobolev space) is presented. Starting from a numerical approximate solution (computed with divergence-free finite elements), we determine a bound for its defect and a norm bound for the inverse of the linearization at the approximate solution. For the latter, bounds for the essential spectrum and for eigenvalues close to zero of an associated self-adjoint operator play a crucial role. To obtain the desired lower bounds for the eigenvalues below the essential spectrum we use a combination of the Rayleigh-Ritz method, a corollary of the Temple-Lehmann-Goerisch theorem and a homotopy method.
      • [04194] Relative equilibria for the n-body problem
        • Format : Talk at Waseda University
        • Author(s) :
          • Warwick Tucker (Monash University)
          • Jordi-Lluis Figueras (Uppsala University)
          • Piotr Zgliczynski (Jagiellonian University)
        • Abstract : We will discuss the classical problem from celestial mechanics of determining the number of relative equilibria a set of planets can display. Several already established results will be presented, as well as a new contribution (in terms of a new proof) for the restricted 4-body problem. We will discuss its possible extensions to harder instances of the general problem.
      • [05267] Chaos in Mackey-Glass: computation of transverse homoclinic orbits
        • Format : Talk at Waseda University
        • Author(s) :
          • Olivier Hénot (McGill University University)
        • Abstract : The Mackey-Glass equation is a scalar delay differential equation, famous for its rich dynamics. Since 1977, the equation has become a primary example of chaos in infinite dimensions. Yet, a proof of existence of chaotic dynamics remains an open problem. In this talk, we present a computational method for studying transverse homoclinic orbits for periodic solutions of delay differential equations. The connection is formulated as the zero of a nonlinear map representing a boundary value problem, with boundary conditions in the (finite dimensional) unstable and (infinite dimensional) stable manifolds of the periodic orbit; the transversality of the intersection is a by-product of the invertibility of the Fréchet derivative of the map. This technique is designed to be amenable for computer-assisted proofs through a Newton-Kantorovich type argument. As a notable illustration, we compute a transverse homoclinic orbit in the Mackey-Glass equation.
    • 01768 (2/4) : 3D @G405 [Chair: Jean-Philippe Lessard]
      • [05182] Smooth imploding solutions for 3D compressible fluids
        • Format : Talk at Waseda University
        • Author(s) :
          • Javier Gomez Serrano (Brown University)
        • Abstract : In this talk I will present results on singularity formation for the 3D isentropic compressible Euler and Navier-Stokes equations for ideal gases. These equations describe the motion of a compressible ideal gas, which is characterized by a parameter called the adiabatic constant. Finite time singularities for generic adiabatic constants were found in the recent breakthrough of Merle, Raphaël, Rodnianski and Szeftel. Our results allow us to drop the genericity assumption and construct smooth self-similar profiles for all values of the adiabatic constant. In particular, we will construct the first smooth self-similar profile for a monoatomic gas. Part of the proof is very delicate and requires a computer-assisted analysis. Joint work with Tristan Buckmaster and Gonzalo Cao-Labora.
      • [02910] Computer-assisted proofs of localized patterns in the planar Swift-Hohenberg equation
        • Format : Talk at Waseda University
        • Author(s) :
          • Matthieu Cadiot (McGill University)
          • Jean-Philippe Lessard (McGill University)
          • Jean-Christophe Nave (McGill University)
        • Abstract : In this talk, I will present computer-assisted proofs of stationary localized patterns in the planar Swift-Hohenberg equation. Using a Newton-Kantorovich approach, we develop a numerical method to prove local existence and uniqueness of strong solutions in $\mathbb{R}^m$. In particular, I will explain how we manage to approximate the inverse of the linearization of the PDE around some approximated solution. Finally, I will expose the numerical details of some specific computer-assisted proofs.
      • [05035] Rigorous computation of Poincare maps
        • Format : Talk at Waseda University
        • Author(s) :
          • Daniel Wilczak (Jagiellonian University)
          • Tomasz Kapela (Jagiellonian University)
          • Piotr Zgliczyński (Jagiellonian University)
        • Abstract : We present recent advances on interval methods for rigorous computation of Poincare maps. We also discuss the impact of choice of Poincare section and coordinate system on obtained bounds for computing Poincare map nearby fixed points.
      • [02908] Validation of Elliptic Invariant Tori in Hamiltonian Systems
        • Format : Talk at Waseda University
        • Author(s) :
          • Chiara Caracciolo (Uppsala University)
        • Abstract : The applicability of KAM theorem to realistic physical problems can be significantly improved by CAPs. These proofs exploit the explicit computation of approximately invariant solutions by the mean of normal forms or parametrization methods. I will discuss the extension of these techniques to lower-dimensional elliptic tori and present an algorithm based on a parametrization method. I will discuss the main benefits of this technique and how it can be made completely rigorous. Based on joint works with J-Ll. Figueras, A. Haro, U. Locatelli.
    • 01768 (3/4) : 3E @G405 [Chair: Nobito Yamamoto]
      • [03720] Validated Numerics for divergent series via the Borel Transform
        • Format : Talk at Waseda University
        • Author(s) :
          • Jason Desmond Mireles James (Florida Atlantic University)
        • Abstract : Parabolic invariant manifolds are associated with fixed points of diffeomorphisms which have one as an eigenvalue of the linearization, or equilibrium solutions of differential equations which have zero as an eigenvalue. Supposing that the map or vector field is real analytic, It is well known (for example Baldoma and Haro, 2008) that while the Taylor expansion of the manifold may diverge, it typically does so in a Gevery fashion. That is, the power series coefficients diverge like a factorial. In this case, some truncations of the divergent series may still provide useful approximation, and it is desirable to have quantitative bounds on the errors. This is in fact necessary if the expansion is going to be used as an ingredient of a subsequent computer assisted proof. I will discuss a method for obtaining such bounds based on Borel resummation. The idea is that the Borel transform of the conjugacy equation describing the parabolic manifold has much nicer properties than the original equation. For example the transformed equation typically has analytic solutions. I will discuss methods for solving the transformed equation using validated numerics. If one can analytically continue this solution (in a process similar to numerical integration) to an open set covering the positive real axis in the complex Borel Plane, then it is possible to take a Laplace transform, recovering the solution to the original problem. This procedure also leads to validated computer assisted error bounds.
      • [04398] Characterising blenders via covering relations and cone conditions
        • Format : Talk at Waseda University
        • Author(s) :
          • Hinke M Osinga (University of Auckland)
          • Bernd Krauskopf (University of Auckland)
          • Piotr Zgliczynski (Jagiellonian University)
          • Maciej Capinski (AGH University of Science and Technology)
        • Abstract : A blender is an invariant hyperbolic set of a diffeomorphism with the property that its stable or unstable manifold has a dimension larger than expected from the underlying hyperbolic splitting. We present a characterisation of a blender based on the correct topological alignment of sets in combination with the propagation of cones. It is applicable to multidimensional blenders in ambient phase spaces of any dimension. The required conditions can be verified by checking properties of a single iterate of the diffeomorphism, which is achieved by positioning the required sets in such a way that they form a suitable sequence of coverings. This setup is flexible and allows for a rigorous, interval arithmetic based, computer assisted validation.
      • [03900] Validated integration of semilinear parabolic PDEs
        • Format : Talk at Waseda University
        • Author(s) :
          • Maxime Breden (Ecole polytechnique)
          • Jan Bouwe van den Berg (VU Amsterdam)
          • Ray Sheombarsing (VU Amsterdam)
        • Abstract : Integrating evolutionary partial differential equations (PDEs) is an essential ingredient for studying the dynamics of the solutions. Indeed, simulations are at the core of scientific computing, but their mathematical reliability is often difficult to quantify, especially when one is interested in the output of a given simulation, rather than in the asymptotic regime where the discretization parameter tends to zero. In this paper we present a computer-assisted proof methodology to perform rigorous time integration for scalar semilinear parabolic PDEs with periodic boundary conditions. We formulate an equivalent zero-finding problem based on a variations of constants formula in Fourier space. Using Chebyshev interpolation and domain decomposition, we then finish the proof with a Newton-Kantorovich type argument. The final output of this procedure is a proof of existence of an orbit, together with guaranteed error bounds between this orbit and a numerically computed approximation. We illustrate the versatility of the approach with results for the Fisher equation, the Swift-Hohenberg equation, the Ohta-Kawasaki equation and the Kuramoto–Sivashinsky equation. We expect that this rigorous integrator can form the basis for studying boundary value problems for connecting orbits in partial differential equations.
      • [05270] Validated dynamics in neural networks: towards chaos
        • Format : Talk at Waseda University
        • Author(s) :
          • Elena Queirolo (TUM)
        • Abstract : Neural networks, a class of machine learning algorithms, can be interpreted as dynamical systems an d can be studied by dynamical techniques. Here, we use validation techniques to understand how the reliability of the algorithm relates to dynamical behaviours. In particular, we want to investigate the co nnection between chaos and reliability. First, we prove or disprove the existence of chaos in a given neural net, then we draw behavioural conclusions based on its existence.
    • 01768 (4/4) : 4C @G405 [Chair: Akitoshi Takayasu]
      • [05292] Global Dynamics and Blowup in Some Quadratic PDEs
        • Format : Talk at Waseda University
        • Author(s) :
          • Jonathan Jaquette
          • Jean-Philippe Lessard (McGill University)
          • Akitoshi Takayasu (University of Tsukuba)
        • Abstract : Conservation laws and Lyapunov functions are powerful tools for proving the global existence of stability of solutions, but for many complex systems these tools are insufficient to completely understand non-perturbative dynamics. In this talk I will discuss a complex-scalar PDE which may be seen as a toy model for vortex stretching in fluid flow, and cannot be neatly categorized as conservative nor dissipative. In a recent series of papers we have shown that this equation exhibits rich dynamical behavior that exist globally in time: non-trivial equilibria, homoclinic orbits, heteroclinic orbits, and integrable subsystems foliated by periodic orbits. On the other side of the coin, we show several mechanisms by which solutions can blowup. I will discuss these results, and current work toward understanding unstable blowup.
      • [05275] Worrisome Properties of Symbolic Representations of Deep Neural Network Controllers
        • Format : Talk at Waseda University
        • Author(s) :
          • Jacek Cyranka (Warsaw University)
          • Kevin Church ( Université de Montréal )
          • Jean-Philippe Lessard (McGill University)
        • Abstract : We studied dynamics of simple controlled problems like Pendulum and CartPole, where the controllers were trained using reinforcement learning algorithms. We raise concerns about symbolic controllers' robustness. A typical symbolic controller reaching high mean return values still generates an abundance of unstabilized solutions, which is highly undesirable property, easily exploitable by an adversary. We provide an algorithm for a systematic robustness study and prove the unstabilized solutions and periodic orbits, using a computer-assisted proof methodology.
      • [05090] A rigorous integrator and global existence for higher-dimensional semilinear parabolic PDEs via semigroup theory
        • Format : Talk at Waseda University
        • Author(s) :
          • Gabriel William Duchesne (McGill)
        • Abstract : In this talk, we introduce a general constructive method to compute solutions of initial and boundary value problems of semilinear parabolic partial differential equations via semigroup theory and computer-assisted proofs. We will present techniques to prove the global existence of solutions in the 2D/3D Swift-Hohenberg equation and to prove the existence of a solution of a projected boundary value problem in the 2D Ohta-Kawasaki equation.