23 février 2021 de 10 h 00 à 11 h 00 (heure de Montréal/HNE) Réunion Zoom
A wide range of techniques have been developed to compute validated numerical solutions to various kind of equations (e.g., ODE, PDE, DDE) arising in computer-assisted proofs. Among them are Newton-Galerkin a posteriori validation techniques, which provide error bounds for approximate solutions by using the contraction map principle in a suitable coefficient space (e.g., Fourier or Chebyshev). More precisely, a contracting Newton-like operator is constructed by truncating and inverting the inverse Jacobian of the equation.
While these techniques were extensively used in cutting-edge works in the community, we show that they suffer from an exponential running time w.r.t. the input equation. We illustrate this shortcomings on simple linear ODEs, where a "large" parameter in the equation leads to an intractable instance for Newton-Galerkin validation algorithms.
From this observation, we build a new validation scheme, called Newton-Picard, which breaks this complexity barrier. The key idea consists in replacing the inverse Jacobian not by a finite-dimensional truncated matrix as in Newton-Galerkin, but by an integral operator with a polynomial approximation of the so-called resolvent kernel. Moreover, this method is also less basis-dependent and more suitable to be formalized in a computer proof assistant towards a fully certified implementation in the future.