Le principal objectif du projet CRM CAMP est de rassembler la communauté mondiale des chercheurs dans le domaine des méthodes de preuve assistées par ordinateur, en particulier ceux qui travaillent dans les domaines de la théorie des systèmes dynamiques et de l’analyse non linéaire. Cette communauté a connu une croissance spectaculaire au cours des trois dernières décennies, et a développé des méthodes pour résoudre un certain nombre de problèmes importants non résolus en mathématiques. Cependant, les chercheurs participants sont dispersés dans le monde entier et il existe un besoin croissant d’un forum régulier de discussion et de diffusion des résultats. Cela est particulièrement important en cette période d’interruption sans précédent des voyages.
Notre chaîne Youtube
À propos
La série de séminaires du CAMP CRM explore l’interaction entre le calcul scientifique et l’analyse mathématique rigoureuse, en mettant l’accent sur la recherche dans des domaines tels que la théorie des systèmes dynamiques et l’analyse non linéaire. Ce domaine s’est rapidement développé au cours des dernières décennies et, les chercheurs étant répartis dans le monde entier, il est de plus en plus nécessaire de mettre en place un forum régulier pour partager les résultats, poser des questions intéressantes et discuter de nouvelles orientations. Ce projet est envisagé comme une sorte de centre communautaire en ligne pour les rassemblements hebdomadaires, ainsi que comme un dépôt de matériel pédagogique. En plus de la série de conférences hebdomadaires, le programme sert également de mécanisme pour organiser des ateliers, des tutorats et d’autres activités scientifiques. Nous espérons qu’en augmentant la visibilité de cette recherche, le projet stimulera les collaborations entre les groupes existants et entre notre communauté et les mathématiciens travaillant dans d’autres domaines.
This is a series of talks focusing on either open problems concerning techniques of computer-assisted proof, or more broadly open problem in mathematics where the speaker believes there could be a computer-assisted solution. Talks range from 5 minutes to an hour, and can be proposed at any level. When an open problem is solved, or when substantial progress is made, we provide citation and links to the relevant work.
Open Problems passés
8 juin 2021 de 10 h 00 à 11 h 00 (heure de Montréal/HNE) Réunion Zoom
OPEN PROBLEMS SERIES: Some conjectures that seem difficult to prove
Séminaire par Vladimir Sverak (University of Minnesota)
In many cases, numerics and/or heuristics provide compelling evidence for statements that we have trouble proving rigorously. I will discuss some examples, mostly inspired by fluid flows.
1 décembre 2020 de 10 h 00 à 11 h 00 (heure de Montréal/HNE) Réunion Zoom
OPEN PROBLEMS SERIES: Defect and front dynamics: analysis and computation
Séminaire par Arnd Scheel (University of Minnesota, USA)
This will be a personal selection of results and related open problems in dissipative spatially extended systems. I will focus on simple, sometimes universal models such as the complex Ginzburg-Landau, the Swift-Hohenberg, and extended KPP equations and attempts to describe their dynamics based on coherent structures. I will present « conceptual’ analytical results, and describe gaps that rigorous computations may be able to close. Topics include invasion fronts, defects in one- and two-dimensional oscillatory media, and point defects in striped phases.
16 février 2021 de 10 h 00 à 11 h 00 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP COLLOQUIUM: Wherefore computer assisted proofs in dynamics?
Séminaire par Konstantin Mischaikow (Rutgers University, USA)
Over the past few decades the topic of computer assisted proofs in nonlinear dynamics has blossomed and is well on the way to becoming a standard part of the field. So perhaps it is worth reflecting on some high level topics. With this in mind I will discuss, from an admittedly biased personal perspective, several questions:
- Why do computer assisted proofs?
- Where do computer assisted proofs in dynamics as currently being done lie in the bigger scheme of formal proof systems?
- What new perspective about nonlinear dynamics can we extract from computer assisted proofs?
- How should we resolve the dichotomy between precision and accuracy?
- What role do computer assisted proofs have to play as we move into an era of data driven science and machine learning?
3 décembre 2020 de 12 h 00 à 12 h 15 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Rigorous computation of the unstable manifold for equilibria of delay differential equations
Séminaire par Olivier Hénot (McGill University, Canada)
We will review the parameterization method to obtain the unstable manifold of equilibria of Delay Differential Equations. Then, we will discuss how to compute rigorous error bounds for this parameterization.
3 décembre 2020 de 11 h 45 à 12 h 00 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Periodic orbit for Brusselator system with diffusion
Séminaire par Jakub Banaśkiewicz (Jagiellonian University, Poland)
We will present numerical evidence for the existence of periodic solutions to a one-dimensional Brusselator system with diffusion and Dirichlet boundary conditions. Then we discuss a plan for proving their existence by a rigorous integration of differential inclusion corresponding to the first modes of the Galerkin projection and dissipative estimations on further modes.
3 décembre 2020 de 11 h 15 à 11 h 30 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Parameterized invariant manifold and applications in celestial mechanics
Séminaire par Maxime Murray (Florida Atlantic University, USA)
The parameterization method is a well-known framework with proven value to parameterize hyperbolic manifolds attached to periodic solutions of ordinary differential equations. Using a Taylor expansion, one can rewrite the computation of the manifold into a recursive system of linear differential equations describing the coefficients. I will discuss this approach and how to obtain an interval enclosure of the truncated solution to the system. I will then show how validated manifolds are used to compute cycle-to-cycle connections in the case of the circular restricted three-body problem and Hill’s four-body problem.
3 décembre 2020 de 11 h 00 à 11 h 15 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Computer-assisted proofs for a nonlinear Laplace-Beltrami equation on the sphere
Séminaire par Gabriel William Duchesne (McGill University, Canada)
We prove the existence and local uniqueness of radially symmetric solutions of nonlinear Laplace-Beltrami equation on the sphere by using the Radii Polynomial Theorem on Banach spaces with a combination of Taylor and Chebyshev coefficients of the solutions.
3 décembre 2020 de 10 h 45 à 11 h 00 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Computer-assisted proofs of two-dimensional attracting invariant tori for ODEs
Séminaire par Emmanuel Fleurantin (Florida Atlantic University, USA)
We study the existence and regularity questions for attracting invariant tori in three dimensional dissipative systems of ordinary differential equations. Our main result is a constructive method of computer assisted proof which applies to explicit problems in non-perturbative regimes. We consider separately two important cases of rotational and resonant tori for which we describe how we apply our methods. This is a joint work with Maciej Capinski and J.D. Mireles-James.
3 décembre 2020 de 10 h 15 à 10 h 30 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Computer-assisted existence proofs for Navier-Stokes equations on an unbounded strip with obstacle
Séminaire par Jonathan Wunderlich (Karlsruhe Institute of Technology, Germany)
The incompressible stationary 2D Navier-Stokes equations are considered on an unbounded strip domain with a compact obstacle. In order to get existence and error bounds (in a Sobolev space) for a solution, an approximate solution (using divergence-free finite elements), a bound for its defect, and a norm bound for the inverse of the linearization at the approximate solution are computed. For the latter, bounds for the essential spectrum and for eigenvalues play a crucial role, especially for the eigenvalues “close to” zero. Note that, on an unbounded domain, the only possible method for computing the desired norm bound appears to be via eigenvalue bounds. In this way, the first rigorous existence proof for the Navier-Stokes problem under consideration is obtained.
3 décembre 2020 de 10 h 00 à 10 h 15 (heure de Montréal/HNE) Réunion Zoom
CRM-CAMP SPOTLIGHT ON GRADUATE RESEARCH: Computation of tight enclosures for Laplacian eigenvalues
Séminaire par Joel Dahne (Uppsala University, Sweden)
Recently, there has been interest in high-precision approximations of the fundamental eigenvalue of the Laplace-Beltrami operator on spherical triangles for combinatorial purposes. We present computations of improved and rigorous enclosures to these eigenvalues. This is achieved by applying the method of particular solutions in high precision, the enclosure being obtained by a combination of interval arithmetic and Taylor models. The index of the eigenvalue can be certified by exploiting the monotonicity of the eigenvalue with respect to the domain. The classically troublesome case of singular corners we handle by combining expansions from all singular corners and an expansion from an interior point.
